Commit 2026-04-17 14:24 42a456f0
View on Github →chore(Geometry/Manifold): don't expose definitions depending on choice (#37358)
Some definitions in Immersion.lean still depend on choice, but need to be exposed for subsequent instances using their definition. We leave them alone for now.
Also make not exposing definition the default in LocalDiffeomorph.lean;
four definitions have useful definitional equalities, the others do not.