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.
