Revision #1713 → #2554 · back to history
modifiedRiemannian metric on a surfaceb29ae80895d9
| Field | From #1713 | To #2554 |
|---|
| mathlib.decl | RiemannianMetric | Bundle.RiemannianMetric |
| provenance | ai | ai-moderated |
modifiedLength and energy of a pathe0c2a25a26b2
| Field | From #1713 | To #2554 |
|---|
| mathlib.decl | pathELength | Manifold.pathELength |
| provenance | ai | ai-moderated |
modifiedLength independent of parametrizationc0f8c91655ba
| Field | From #1713 | To #2554 |
|---|
| mathlib.decl | pathELength_comp_of_monotoneOn | Manifold.pathELength_comp_of_monotoneOn |
| provenance | ai | ai-moderated |