Commit 2024-05-14 07:39 c36fe272

View on Github →

feat: bialgebra homomorphisms (#11962) Homomorphisms of bialgebras, mimicking the file Mathlib.Algebra.Algebra.Hom.

Estimated changes

added theorem BialgHom.coe_comp
added theorem BialgHom.coe_copy
added theorem BialgHom.coe_fn_inj
added theorem BialgHom.coe_id
added theorem BialgHom.coe_mk
added theorem BialgHom.coe_mks
added theorem BialgHom.coe_toAlgHom
added def BialgHom.comp
added theorem BialgHom.comp_assoc
added theorem BialgHom.comp_id
added theorem BialgHom.comp_toAlgHom
added theorem BialgHom.copy_eq
added theorem BialgHom.ext
added theorem BialgHom.ext_iff
added theorem BialgHom.ext_of_ring
added theorem BialgHom.id_comp
added theorem BialgHom.id_toAlgHom
added theorem BialgHom.id_toCoalgHom
added theorem BialgHom.mk_coe
added theorem BialgHom.mul_apply
added theorem BialgHom.one_apply
added structure BialgHom
added theorem Bialgebra.ext_to_ring
added theorem CoalgHom.coe_copy
added theorem CoalgHom.copy_eq