Theorem NoZeroDivisors.toIsCancelMulZero

Modification history

2026-01-20 16:34
Mathlib/Algebra/Ring/Regular.lean
chore(Algebra): deprecate `CancelMonoidWithZero` (#33851) …
Added NoZeroDivisors.toIsCancelMulZeroView on Github →