Def AddMonoidAlgebra.toMultiplicativeBialgEquiv

Modification history

2026-07-23 16:42

Mathlib/RingTheory/Bialgebra/MonoidAlgebra.lean

feat(RingTheory/MonoidAlgebra): `toAdditive` as a `BialgEquiv` (#41413) …

Added AddMonoidAlgebra.toMultiplicativeBialgEquiv View on Github →