Mathlib v3 is deprecated. Go to Mathlib v4

Theorem units.coe_eq_one

Modification history

2022-01-05 23:45
src/algebra/group/units.lean
chore(*): notation for `units` (#11236)
Modified units.coe_eq_oneView on Github →
2020-07-20 18:42
src/algebra/group/units.lean
fix(algebra/group/units): add missing coe lemmas to units (#3472) …
Added units.coe_eq_oneView on Github →