Mathlib v3 is deprecated. Go to Mathlib v4

Theorem nonempty_invertible_iff_is_unit

Modification history

2022-05-14 10:51
src/algebra/invertible.lean
chore(algebra/invertible): minor golf (#14141)
Modified nonempty_invertible_iff_is_unitView on Github →
2021-07-06 05:05
src/algebra/invertible.lean
feat(algebra/invertible): construction from is_unit (#8205)
Added nonempty_invertible_iff_is_unitView on Github →