Commit 2024-06-14 14:02 c4806696

View on Github →

chore: generalize some results to non-unital rings (#13807)

Estimated changes

Modified Mathlib/Algebra/GeomSum.lean

Modified Mathlib/Algebra/Order/AbsoluteValue.lean

Modified Mathlib/Algebra/Regular/Basic.lean

Modified Mathlib/Algebra/Ring/Basic.lean

modified theorem IsLeftCancelMulZero.to_noZeroDivisors

modified theorem IsRightCancelMulZero.to_noZeroDivisors

modified theorem isCancelMulZero_iff_noZeroDivisors

Modified Mathlib/Data/Real/NNReal.lean