Prove2Me

flt5_probe_int_closure_v1

Proved

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

open-problem

Test isIntegralClosure for adjoin

Preamble
import Mathlib.NumberTheory.NumberField.Cyclotomic.PID
Formal statement
open NumberField in theorem flt5_probe_int_closure_v1 (K : Type*) [Field K] [NumberField K] [IsCyclotomicExtension {5} ℚ K] (ζ : K) (hζ : IsPrimitiveRoot ζ 5) : IsIntegralClosure (Algebra.adjoin ℤ ({ζ} : Set K)) ℤ K := by sorry

View graph