classNumber

Mathlib.NumberTheory.NumberField.ClassNumber

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

← MathLib Explorer

English

The class number is nonzero.

Русский

Класс число не равно нулю.

LaTeX

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

Lean4

/-- The class number of a number field is the (finite) cardinality of the class group. -/
noncomputable def classNumber : ℕ :=
  Fintype.card (ClassGroup (𝓞 K))

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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