instIsCyclicSubtypeUnitsRingOfIntegersMemSubgroupTorsion

Mathlib.NumberTheory.NumberField.Units.Basic

URI: https://scilib.ai/kg/mathlib#NumberField.Units.instIsCyclicSubtypeUnitsRingOfIntegersMemSubgroupTorsion

English

For any number field K, the torsion subgroup of the units is cyclic.

Русский

Для любого числа поля K торсионная подгруппа единиц циклична.

LaTeX

$$$\exists n \in \mathbb{N},\; \mathrm{torsion}(K)\;\cong\; \mathbb{Z}/n\mathbb{Z}$$$

Lean4

/-- The torsion subgroup is cyclic. -/
instance : IsCyclic (torsion K) :=
  subgroup_units_cyclic _

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

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

Разделы

Аффилиация

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