Commit 2021-03-05 00:23 d2cc044f

chore(algebra/algebra/basic): add a missing coe lemma (#6535) This is just to stop the terrible pain of having to work with ⇑(e.to_ring_equiv) x in goals. In the long run, we should sort out the simp normal form, but for now I just want to stop the pain.