Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-20 18:42 7aa85c2b

View on Github →

fix(algebra/group/units): add missing coe lemmas to units (#3472) Per @kbuzzard's suggestions here:

  • Add a new lemma coe_eq_one to units API
  • Tag eq_iff with norm_cast

Estimated changes

added theorem units.coe_eq_one
added theorem units.eq_iff