mathlib

4c2edb00 - feat(data/equiv/mul_add): add `units.coe_inv` (#8477)

feat(data/equiv/mul_add): add `units.coe_inv` (#8477) * rename old `units.coe_inv` to `units.coe_inv''`; * add new `@[simp, norm_cast, to_additive] lemma units.coe_inv` about coercion of units of a group; * add missing `coe_to_units`.