Mathlib v3 is deprecated. Go to Mathlib v4

Def no_zero_divisors.to_cancel_comm_monoid_with_zero

Modification history

2022-10-09 08:02
src/algebra/ring/basic.lean
chore(algebra/ring/basic): move results about regular elements (#16865)
Modified no_zero_divisors.to_cancel_comm_monoid_with_zeroView on Github →
2022-05-22 23:41
src/algebra/ring/basic.lean
feat(algebra/ring/basic): add `no_zero_divisors.to_cancel_comm_monoid_with_zero` (#14302) …
Added no_zero_divisors.to_cancel_comm_monoid_with_zeroView on Github →