Theorem MonoidAlgebra.mapDomainBialgHom_id

Modification history

2026-01-01 18:05
Mathlib/RingTheory/Bialgebra/MonoidAlgebra.lean
chore(RingTheory/Bialgebra/MonoidAlgebra): use `to_additive` (#33452)
Modified MonoidAlgebra.mapDomainBialgHom_idView on Github →
2025-12-08 07:46
Mathlib/RingTheory/Bialgebra/MonoidAlgebra.lean
feat(Algebra/MonoidAlgebra): extend the `R[M]` notation to `MonoidAlgebra R M` (#30877) …
Modified MonoidAlgebra.mapDomainBialgHom_idView on Github →
2025-04-23 09:49
Mathlib/RingTheory/Bialgebra/MonoidAlgebra.lean
feat(Bialgebra/MonoidAlgebra): `mapDomain` as a `BialgHom` (#23722) …
Added MonoidAlgebra.mapDomainBialgHom_idView on Github →