Commit 2026-08-05 23:32 8be9d514

View on Github →

chore: generalize NoZeroDivisors to IsReduced when possible (#42417) Follow-up to #33775. In several places where eq_zero_of_pow_eq_zero or related lemmas are being used, we can generalize from NoZeroDivisors to IsReduced without changing anything else.

Estimated changes

Modified Mathlib/Algebra/GroupWithZero/Indicator.lean

Modified Mathlib/Algebra/GroupWithZero/Torsion.lean

modified theorem IsMulTorsionFree.mk'

Modified Mathlib/Algebra/IsPrimePow.lean

modified theorem IsPrimePow.ne_zero

modified theorem not_isPrimePow_zero

Modified Mathlib/Algebra/Order/GroupWithZero/Canonical.lean

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

modified theorem CanonicallyOrderedAdd.pow_pos

Modified Mathlib/Tactic/LinearCombinationPrime.lean

modified theorem Mathlib.Tactic.LinearCombinationPrime.eq_of_add_pow