mathlib3

7aa85c2b - fix(algebra/group/units): add missing coe lemmas to units (#3472)

fix(algebra/group/units): add missing coe lemmas to units (#3472) Per @kbuzzard's suggestions [here](https://leanprover-community.github.io/archive/stream/113489-new-members/topic/Shortening.20proof.20on.20product.20of.20units.20in.20Z.html#204406319): - Add a new lemma `coe_eq_one` to `units` API - Tag `eq_iff` with `norm_cast` Co-authored-by: Johan Commelin <johan@commelin.net>