basic): all non-zero elements in a non-trivial ring with no non-zero zero divisors are regular (#12947)

Commit

3 years ago

feat(algebra/ring/basic): all non-zero elements in a non-trivial ring with no non-zero zero divisors are regular (#12947) Besides what the PR description says, I also golfed two earlier proofs.

Author

adomani

Parents

b30f25ce

mathlib3 e63e3322 - feat(algebra/ring/basic): all non-zero elements in a non-trivial ring with no non-zero zero divisors are regular (#12947)

mathlib3
e63e3322 - feat(algebra/ring/basic): all non-zero elements in a non-trivial ring with no non-zero zero divisors are regular (#12947)