Commit 2024-10-01 11:19 4ae56c11

View on Github →

chore: rename unique_diff to uniqueDiffOn in theorems (#17291)

Estimated changes

Modified Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean

Modified Mathlib/Geometry/Manifold/Diffeomorph.lean

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

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

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

Modified Mathlib/Geometry/Manifold/SmoothManifoldWithCorners.lean

added theorem ModelWithCorners.uniqueDiffOn_preimage

added theorem ModelWithCorners.uniqueDiffOn_preimage_source

added theorem ModelWithCorners.uniqueDiffWithinAt_image

deleted theorem ModelWithCorners.unique_diff_at_image

deleted theorem ModelWithCorners.unique_diff_preimage

deleted theorem ModelWithCorners.unique_diff_preimage_source

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