Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-31 21:11 4c2edb00

View on Github →

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.

Estimated changes

added theorem units.coe_inv''
deleted theorem units.coe_inv
added theorem coe_to_units
modified def to_units
added theorem units.coe_inv