Commit 2025-12-20 08:12 665d8616

View on Github →

fix: rename definitions which use underscores in their name (#33103) Per the naming convention, "all other terms of types" should be named in lowerCamelCase: this applies to all changes made in this PR. This PR is far from exhaustive.

Estimated changes

Modified Mathlib/Geometry/Manifold/IsManifold/Basic.lean

added def ModelWithCorners.ofConvexRange

added def ModelWithCorners.ofTargetUniv

deleted def ModelWithCorners.of_convex_range

deleted def ModelWithCorners.of_target_univ

Modified Mathlib/Geometry/Manifold/LocalDiffeomorph.lean

Modified Mathlib/Geometry/Manifold/VectorBundle/LocalFrame.lean

deleted def IsLocalFrameOn.fintype_of_finiteDimensional

Modified Mathlib/Topology/IsLocalHomeomorph.lean