Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-16 16:19 80b699bc

View on Github →

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?

Estimated changes