Commit 2026-01-01 18:05 d3acd13a

View on Github →

chore(RingTheory/Bialgebra/MonoidAlgebra): use to_additive (#33452)

Estimated changes

Modified Mathlib/RingTheory/Bialgebra/MonoidAlgebra.lean

deleted theorem AddMonoidAlgebra.mapDomainBialgHom_comp

deleted theorem AddMonoidAlgebra.mapDomainBialgHom_id

deleted theorem AddMonoidAlgebra.mapDomainBialgHom_mapDomainBialgHom

modified theorem MonoidAlgebra.mapDomainBialgHom_id

Modified Mathlib/RingTheory/HopfAlgebra/MonoidAlgebra.lean

deleted theorem AddMonoidAlgebra.antipode_single