instNeZeroNatTorsionOrder

Mathlib.NumberTheory.NumberField.Units.Basic

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

English

The torsion order is nonzero (there exists a torsion subgroup).

Русский

Порядок торсионной подгруппы отличен от нуля.

LaTeX

$$$\mathrm{torsionOrder}(K) \neq 0$$$

Lean4

instance [NumberField K] : NeZero (torsionOrder K) :=
  inferInstanceAs (NeZero (Fintype.card (torsion K)))

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

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

Разделы

Аффилиация

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