instAddCommGroup

Mathlib.RepresentationTheory.Coinvariants

URI: https://scilib.ai/kg/mathlib#Representation.Coinvariants.instAddCommGroup

English

The coinvariants ρ.Coinvariants carry a natural AddCommGroup structure.

Русский

Коинварианты ρ.Coinvariants естественным образом образуют структуру добавочно-коммутативной группы.

LaTeX

$$$\rho.\mathrm{Coinvariants}$ is an additive commutative group$$

Lean4

instance : AddCommGroup (Coinvariants ρ) :=
  inferInstanceAs <| AddCommGroup (_ ⧸ _)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru