Commit 2025-04-23 09:49 e9feb085

View on Github →

feat(Bialgebra/MonoidAlgebra): mapDomain as a BialgHom (#23722) From Toric

Estimated changes

Modified Mathlib/RingTheory/Bialgebra/Hom.lean

added def BialgHom.ofAlgHom

Modified Mathlib/RingTheory/Bialgebra/MonoidAlgebra.lean

added theorem AddMonoidAlgebra.mapDomainBialgHom_comp

added theorem AddMonoidAlgebra.mapDomainBialgHom_id

added theorem AddMonoidAlgebra.mapDomainBialgHom_mapDomainBialgHom

added theorem MonoidAlgebra.mapDomainBialgHom_comp

added theorem MonoidAlgebra.mapDomainBialgHom_id

added theorem MonoidAlgebra.mapDomainBialgHom_mapDomainBialgHom