instFGInt

Mathlib.GroupTheory.Finiteness

URI: https://scilib.ai/kg/mathlib#AddGroup.instFGInt

English

The additive group of integers is finitely generated (by 1).

Русский

Целочисленная аддитивная группа FG порождается единицей.

LaTeX

$$$\mathbb{Z}$ (as AddGroup) is FG$$

Lean4

instance : FG ℤ where out := ⟨{ 1 }, by simp⟩

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

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

Разделы

Аффилиация

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