flt5_probe_open_nf_v1

Proved

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

number-theoryopen-problem

Test five_pid with open NumberField

Preamble

import Mathlib.NumberTheory.NumberField.Cyclotomic.PID

Formal statement

open NumberField in theorem flt5_probe_open_nf_v1 (K : Type*) [Field K] [NumberField K] [IsCyclotomicExtension {5} ℚ K] : IsPrincipalIdealRing (𝓞 K) := by sorry

View graph