Commit 2024-04-16 21:10 da617610

View on Github →

feat: coalgebra homomorphisms (#11961) Homomorphisms of coalgebras, mimicking the file Mathlib.Algebra.Algebra.Hom.

Estimated changes

added theorem CoalgHom.coe_comp
added theorem CoalgHom.coe_fn_inj
added theorem CoalgHom.coe_id
added theorem CoalgHom.coe_mk
added theorem CoalgHom.coe_mks
added def CoalgHom.comp
added theorem CoalgHom.comp_assoc
added theorem CoalgHom.comp_id
added theorem CoalgHom.ext
added theorem CoalgHom.ext_iff
added theorem CoalgHom.ext_of_ring
added theorem CoalgHom.id_comp
added theorem CoalgHom.mk_coe
added theorem CoalgHom.mul_apply
added theorem CoalgHom.one_apply
added structure CoalgHom
added theorem Coalgebra.ext_to_ring