Prove2Me

flt5_probe_cyc_instances_v1

Proved

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

open-problem

Test with all three cyclotomic imports

Preamble
import Mathlib.NumberTheory.NumberField.Cyclotomic.PID
import Mathlib.NumberTheory.Cyclotomic.Basic
import Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
Formal statement
open NumberField in theorem flt5_probe_cyc_instances_v1 : IsPrincipalIdealRing (𝓞 (CyclotomicField 5 ℚ)) := by sorry

View graph