pith. machine review for the scientific record. sign in
theorem proved term proof

gradient_squared_minkowski

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  83theorem gradient_squared_minkowski (φ : ScalarField) (x : Fin 4 → ℝ) :
  84  gradient_squared φ minkowski_tensor x =
  85    -(gradient φ x 0)^2 + (gradient φ x 1)^2 + (gradient φ x 2)^2 + (gradient φ x 3)^2 := by

proof body

Term-mode proof.

  86  unfold gradient_squared
  87  apply gradient_squared_minkowski_sum
  88
  89/-- Field squared. -/

depends on (7)

Lean names referenced from this declaration's body.