classNumber_pos

Mathlib.NumberTheory.NumberField.ClassNumber

URI: https://scilib.ai/kg/mathlib#NumberField.classNumber_pos

English

Let K be a number field. The class number of K is a positive integer: there holds 0 < classNumber(K).

Русский

Пусть K — число поле. Число класса K является положительным целым числом: 0 < classNumber(K).

LaTeX

$$$0 < \mathrm{classNumber}(K)$$$

Lean4

theorem classNumber_pos : 0 < classNumber K :=
  Fintype.card_pos

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

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

Разделы

Аффилиация

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