Commit 2022-03-26 21:16 e63e3322
View on Github →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.
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.