English
For any fractional ideal I in 𝓞_K, there exists a nonzero a ∈ I with |N_Q(a)| bounded by absNorm(I) times a Minkowski-type factor times sqrt(|discr(K)|).
Русский
Для любого дробного идеала I в 𝓞_K существует не нулевой элемент a ∈ I, удовлетворяющий неравенству на |N_Q(a)|, выражаемому через absNorm(I) и дискриминант.
LaTeX
$$$\exists a \in I,\ a \neq 0 \land |\mathrm{Algebra.norm}_{\mathbb{Q}}(a)| \\le \, \mathrm{absNorm}(I) \cdot (4/\pi)^{nrComplexPlaces(K)} \cdot \dfrac{(\mathrm{finrank}\mathbb{Q}K)!.}{(\mathrm{finrank}\mathbb{Q}K)^{\mathrm{finrank}\mathbb{Q}K}} \cdot \sqrt{|\mathrm{discr}(K)|}$$$
Lean4
theorem classNumber_eq : NumberField.classNumber ℚ = 1 :=
classNumber_eq_one_iff.mpr <|
IsPrincipalIdealRing.of_surjective Rat.ringOfIntegersEquiv.symm Rat.ringOfIntegersEquiv.symm.surjective
