Revision #3455 → #4004 · back to history
modifiedDefinition of submersione5952a18fdc1
| Field | From #3455 | To #4004 |
|---|
| mathlib.decl | — | Manifold.IsSubmersion |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Geometry.Manifold.Submersion |
| note | Mathlib does not have a definition of submersion (surjective differential) for maps between manifolds. The concept exists in `Immersion.lean` docstrings as future work but has not been implemented. | `Manifold.IsSubmersion I J n f` formalizes C^n submersions between manifolds via local normal forms (charts in which `f` looks like the projection `(u,v) ↦ u`). |
| status | not_formalized | formalized |
modifiedJacobian matrix5fb7e76437d7
| Field | From #3455 | To #4004 |
|---|
| mathlib.module | Mathlib.Analysis.Calculus.FDeriv.Basic | Mathlib.Analysis.Calculus.FDeriv.Defs |
addedDefinition of differentiable manifoldebad31ff285d
addedComposition of diffeomorphisms is a diffeomorphism5749da14fcab
addedConfiguration space of a manifold0d0e877b347e
addedAlexander trick: extending a circle diffeomorphism to the disc3614495f0bd2
addedMapping class group of the torus is SL(2,Z) (the modular group)51692c5287de
addedGroup extension: components of Diff(M) split via permutations of components of Maed1b783a4fd