English
If {5} is the cyclotomic extension over ℚ for K, then 𝓞K is a principal ideal domain.
Русский
Если {5} образует циклотомическое расширение над ℚ для K, то 𝓞K является PID.
LaTeX
$$$\text{IsCyclotomicExtension} \{5\} \,\mathbb{Q} \,K \Rightarrow \mathcal{O}_K \text{ is a PID}$$$
Lean4
/-- If `IsCyclotomicExtension {5} ℚ K` then `𝓞 K` is a principal ideal domain. -/
theorem five_pid [IsCyclotomicExtension { 5 } ℚ K] : IsPrincipalIdealRing (𝓞 K) :=
by
have : Fact (Nat.Prime 5) := ⟨Nat.prime_five⟩
apply RingOfIntegers.isPrincipalIdealRing_of_abs_discr_lt
rw [absdiscr_prime 5 K, IsCyclotomicExtension.finrank (n := 5) K (irreducible_rat (by simp)),
nrComplexPlaces_eq_totient_div_two 5, totient_prime Nat.prime_five]
simp only [Int.reduceNeg, succ_sub_succ_eq_sub, tsub_zero, reduceDiv, even_two, Even.neg_pow, one_pow, cast_ofNat,
Int.reducePow, one_mul, Int.cast_abs, Int.cast_ofNat, abs_of_pos (show (0 : ℝ) < 125 by simp), div_pow,
show 4! = 24 by rfl]
suffices (2 * (3 ^ 2 / 4 ^ 2) * (4 ^ 4 / 24)) ^ 2 < (2 * (π ^ 2 / 4 ^ 2) * (4 ^ 4 / 24)) ^ 2 from
lt_trans (by norm_num) this
gcongr
exact pi_gt_three
