mathlib3
79be90a7 - feat(algebra/regular): add lemmas about regularity of non-zero elements (#6579)

Commit

4 years ago

feat(algebra/regular): add lemmas about regularity of non-zero elements (#6579) More API, to deal with cases in which a regular element is non-zero.

Author

adomani

Parents