Commit 2022-05-22 23:41 9e9a2c9e
View on Github →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.
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.