Commit 2022-01-12 07:31 72c86c3f

chore(algebra/ring/basic): generalize is_domain.to_cancel_monoid_with_zero to no_zero_divisors (#11387) This generalization doesn't work for typeclass search as cancel_monoid_with_zero implies no_zero_divisors which would form a loop, but it can be useful for a letI in another proof. Independent of whether this turns out to be useful, it's nice to show that nontriviality doesn't affect the fact that rings with no zero divisors are cancellative.