Mathlib v3 is deprecated. Go to Mathlib v4

Theorem is_unit_iff_ne_zero

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_iff_ne_zeroView on Github →
2022-06-15 14:55
src/algebra/group_with_zero/basic.lean
refactor(algebra/group_with_zero/basic): Golf using division monoid lemmas (#14213) …
Modified is_unit_iff_ne_zeroView on Github →
2020-04-30 18:20
src/algebra/associated.lean
feat(*): small additions that prepare for Chevalley-Warning (#2560) …
Modified is_unit_iff_ne_zeroView on Github →
2020-02-19 21:46
src/algebra/associated.lean
refactor(analysis/calculus/tangent_cone): split a proof into parts (#2013) …
Added is_unit_iff_ne_zeroView on Github →