pith. machine review for the scientific record. sign in
structure definition def or abbrev

ChristoffelSymbols

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)

  24structure ChristoffelSymbols where
  25  Γ : (Fin 4 → ℝ) → Fin 4 → Fin 4 → Fin 4 → ℝ := fun _ _ _ _ => 0

proof body

Definition body.

  26
  27/-- Christoffel symmetry predicate: Γ^ρ_μν = Γ^ρ_νμ. -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.