toAdditiveAlgEquiv — Mathlib

English

There is an algebra equivalence between MonoidAlgebra k G and AddMonoidAlgebra k (Additive G) that expresses MonoidAlgebra in additive form.

Русский

Существует алгебраическое эквивалентное отображение между MonoidAlgebra k G и AddMonoidAlgebra k (Additive G) в аддитивной форме.

LaTeX

$$$\\text{toAdditiveAlgEquiv} : MonoidAlgebra\\, k\\, G \\simeq_A\\, AddMonoidAlgebra\\, k\\, (Additive\\, G).$$$

Lean4

/-- The algebra equivalence between `MonoidAlgebra` and `AddMonoidAlgebra` in terms of
`Additive`. -/
def toAdditiveAlgEquiv [Semiring k] [Algebra R k] [Monoid G] :
    MonoidAlgebra k G ≃ₐ[R] AddMonoidAlgebra k (Additive G) :=
  { MonoidAlgebra.toAdditive k G with commutes' := fun r => by simp [MonoidAlgebra.toAdditive] }

Похожие утверждения