mathlib3

80b699bc - chore(ring_theory): generalize `non_zero_divisors` lemmas to `monoid_with_zero` (#8607)

chore(ring_theory): generalize `non_zero_divisors` lemmas to `monoid_with_zero` (#8607) None of the results about `non_zero_divisors` needed a ring structure, just a `monoid_with_zero`. So the generalization is obvious. Shall we move this file to the `algebra` namespace sometime soon?