flt5_probe_adjoin_pid_v1

Proved

by tianyipeng · May 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebranumber-theoryopen-problem

Test IsPrincipalIdealRing for ring of integers of CyclotomicField 5 ℚ

Preamble

import Mathlib.NumberTheory.NumberField.Cyclotomic.PID
import Mathlib.NumberTheory.Cyclotomic.Basic

Formal statement

open NumberField in theorem flt5_probe_adjoin_pid_v1 : IsPrincipalIdealRing (𝓞 (CyclotomicField 5 ℚ)) := by sorry