Revision #1404 → #2610 · back to history
modifiedArc length on a parametric surface01e23096e607
| Field | From #1404 | To #2610 |
|---|
| mathlib.decl | pathELength | Manifold.pathELength |
| provenance | ai | ai-moderated |
modifiedSylvester's law of inertia for metric diagonalizationf43b68127d21
| Field | From #1404 | To #2610 |
|---|
| mathlib.decl | QuadraticForm.sigPos_of_equiv_weightedSumOfSquares | QuadraticForm.sigPos_of_equiv_weightedSumSquares |
| provenance | ai | ai-moderated |
modifiedSignature of a metric7d4aec959128
| Field | From #1404 | To #2610 |
|---|
| mathlib.decl | QuadraticForm.sigPos | sigPos |
| provenance | ai | ai-moderated |
modifiedImmersion and immersed submanifold6bdef46bf539
| Field | From #1404 | To #2610 |
|---|
| mathlib.decl | IsImmersion | Manifold.IsImmersion |
| provenance | ai | ai-moderated |
modifiedArclength of a parametric curve on a Riemannian manifold5f029ec45a4c
| Field | From #1404 | To #2610 |
|---|
| mathlib.decl | pathELength | Manifold.pathELength |
| provenance | ai | ai-moderated |
modifiedCoordinate-independence of length formulas8a7153fb9534
| Field | From #1404 | To #2610 |
|---|
| mathlib.decl | pathELength | Manifold.pathELength |
| provenance | ai | ai-moderated |