English
If {3} is the cyclotomic set over ℚ for K, then the ring of integers 𝓞K is a principal ideal domain.
Русский
Если 3 образует циклотомическое расширение над ℚ для K, то кольцо целых 𝓞K является основным идеальным кольцом.
LaTeX
$$$\text{IsCyclotomicExtension} \{3\} \mathbb{Q} K \Rightarrow \mathcal{O}_K \,\text{is a PID}$$$
Lean4
/-- If `IsCyclotomicExtension {3} ℚ K` then `𝓞 K` is a principal ideal domain. -/
theorem three_pid [IsCyclotomicExtension { 3 } ℚ K] : IsPrincipalIdealRing (𝓞 K) :=
by
apply RingOfIntegers.isPrincipalIdealRing_of_abs_discr_lt
rw [absdiscr_prime 3 K, IsCyclotomicExtension.finrank (n := 3) K (irreducible_rat (by simp)),
nrComplexPlaces_eq_totient_div_two 3, totient_prime Nat.prime_three]
simp only [Int.reduceNeg, succ_sub_succ_eq_sub, tsub_zero, zero_lt_two, Nat.div_self, pow_one, cast_ofNat, neg_mul,
one_mul, abs_neg, Int.cast_abs, Int.cast_ofNat, abs_of_pos (zero_lt_three' ℝ), factorial_two]
suffices (2 * (3 / 4) * (2 ^ 2 / 2)) ^ 2 < (2 * (π / 4) * (2 ^ 2 / 2)) ^ 2 from lt_trans (by norm_num) this
gcongr
exact pi_gt_three
