`field_squared_nonneg`

proved

show as: view math explainer →

module: IndisputableMonolith.Relativity.Fields.Scalar
domain: Relativity
line: 93 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Relativity.Fields.Scalar on GitHub at line 93.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  90noncomputable def field_squared (φ : ScalarField) (x : Fin 4 → ℝ) : ℝ :=
  91  (φ.ψ x) ^ 2
  92
  93theorem field_squared_nonneg (φ : ScalarField) (x : Fin 4 → ℝ) :
  94  field_squared φ x ≥ 0 := by
  95  simp [field_squared]
  96  exact sq_nonneg _
  97
  98end Fields
  99end Relativity
 100end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.