Inverse conversion between additive and multiplicative monoid algebras

The inverses of Mathlib's algebra and bialgebra equivalences induced by Multiplicative send a monomial at m to the monomial at m.toAdd, with the same coefficient.

@[simp]

theorem AddMonoidAlgebra.toMultiplicativeAlgEquiv_symm_single {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [Semiring A] [AddMonoid M] [Algebra R A] (m : Multiplicative M) (a : A) : (toMultiplicativeAlgEquiv R A M).symm (MonoidAlgebra.single m a) = single (Multiplicative.toAdd m) a

The inverse algebra equivalence induced by Multiplicative preserves monomials.

@[simp]

theorem AddMonoidAlgebra.toMultiplicativeBialgEquiv_symm_single {R : Type u_1} {A : Type u_2} {M : Type u_3} [CommSemiring R] [Semiring A] [AddMonoid M] [Bialgebra R A] (m : Multiplicative M) (a : A) : (toMultiplicativeBialgEquiv R A M).symm (MonoidAlgebra.single m a) = single (Multiplicative.toAdd m) a

The inverse bialgebra equivalence induced by Multiplicative preserves monomials.