Mathlib v3 is deprecated. Go to Mathlib v4

Theorem units.coe_inv''

Modification history

2021-08-09 13:47
src/algebra/group/units.lean
chore(algebra/group/units): Make coercion the simp-normal form of units (#8568) …
Deleted units.coe_inv''View on Github →
2021-07-31 21:11
src/algebra/group/units.lean
feat(data/equiv/mul_add): add `units.coe_inv` (#8477) …
Added units.coe_inv''View on Github →