Commit 2021-10-23 14:30 2a1f4542

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.