Commit 2026-09-11 08:52 0ef25053

View on Github →

chore: rename Coalg{Hom,Equiv}Class.toCoalg{Hom,Equiv} as Coalg{Hom,Equiv}.ofClass (#43576) and rename affected lemmas accordingly. Following item (2) in https://github.com/leanprover-community/mathlib4/issues/31365, the definition which implements the coercion from a morphism class FooHomClass to FooHoms should be called FooHom.ofClass. This makes two more classes follow this pattern.

Estimated changes

Modified Mathlib/RingTheory/Bialgebra/Hom.lean

Modified Mathlib/RingTheory/Bialgebra/TensorProduct.lean

Modified Mathlib/RingTheory/Coalgebra/Equiv.lean

added theorem CoalgEquiv.coe_coalgHomOfClass

deleted theorem CoalgEquiv.coe_coe

added theorem CoalgEquiv.coe_ofClass

deleted theorem CoalgEquiv.coe_toCoalgHom

added def CoalgEquiv.ofClass

deleted theorem CoalgEquiv.toCoalgHom_eq_coe

added theorem CoalgEquiv.toCoalgHom_eq_ofClass

deleted def CoalgEquivClass.toCoalgEquiv

Modified Mathlib/RingTheory/Coalgebra/GroupLike.lean

Modified Mathlib/RingTheory/Coalgebra/Hom.lean

deleted theorem CoalgHom.coe_fn_inj

deleted theorem CoalgHom.coe_fn_injective

added theorem CoalgHom.coe_inj

added theorem CoalgHom.coe_injective

added theorem CoalgHom.coe_linearMapOfClass

deleted theorem CoalgHom.coe_linearMap_injective

deleted theorem CoalgHom.coe_toLinearMap

added theorem CoalgHom.linearMapOfClass_injective

added def CoalgHom.ofClass

deleted theorem CoalgHom.toLinearMap_eq_coe

added theorem CoalgHom.toLinearMap_eq_ofClass

deleted def CoalgHomClass.toCoalgHom

Modified Mathlib/RingTheory/Coalgebra/Primitive.lean