Mathlib v3 is deprecated. Go to Mathlib v4

Def equiv.units_equiv_ne_zero

Modification history

2021-10-23 17:11
src/data/equiv/ring.lean
chore(data/fintype/basic): make units.fintype computable (#9846) …
Deleted equiv.units_equiv_ne_zeroView on Github →
2020-03-14 17:09
src/data/equiv/algebra.lean
refactor(data/equiv/algebra): split (#2147) …
Modified equiv.units_equiv_ne_zeroView on Github →
2019-09-27 07:02
src/data/equiv/algebra.lean
chore(*): drop some unused args reported by `#sanity_check_mathlib` (#1490) …
Modified equiv.units_equiv_ne_zeroView on Github →
2018-11-05 10:08
data/equiv/algebra.lean
refactor(field_theory/finite): generalize proofs (#429)
Added equiv.units_equiv_ne_zeroView on Github →