theorem proved term proof

`minkowski_christoffel_zero`

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

formal statement (Lean)

  61@[simp] theorem minkowski_christoffel_zero
  62    (x : Fin 4 → ℝ) (ρ μ ν : Fin 4) :
  63    (christoffel_from_metric minkowski_tensor).Γ x ρ μ ν = 0 := rfl

proof body

Term-mode proof.

  64
  65end Geometry
  66end Relativity
  67end IndisputableMonolith

depends on (3)

Lean names referenced from this declaration's body.

christoffel_from_metric in IndisputableMonolith.Gravity.Connection decl_use
christoffel_from_metric in IndisputableMonolith.Relativity.Geometry.Connection decl_use
minkowski_tensor in IndisputableMonolith.Relativity.Geometry.Metric decl_use