English
In the ring of integers, if a certain norm-bound condition holds for principal ideals over primes within a Minkowski-like interval, then the ring is a PID.
Русский
В кольце целых, если выполняется определённое ограничение по норме для идеалов над простыми внутри интервала Минковского, то кольцо является ПИД.
LaTeX
$$$\forall p,\ p\in \mathrm{Icc}\;1\;\big\lfloor M(K) \big\rfloor_+ \Rightarrow \exists P \in \mathrm{primesOver}(\mathrm{span}\{p\})\, (\mathcal{O}_K): \ text{...} \Rightarrow \mathrm{IsPrincipalIdealRing}(\mathcal{O}_K)$$$
Lean4
/-- **Dirichlet class number formula**
-/
theorem tendsto_sub_one_mul_dedekindZeta_nhdsGT :
Tendsto (fun s : ℝ ↦ (s - 1) * dedekindZeta K s) (𝓝[>] 1) (𝓝 (dedekindZeta_residue K)) :=
by
refine LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div_and_nonneg _ ?_ (fun _ ↦ Nat.cast_nonneg _)
refine ((Ideal.tendsto_norm_le_div_atTop₀ K).comp tendsto_natCast_atTop_atTop).congr fun n ↦ ?_
simp only [Function.comp_apply, Nat.cast_le, ← Nat.cast_sum]
congr
rw [← add_left_inj 1, ← card_norm_le_eq_card_norm_le_add_one,
show Finset.Icc 1 n = Finset.Ioc 0 n from Finset.Icc_succ_left_eq_Ioc _ _,
show 1 = Nat.card { I : Ideal (𝓞 K) // absNorm I = 0 } by simp [Ideal.absNorm_eq_zero_iff],
Finset.sum_Ioc_add_eq_sum_Icc (n.zero_le), ←
Finset.card_preimage_eq_sum_card_image_eq (fun k _ ↦ finite_setOf_absNorm_eq k)]
simp [Set.coe_eq_subtype]
