flt5_zz5_beta_fifth_power

Disproved

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

algebragraph-theorynumber-theoryopen-problem

In ZZ5 = Z[ζ₅] (a PID), given β:ZZ5 with N(β)=s^5 and gcd(a,b)=1, there exists a unit u:ZZ5ˣ and d:ZZ5 such that β = (u:ZZ5)d^5. This is the Kummer-PID argument: β is coprime to its Galois conjugates β₂,...,β₄ (from gcd(a,b)=1), and in a PID, pairwise coprime elements whose product is a 5th power are individually 5th powers up to unit. So β = ud^5 for some unit u.

Preamble

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

Formal statement

theorem flt5_zz5_beta_fifth_power (a b s : ℤ) (h_cop : Int.gcd a b = 1) (β : NumberField.RingOfIntegers (CyclotomicField 5 ℚ)) (hβ : Algebra.norm ℤ β = s ^ 5) (hPID : IsPrincipalIdealRing (NumberField.RingOfIntegers (CyclotomicField 5 ℚ))) : ∃ (u : (NumberField.RingOfIntegers (CyclotomicField 5 ℚ))ˣ) (d : NumberField.RingOfIntegers (CyclotomicField 5 ℚ)), β = (u : NumberField.RingOfIntegers (CyclotomicField 5 ℚ)) * d ^ 5 := by sorry

View graph