classNumber_eq_one_iff — Mathlib

English

Let K be a number field. The class number equals 1 if and only if the ring of integers 𝓞_K is a Principal Ideal Ring (PID).

Русский

Пусть K — число поле. Число класса K равно 1 тогда и только тогда, когда кольцо целых 𝓞_K является кольцом главных идеалов (ПИД).

LaTeX

$$$\mathrm{classNumber}(K) = 1 \;\iff\; \mathrm{IsPrincipalIdealRing}(\mathcal{O}_K)$$$

Lean4

/-- The class number of a number field is `1` iff the ring of integers is a PID. -/
theorem classNumber_eq_one_iff : classNumber K = 1 ↔ IsPrincipalIdealRing (𝓞 K) :=
  card_classGroup_eq_one_iff

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