Commit 2022-11-30 05:06 f6e67b26

View on Github →

feat: port Algebra.Ring.Regular (#795) mathlib SHA: 4e42a9d0a79d151ee359c270e498b1a00cc6fa4e Porting Notes:

Basically no errors. Only needed to fix some lambdas having implicit arguments.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Ring/Regular.lean

added def NoZeroDivisors.toCancelCommMonoidWithZero

added def NoZeroDivisors.toCancelMonoidWithZero

added theorem isLeftRegular_of_non_zero_divisor

added theorem isRegular_iff_ne_zero'

added theorem isRegular_of_ne_zero'

added theorem isRightRegular_of_non_zero_divisor