Commit 2026-10-06 22:43 474912ea

View on Github →

chore: deprecate plus and minus in names (#44566) This doesn't touch haves, only lemma names. This also fixes an incorrect to_additive that was turning a Nat + 1 into add_zero in the name.

Estimated changes

Modified Archive/MiuLanguage/DecisionSuf.lean

deleted theorem Miu.replicate_pow_minus_append

added theorem Miu.replicate_pow_sub_append

Modified Mathlib/Algebra/Order/Interval/Set/Instances.lean

deleted theorem Set.Ioo.one_minus_lt_one

deleted theorem Set.Ioo.one_minus_pos

added theorem Set.Ioo.one_sub_lt_one

added theorem Set.Ioo.one_sub_pos

Modified Mathlib/Computability/Ackermann.lean

Modified Mathlib/GroupTheory/Nilpotent.lean

added theorem Group.nilpotencyClass_eq_quotient_center_add_one

deleted theorem Group.nilpotencyClass_eq_quotient_center_plus_one

Modified Mathlib/RingTheory/HahnSeries/Summable.lean

deleted theorem HahnSeries.one_minus_single_neg_mul

added theorem HahnSeries.one_sub_single_neg_mul

Modified Mathlib/Topology/Subpath.lean

Modified Mathlib/Topology/UnitInterval.lean

deleted theorem unitInterval.one_minus_le_one

deleted theorem unitInterval.one_minus_nonneg

added theorem unitInterval.one_sub_le_one

added theorem unitInterval.one_sub_nonneg