Commit 2026-09-21 19:06 a8db657b

View on Github →

chore: rename declarations whose names do not match their statements (#44051) The lemmas about IsLocalDiffeomorphAt.localInverse simply were in the wrong order: they should say continuous_localInverse etc. instead of localInverse_continuous. In some cases, both variants already existed (so we deprecated the wrongly named one). Split out of #43889. Written with the assistance of Claude (Claude Code).

Estimated changes

Modified Mathlib/Algebra/Order/Ring/Cast.lean

deleted theorem Int.nneg_mul_add_sq_of_abs_le_one

added theorem Int.nonneg_mul_add_sq_of_abs_le_one

Modified Mathlib/Algebra/Vertex/HVertexOperator.lean

deleted theorem HVertexOperator.coeff_isPWOsupport

added theorem HVertexOperator.isPWO_support_coeff

modified theorem HVertexOperator.of_coeff_coeff

Modified Mathlib/CategoryTheory/Sites/LeftExact.lean

Modified Mathlib/Data/Rat/Lemmas.lean

added theorem Rat.sub_num_den'

deleted theorem Rat.substr_num_den'

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

Modified Mathlib/Geometry/Manifold/LocalDiffeomorph.lean

added theorem IsLocalDiffeomorphAt.contMDiffAt_localInverse

added theorem IsLocalDiffeomorphAt.contMDiffOn_localInverse

deleted theorem IsLocalDiffeomorphAt.contmdiffOn_localInverse

deleted theorem IsLocalDiffeomorphAt.localInverse_contMDiffAt

deleted theorem IsLocalDiffeomorphAt.localInverse_contMDiffOn

deleted theorem IsLocalDiffeomorphAt.localInverse_mdifferentiableAt

added theorem IsLocalDiffeomorphAt.mdifferentiableAt_localInverse

Modified Mathlib/NumberTheory/Modular.lean

Modified Mathlib/Probability/Martingale/Convergence.lean

deleted theorem MeasureTheory.tendsto_of_uncrossing_lt_top

added theorem MeasureTheory.tendsto_of_upcrossings_lt_top

Modified scripts/nolints_prime_decls.txt