Commit 2025-01-10 13:09 a3ae5436

View on Github →

chore(Geometry/Manifold): move SmoothManifoldWithCorners.lean to IsManifold.lean (#20611) Follow-up to #19696; split into a separate PR to not confuse git.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Geometry/Manifold/AnalyticManifold.lean

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

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

Modified Mathlib/Geometry/Manifold/InteriorBoundary.lean

Renamed Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean to Mathlib/Geometry/Manifold/IsManifold.lean

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

Modified Mathlib/Geometry/Manifold/Metrizable.lean