addCommGroup — Mathlib

English

The MonoidAlgebra R M carries a natural additive commutative group structure. In particular, MonoidAlgebra R M is an AddCommGroup.

Русский

MonoidAlgebra R M обладает естественной структурой абелевой группы по сложению.

LaTeX

$$$\\mathrm{AddCommGroup}(\\mathrm{MonoidAlgebra}(R,M)).$$$

Lean4

@[to_additive (dont_translate := R)]
instance addCommGroup : AddCommGroup (MonoidAlgebra R M) :=
  inferInstanceAs <| AddCommGroup <| M →₀ R

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