Mathlib v3 is deprecated. Go to Mathlib v4

Theorem units.mk_coe

Modification history

2022-01-05 23:45
src/algebra/group/units.lean
chore(*): notation for `units` (#11236)
Modified units.mk_coeView on Github →
2021-01-05 20:33
src/algebra/group/units.lean
fix(algebra/group/prod): fixes for #5563 (#5577) …
Added units.mk_coeView on Github →