instAddCommGroupAsModuleFinsuppFree

English

There is a canonical additive-commutative-group structure on the free k[G]-module on α, inherited as a module via Finsupp on α with MonoidAlgebra k G as base ring; this endows Representation.free k G α with the expected AddCommGroupAsModule structure.

Русский

Существует естественное структуру аддитивной коммутативной группы на свободном k[G]-модуле на α, совместимая с базовым кольцом MonoidAlgebra k G; это задаёт нужное AddCommGroupAsModule на Representation.free k G α.

LaTeX

$$$\\text{AddCommGroup}((\\text{Representation.free } k G α).asModule)$$$

Lean4

noncomputable instance (k G : Type*) [CommRing k] [Monoid G] (α : Type*) : AddCommGroup (free k G α).asModule :=
  Finsupp.instAddCommGroup

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