Commit 2024-12-09 08:25 b670b3ca

View on Github →

chore: cleanup of manifold files (#19807) As a preparation for #19696

Estimated changes

Modified Mathlib/Analysis/Calculus/ContDiff/Defs.lean

Modified Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean

Modified Mathlib/Geometry/Manifold/Algebra/LieGroup.lean

Modified Mathlib/Geometry/Manifold/ChartedSpace.lean

added theorem StructureGroupoid.maximalAtlas_mono

Modified Mathlib/Geometry/Manifold/ContMDiff/Defs.lean

added theorem contMDiffOn_zero_iff

added theorem contMDiff_zero_iff

Modified Mathlib/Geometry/Manifold/Diffeomorph.lean

Modified Mathlib/Geometry/Manifold/Instances/Real.lean

Modified Mathlib/Geometry/Manifold/MFDeriv/NormedSpace.lean

Modified Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean