mathlib3

84d64972 - fix(algebra/ring): add coe_neg_one lemma to units (#3489)

fix(algebra/ring): add coe_neg_one lemma to units (#3489) Follow up to #3472 - adds `coe_neg_one`, which allows `norm_cast` to handle hypotheses like `↑-1 = 1`