Commit 2026-09-22 06:19 eaaea467

View on Github →

chore: fix camelCase capitalisation in declaration names (#44050) Fixes capitalisation in seven declaration names. Old and new are identical letter-for-letter once case is ignored, so this is a naming-convention judgement rather than a spelling one. Each keeps a @[deprecated] alias. Split out of #43889. Written with the assistance of Claude (Claude Code).

Estimated changes

Modified Mathlib/Algebra/Ring/Ext.lean

added theorem NonAssocRing.toNonUnitalNonAssocRing_injective

deleted theorem NonAssocRing.toNonUnitalNonAssocring_injective

added theorem NonUnitalRing.toNonUnitalNonAssocRing_injective

deleted theorem NonUnitalRing.toNonUnitalNonAssocring_injective

Modified Mathlib/Analysis/Complex/Hadamard.lean

added theorem Complex.HadamardThreeLines.eventuallyLE

deleted theorem Complex.HadamardThreeLines.eventuallyle

Modified Mathlib/CategoryTheory/Monoidal/Limits/Preserves.lean

deleted theorem CategoryTheory.MonoidalCategory.Limits.preservesCoLimit_curriedTensor

added theorem CategoryTheory.MonoidalCategory.Limits.preservesColimit_curriedTensor

Modified Mathlib/LinearAlgebra/BilinearMap.lean

added theorem LinearMap.lsmul_eq_distribSMulToLinearMap

deleted theorem LinearMap.lsmul_eq_distribSMultoLinearMap

Modified Mathlib/NumberTheory/ModularForms/ArithmeticSubgroups.lean

added theorem Subgroup.relIndex_adjoinNegOne_eq_two

deleted theorem Subgroup.relindex_adjoinNegOne_eq_two

Modified Mathlib/RingTheory/AdjoinRoot.lean

added theorem AdjoinRoot.mapAlgHom_comp_mapAlgHom

deleted theorem AdjoinRoot.mapAlgHom_comp_mapAlghom

Modified Mathlib/RingTheory/Flat/Equalizer.lean

added theorem LinearMap.lTensor_eqLocus_subtype_tensorEqLocusEquiv_symm

deleted theorem LinearMap.lTensor_eqLocus_subtype_tensoreqLocusEquiv_symm

Modified Mathlib/RingTheory/Regular/IsSMulRegular.lean