mathlib3

72c86c3f - chore(algebra/ring/basic): generalize `is_domain.to_cancel_monoid_with_zero` to `no_zero_divisors` (#11387)

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.