mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

Make `to_ring_hom_eq_coe` into a `simp` lemma in `ring_equiv`

Open mcdoll opened this issue 3 years ago • 0 comments

Right now to_ring_hom_eq_coe is not a simp lemma, which makes it not possible to deduce something like (f : R ≃+* S) : ⇑(f.to_ring_hom) = ⇑f by simp. The open question is whether f.to_ring_hom or ↑f should be simp-normal-form.

This came up in this thread in zulip

mcdoll avatar Jan 02 '22 14:01 mcdoll