Commit 2026-06-05 10:09 808ebe0e

View on Github →

chore(Geometry/Manifold): remove some @[expose] public section (#39886) Go through a few files and audit the exposed definitions there. Best reviewed commit by commit.

Estimated changes

Modified Mathlib/Geometry/Manifold/Bordism.lean

modified def SingularManifold.empty.{u}

modified theorem SingularManifold.empty_M

modified def SingularManifold.map.{u}

modified def SingularManifold.prod

modified def SingularManifold.sum

modified theorem SingularManifold.sum_M

modified theorem SingularManifold.sum_f

modified def SingularManifold.toPUnit

Modified Mathlib/Geometry/Manifold/VectorField/LieBracket.lean

Modified Mathlib/Geometry/Manifold/WhitneyEmbedding.lean

deleted theorem SmoothBumpCovering.exists_immersion_euclidean

deleted theorem exists_embedding_euclidean_of_compact