Commit 2024-05-22 09:49 5acadee4

View on Github →

chore(Algebra/Category/Ring): simp lemmas for coercions (#13108) We add more simp lemmas to handle situations where both X →+* Y and CommRingCat.of X ⟶ CommRingCat.of Y appear, due to partial unfolding of this defeq. This appears to make things more confluent (the payoff isn't in this PR, however). If this turns out well, I will install corresponding lemmas in the other concrete categories in a later PR.

Estimated changes

added theorem CommRingCat.coe_id_of
added theorem CommRingCat.ext_of
added theorem CommSemiRingCat.ext_of
added theorem RingCat.coe_comp_of
added theorem RingCat.coe_id_of
added theorem RingCat.coe_ringHom_id
added theorem RingCat.ext_of
added theorem SemiRingCat.coe_id_of
added theorem SemiRingCat.ext_of