Cyclotomic fields whose ring of integers is a PID.

We prove that ℤ [ζₚ] is a PID for specific values of p. The result holds for p ≤ 19, but the proof is more and more involved.

Main results

• three_pid: If IsCyclotomicExtension {3} ℚ K then 𝓞 K is a principal ideal domain.
• five_pid: If IsCyclotomicExtension {5} ℚ K then 𝓞 K is a principal ideal domain.

theorem IsCyclotomicExtension.Rat.three_pid (K : Type u) [Field K] [NumberField K] [IsCyclotomicExtension {3} ℚ K] : IsPrincipalIdealRing (NumberField.RingOfIntegers K)

If IsCyclotomicExtension {3} ℚ K then 𝓞 K is a principal ideal domain.

theorem IsCyclotomicExtension.Rat.five_pid (K : Type u) [Field K] [NumberField K] [IsCyclotomicExtension {5} ℚ K] : IsPrincipalIdealRing (NumberField.RingOfIntegers K)

If IsCyclotomicExtension {5} ℚ K then 𝓞 K is a principal ideal domain.