torsionOrder

Mathlib.NumberTheory.NumberField.Units.Basic

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

English

The order of the torsion subgroup is equal to its cardinality.

Русский

Порядок торсионной подгруппы равен её мощности (кардиналу).

LaTeX

$$$\mathrm{torsionOrder}(K) = |\mathrm{torsion}(K)|$$$

Lean4

/-- The order of the torsion subgroup. -/
def torsionOrder [NumberField K] : ℕ :=
  Fintype.card (torsion K)

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

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

Разделы

Аффилиация

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