mathlib
9e9a2c9e - feat(algebra/ring/basic): add `no_zero_divisors.to_cancel_comm_monoid_with_zero` (#14302)

Commit
3 years ago
feat(algebra/ring/basic): add `no_zero_divisors.to_cancel_comm_monoid_with_zero` (#14302) This already existed as `is_domain.to_cancel_comm_monoid_with_zero` with overly strong assumptions.
Author
Parents
Loading