Commit 2026-09-03 14:21 03134a32

View on Github →

feat(Algebra/Group/Units/Basic): deduplicate lemmas by generalizing to IsDedekindFiniteMonoid (#41457) Generalize a group of lemmas to IsDedekindFiniteMonoid which previously had versions for CommMonoid, LeftCancelMonoid, RightCancelMonoid, CancelMonoid, and Ordinal.

Estimated changes

Modified Mathlib/Algebra/AffineMonoid/Irreducible.lean

Modified Mathlib/Algebra/Group/Units/Basic.lean

deleted theorem eq_one_of_mul_left'

modified theorem eq_one_of_mul_left

deleted theorem eq_one_of_mul_right'

deleted theorem mul_eq_one'

deleted theorem mul_ne_one'

modified theorem mul_ne_one

Modified Mathlib/AlgebraicTopology/SimplicialSet/Horn.lean

Modified Mathlib/Combinatorics/Enumerative/DyckWord.lean

Modified Mathlib/SetTheory/Ordinal/Arithmetic.lean

deleted theorem Ordinal.add_eq_zero_iff

deleted theorem Ordinal.left_eq_zero_of_add_eq_zero

deleted theorem Ordinal.right_eq_zero_of_add_eq_zero

Modified Mathlib/SetTheory/Ordinal/Exponential.lean

Modified scripts/nolints_prime_decls.txt