Def BialgHom.ofAlgHom

Modification history

2025-08-21 10:17

Mathlib/RingTheory/Bialgebra/Hom.lean

refactor: state hypotheses of `BialgHom.ofAlgHom` as equalities of `AlgHom`s (#28142) …

Modified BialgHom.ofAlgHom View on Github →

2025-04-23 09:49

Mathlib/RingTheory/Bialgebra/Hom.lean

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

Added BialgHom.ofAlgHom View on Github →