179structure FundamentalTheoremExistence (g : MetricTensor) : Prop where 180 torsion_free : IsTorsionFree (christoffel g) 181 metric_compatible : ∀ x, KoszulIdentity g x → 182 ∀ ρ μ ν, cov_deriv_metric (christoffel g) g x ρ μ ν = 0 183 184/-- The Fundamental Theorem of Pseudo-Riemannian Geometry (uniqueness part): 185 Any torsion-free, metric-compatible connection has the same lowered coefficients 186 as the Christoffel connection. -/
used by (3)
From the project-wide theorem graph. These declarations reference this one in their body.