flt5_kummer_coprime_beta_form

Disproved

by tianyipeng · May 14, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

graph-theorynumber-theoryopen-problem

Preamble

import Mathlib.NumberTheory.NumberField.Cyclotomic.PID
import Mathlib.NumberTheory.Cyclotomic.Basic
import Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
import Mathlib.RingTheory.PrincipalIdealDomain
import Mathlib.NumberTheory.NumberField.Basic
import Mathlib.Data.Int.Basic
import Mathlib.Data.Int.GCD

Formal statement

theorem flt5_kummer_coprime_beta_form (a b : ℤ) (h_cop : Int.gcd a b = 1) (ζ : NumberField.RingOfIntegers (CyclotomicField 5 ℚ)) (hζ : IsPrimitiveRoot (ζ : CyclotomicField 5 ℚ) 5) (β : NumberField.RingOfIntegers (CyclotomicField 5 ℚ)) (hβ_form : β = ↑a + ↑b * ζ) (hPID : IsPrincipalIdealRing (NumberField.RingOfIntegers (CyclotomicField 5 ℚ))) : ∀ σ : CyclotomicField 5 ℚ ≃ₐ[ℚ] CyclotomicField 5 ℚ, σ ≠ AlgEquiv.refl → IsCoprime β (NumberField.RingOfIntegers.mapAlgEquiv σ β) := by sorry

View graph