feat(ring_theory): non-zero divisors are not zero (#9043)
feat(ring_theory): non-zero divisors are not zero (#9043)

I'm kind of suprised we didn't have this before!





leanprover-community/mathlib,leanprover-community/mathlib