Mathlib v3 is deprecated. Go to Mathlib v4

Theorem units.is_regular

Modification history

2022-01-05 23:45
src/algebra/regular/basic.lean
chore(*): notation for `units` (#11236)
Modified units.is_regularView on Github →
2021-02-20 17:42
src/algebra/regular.lean
feat(algebra/regular): define regular elements (#6282) …
Added units.is_regularView on Github →