instFiniteInt

Mathlib.RingTheory.Finiteness.Finsupp

URI: https://scilib.ai/kg/mathlib#FreeAbelianGroup.instFiniteInt

English

If σ is finite, then the FreeAbelianGroup σ is finitely generated as a module over ℤ.

Русский

Если σ конечно, то FreeAbelianGroup σ порождается как модуль над ℤ.

LaTeX

$$Module.Finite Int (FreeAbelianGroup σ)$$

Lean4

instance : Module.Finite ℤ (FreeAbelianGroup σ) :=
  .of_surjective _ (FreeAbelianGroup.equivFinsupp σ).toIntLinearEquiv.symm.surjective

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

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

Разделы

Аффилиация

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