Revision #3617 → #4159 · back to history
2dfcff3c05eb| Field | From #3617 | To #4159 |
|---|---|---|
| mathlib.decl | — | CovariantDerivative.IsLeviCivitaConnection.uniqueness |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.LeviCivita |
| note | Although metric-compatibility and torsion-freeness are defined, existence/uniqueness of the Levi-Civita connection is not proved in Mathlib. | Existence is `CovariantDerivative.leviCivitaConnection` with `isLeviCivitaConnection_leviCivitaConnection` (compatible + torsion-free), and uniqueness on differentiable vector fields is `IsLeviCivitaConnection.uniqueness`. |
| status | not_formalized | formalized |
c29f7d266e4f0506d66deff75d5f19ba4b0dd3173b4383c8d79d15abb919f55bddcf84d77acf41f7c3779c3fcfb7227ceb9454e4ab94a04764bf0d4b