classNumber — Mathlib

English

The class number is 1 if and only if the ring of integers is a principal ideal ring.

Русский

Число класса равно 1 тогда и только тогда, когда кольцо целых чисел является кольцом главных идеалов.

LaTeX

$$classNumber Fq F = 1 \\iff IsPrincipalIdealRing (ringOfIntegers Fq F)$$

Lean4

/-- The class number in a function field is the (finite) cardinality of the class group. -/
noncomputable def classNumber : ℕ :=
  Fintype.card (ClassGroup (ringOfIntegers Fq F))

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