Theorem AddMonoidAlgebra.mapDomainBialgHom_id

Modification history

2026-01-01 18:05

Mathlib/RingTheory/Bialgebra/MonoidAlgebra.lean

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

Deleted AddMonoidAlgebra.mapDomainBialgHom_id View on Github →

2025-04-23 09:49

Mathlib/RingTheory/Bialgebra/MonoidAlgebra.lean

feat(Bialgebra/MonoidAlgebra): `mapDomain` as a `BialgHom` (#23722) …

Added AddMonoidAlgebra.mapDomainBialgHom_id View on Github →