refactor(algebra/algebra): choose `coe` as the normal form for the map `alg_equiv → ring_equiv` (#9848)
refactor(algebra/algebra): choose `coe` as the normal form for the map `alg_equiv → ring_equiv` (#9848)

We never chose a `simp`-normal form for this map, resulting in some duplicate work and annoying `show _ = _, from rfl` when rewriting. I picked this choice because it matches the convention for the map `alg_hom → ring_hom`.

Very surprisingly, there were absolutely no CI failures due to this choice.





leanprover-community/mathlib,leanprover-community/mathlib