Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Theorem
is_regular_of_ne_zero'
Modification history
2022-10-09 08:02
src/algebra/ring/basic.lean
chore(algebra/ring/basic): move results about regular elements (#16865)
Modified
is_regular_of_ne_zero'
View on Github →
2022-04-23 22:43
src/algebra/ring/basic.lean
feat(algebra/ring/basic): generalisation linter suggestions (#13649)
Modified
is_regular_of_ne_zero'
View on Github →
2021-08-09 15:47
src/algebra/ring/basic.lean
feat(algebra/ring/basic): mul_{left,right}_cancel_of_non_zero_divisor (#8425) …
Added
is_regular_of_ne_zero'
View on Github →