Theorem AddMonoidAlgebra.toMultiplicativeBialgEquiv_single

Modification history

2026-07-23 16:42
Mathlib/RingTheory/Bialgebra/MonoidAlgebra.lean
feat(RingTheory/MonoidAlgebra): `toAdditive` as a `BialgEquiv` (#41413) …
Added AddMonoidAlgebra.toMultiplicativeBialgEquiv_singleView on Github →