Theorem units.coe_inv
Modification history
2022-08-25 00:16
src/algebra/group/units.lean
feat(algebra/group_with_zero): add `eq_on_inv₀` (#16222) …
Modified units.coe_invView on Github →2022-05-16 11:34
src/algebra/hom/equiv.lean
refactor(algebra/hom/group): Generalize `map_inv` to division monoids (#14134) …
Modified units.coe_invView on Github →2022-01-05 23:45
src/data/equiv/mul_add.lean
chore(*): notation for `units` (#11236)
Modified units.coe_invView on Github →2021-07-31 21:11
src/algebra/group/units.lean
feat(data/equiv/mul_add): add `units.coe_inv` (#8477) …
Modified units.coe_invView on Github →2020-05-06 16:31
src/algebra/group/units.lean
feat(algebra/units): some norm_cast attributes (#2612)
Modified units.coe_invView on Github →2020-03-06 19:21
src/algebra/group/units.lean
refactor(group_theory/monoid_localization): use characteristic predicate (#2004) …
Modified units.coe_invView on Github →