Mathlib v3 is deprecated. Go to Mathlib v4

Def unit_of_invertible

Modification history

2022-01-05 23:45
src/algebra/invertible.lean
chore(*): notation for `units` (#11236)
Modified unit_of_invertibleView on Github →
2020-07-21 21:58
src/algebra/invertible.lean
feat(algebra/invertible): invertible elements are units (#3499)
Added unit_of_invertibleView on Github →