Mathlib v3 is deprecated. Go to Mathlib v4

Theorem is_regular_iff_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_iff_ne_zero'View on Github →
2022-04-26 02:57
src/algebra/ring/basic.lean
feat(algebra/ring/basic): define non-unital commutative (semi)rings (#13476) …
Modified is_regular_iff_ne_zero'View on Github →
2022-03-26 21:16
src/algebra/ring/basic.lean
feat(algebra/ring/basic): all non-zero elements in a non-trivial ring with no non-zero zero divisors are regular (#12947) …
Added is_regular_iff_ne_zero'View on Github →