Mathlib v3 is deprecated. Go to Mathlib v4

Theorem is_unit.mk0

Modification history

2022-10-09 11:15
src/algebra/group_with_zero/basic.lean
chore(algebra/group_with_zero/basic): split into two files (#16866)
Modified is_unit.mk0View on Github →
2021-03-26 18:26
src/algebra/group_with_zero/basic.lean
chore(algebra/group): rename `is_unit_unit` to `units.is_unit` (#6886)
Modified is_unit.mk0View on Github →
2020-04-30 18:20
src/algebra/associated.lean
feat(*): small additions that prepare for Chevalley-Warning (#2560) …
Modified is_unit.mk0View on Github →
2019-08-15 05:08
src/algebra/associated.lean
chore(*): migrate `units.map` to bundled homs (#1331)
Added is_unit.mk0View on Github →