internlm/Lean-Github huggingface dataset:
Theorem: FltRegular.is_principal_aux
Proof state before:
case mk.intro.intro
p : ℕ
hpri : Fact p.Prime
K' : Type u_1
inst✝³ : Field K'
inst✝² : CharZero K'
inst✝¹ : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ K'
inst✝ : Fintype (ClassGroup (𝓞 K'))
a b : ℤ
ζ : 𝓞 K'
hreg : p.Coprime (Fintype.card (ClassGroup (𝓞 K')))
I : Ideal (𝓞 K')
hI : span {↑a + ζ * ↑b} = I ^ p
this : NumberField K' := numberField {⟨p, Prime.pos Fact.out⟩} ℚ K'
α : 𝓞 K'
u : (𝓞 K')ˣ
hu : (↑a + ζ * ↑b) * ↑u = α ^ p
⊢ ∃ u α, ↑u * α ^ p = ↑a + ζ * ↑b
Tactic:
refine' ⟨u⁻¹, α, _⟩
Proof state after:
case mk.intro.intro
p : ℕ
hpri : Fact p.Prime
K' : Type u_1
inst✝³ : Field K'
inst✝² : CharZero K'
inst✝¹ : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ K'
inst✝ : Fintype (ClassGroup (𝓞 K'))
a b : ℤ
ζ : 𝓞 K'
hreg : p.Coprime (Fintype.card (ClassGroup (𝓞 K')))
I : Ideal (𝓞 K')
hI : span {↑a + ζ * ↑b} = I ^ p
this : NumberField K' := numberField {⟨p, Prime.pos Fact.out⟩} ℚ K'
α : 𝓞 K'
u : (𝓞 K')ˣ
hu : (↑a + ζ * ↑b) * ↑u = α ^ p
⊢ ↑u⁻¹ * α ^ p = ↑a + ζ * ↑b
Theorem: FltRegular.is_principal_aux
Proof state before:
case mk.intro.intro
p : ℕ
hpri : Fact p.Prime
K' : Type u_1
inst✝³ : Field K'
inst✝² : CharZero K'
inst✝¹ : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ K'
inst✝ : Fintype (ClassGroup (𝓞 K'))
a b : ℤ
ζ : 𝓞 K'
hreg : p.Coprime (Fintype.card (ClassGroup (𝓞 K')))
I : Ideal (𝓞 K')
hI : span {↑a + ζ * ↑b} = I ^ p
this : NumberField K' := numberField {⟨p, Prime.pos Fact.out⟩} ℚ K'
α : 𝓞 K'
u : (𝓞 K')ˣ
hu : (↑a + ζ * ↑b) * ↑u = α ^ p
⊢ ↑u⁻¹ * α ^ p = ↑a + ζ * ↑b
Tactic:
rw [← hu, mul_comm ((_ + ζ * _)), ← mul_assoc]
Proof state after:
case mk.intro.intro
p : ℕ
hpri : Fact p.Prime
K' : Type u_1
inst✝³ : Field K'
inst✝² : CharZero K'
inst✝¹ : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ K'
inst✝ : Fintype (ClassGroup (𝓞 K'))
a b : ℤ
ζ : 𝓞 K'
hreg : p.Coprime (Fintype.card (ClassGroup (𝓞 K')))
I : Ideal (𝓞 K')
hI : span {↑a + ζ * ↑b} = I ^ p
this : NumberField K' := numberField {⟨p, Prime.pos Fact.out⟩} ℚ K'
α : 𝓞 K'
u : (𝓞 K')ˣ
hu : (↑a + ζ * ↑b) * ↑u = α ^ p
⊢ ↑u⁻¹ * ↑u * (↑a + ζ * ↑b) = ↑a + ζ * ↑b
Theorem: FltRegular.is_principal_aux
Proof state before:
case mk.intro.intro
p : ℕ
hpri : Fact p.Prime
K' : Type u_1
inst✝³ : Field K'
inst✝² : CharZero K'
inst✝¹ : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ K'
inst✝ : Fintype (ClassGroup (𝓞 K'))
a b : ℤ
ζ : 𝓞 K'
hreg : p.Coprime (Fintype.card (ClassGroup (𝓞 K')))
I : Ideal (𝓞 K')
hI : span {↑a + ζ * ↑b} = I ^ p
this : NumberField K' := numberField {⟨p, Prime.pos Fact.out⟩} ℚ K'
α : 𝓞 K'
u : (𝓞 K')ˣ
hu : (↑a + ζ * ↑b) * ↑u = α ^ p
⊢ ↑u⁻¹ * ↑u * (↑a + ζ * ↑b) = ↑a + ζ * ↑b
Tactic:
simp only [Units.inv_mul, one_mul]
Proof state after:
no goals
Theorem: FltRegular.is_principal_aux
Proof state before:
p : ℕ
hpri : Fact p.Prime
K' : Type u_1
inst✝³ : Field K'
inst✝² : CharZero K'
inst✝¹ : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ K'
inst✝ : Fintype (ClassGroup (𝓞 K'))
a b : ℤ
ζ : 𝓞 K'
hreg : p.Coprime (Fintype.card (ClassGroup (𝓞 K')))
I : Ideal (𝓞 K')
hI : span {↑a + ζ * ↑b} = I ^ p
this : NumberField K' := numberField {⟨p, Prime.pos Fact.out⟩} ℚ K'
⊢ Submodule.IsPrincipal I
Tactic:
apply IsPrincipal_of_IsPrincipal_pow_of_Coprime (𝓞 K') _ hreg I
Proof state after:
p : ℕ
hpri : Fact p.Prime
K' : Type u_1
inst✝³ : Field K'
inst✝² : CharZero K'
inst✝¹ : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ K'
inst✝ : Fintype (ClassGroup (𝓞 K'))
a b : ℤ
ζ : 𝓞 K'
hreg : p.Coprime (Fintype.card (ClassGroup (𝓞 K')))
I : Ideal (𝓞 K')
hI : span {↑a + ζ * ↑b} = I ^ p
this : NumberField K' := numberField {⟨p, Prime.pos Fact.out⟩} ℚ K'
⊢ Submodule.IsPrincipal (I ^ p)
Theorem: FltRegular.is_principal_aux
Proof state before:
p : ℕ
hpri : Fact p.Prime
K' : Type u_1
inst✝³ : Field K'
inst✝² : CharZero K'
inst✝¹ : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ K'
inst✝ : Fintype (ClassGroup (𝓞 K'))
a b : ℤ
ζ : 𝓞 K'
hreg : p.Coprime (Fintype.card (ClassGroup (𝓞 K')))
I : Ideal (𝓞 K')
hI : span {↑a + ζ * ↑b} = I ^ p
this : NumberField K' := numberField {⟨p, Prime.pos Fact.out⟩} ℚ K'
⊢ Submodule.IsPrincipal (I ^ p)
Tactic:
constructor
Proof state after:
case principal'
p : ℕ
hpri : Fact p.Prime
K' : Type u_1
inst✝³ : Field K'
inst✝² : CharZero K'
inst✝¹ : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ K'
inst✝ : Fintype (ClassGroup (𝓞 K'))
a b : ℤ
ζ : 𝓞 K'
hreg : p.Coprime (Fintype.card (ClassGroup (𝓞 K')))
I : Ideal (𝓞 K')
hI : span {↑a + ζ * ↑b} = I ^ p
this : NumberField K' := numberField {⟨p, Prime.pos Fact.out⟩} ℚ K'
⊢ ∃ a, I ^ p = Submodule.span (𝓞 K') {a}
Theorem: FltRegular.is_principal_aux
Proof state before:
case principal'
p : ℕ
hpri : Fact p.Prime
K' : Type u_1
inst✝³ : Field K'
inst✝² : CharZero K'
inst✝¹ : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ K'
inst✝ : Fintype (ClassGroup (𝓞 K'))
a b : ℤ
ζ : 𝓞 K'
hreg : p.Coprime (Fintype.card (ClassGroup (𝓞 K')))
I : Ideal (𝓞 K')
hI : span {↑a + ζ * ↑b} = I ^ p
this : NumberField K' := numberField {⟨p, Prime.pos Fact.out⟩} ℚ K'
⊢ ∃ a, I ^ p = Submodule.span (𝓞 K') {a}
Tactic:
use ↑a + ζ * ↑b
Proof state after:
case h
p : ℕ
hpri : Fact p.Prime
K' : Type u_1
inst✝³ : Field K'
inst✝² : CharZero K'
inst✝¹ : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ K'
inst✝ : Fintype (ClassGroup (𝓞 K'))
a b : ℤ
ζ : 𝓞 K'
hreg : p.Coprime (Fintype.card (ClassGroup (𝓞 K')))
I : Ideal (𝓞 K')
hI : span {↑a + ζ * ↑b} = I ^ p
this : NumberField K' := numberField {⟨p, Prime.pos Fact.out⟩} ℚ K'
⊢ I ^ p = Submodule.span (𝓞 K') {↑a + ζ * ↑b}
Theorem: FltRegular.is_principal_aux
Proof state before:
case h
p : ℕ
hpri : Fact p.Prime
K' : Type u_1
inst✝³ : Field K'
inst✝² : CharZero K'
inst✝¹ : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ K'
inst✝ : Fintype (ClassGroup (𝓞 K'))
a b : ℤ
ζ : 𝓞 K'
hreg : p.Coprime (Fintype.card (ClassGroup (𝓞 K')))
I : Ideal (𝓞 K')
hI : span {↑a + ζ * ↑b} = I ^ p
this : NumberField K' := numberField {⟨p, Prime.pos Fact.out⟩} ℚ K'
⊢ I ^ p = Submodule.span (𝓞 K') {↑a + ζ * ↑b}
Tactic:
rw [submodule_span_eq, hI]
Proof state after:
no goals
Theorem: FltRegular.is_principal
Proof state before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
hζ : IsPrimitiveRoot ζ p
⊢ ∃ u α, ↑u * α ^ p = ↑a + ζ * ↑b
Tactic:
haveI := CyclotomicField.isCyclotomicExtension P ℚ
Proof state after:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
hζ : IsPrimitiveRoot ζ p
this : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ (CyclotomicField ⟨p, ⋯⟩ ℚ)
⊢ ∃ u α, ↑u * α ^ p = ↑a + ζ * ↑b
Theorem: FltRegular.is_principal
Proof state before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
hζ : IsPrimitiveRoot ζ p
this : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ (CyclotomicField ⟨p, ⋯⟩ ℚ)
⊢ ∃ u α, ↑u * α ^ p = ↑a + ζ * ↑b
Tactic:
replace hζ := hζ.mem_nthRootsFinset hpri.out.pos
Proof state after:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
this : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ (CyclotomicField ⟨p, ⋯⟩ ℚ)
hζ : ζ ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
⊢ ∃ u α, ↑u * α ^ p = ↑a + ζ * ↑b
Theorem: FltRegular.is_principal
Proof state before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
this : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ (CyclotomicField ⟨p, ⋯⟩ ℚ)
hζ : ζ ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
⊢ ∃ u α, ↑u * α ^ p = ↑a + ζ * ↑b
Tactic:
obtain ⟨I, hI⟩ := exists_ideal hp5 H hgcd caseI hζ
Proof state after:
case intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
this : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ (CyclotomicField ⟨p, ⋯⟩ ℚ)
hζ : ζ ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
I : Ideal (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hI : span {↑a + ζ * ↑b} = I ^ p
⊢ ∃ u α, ↑u * α ^ p = ↑a + ζ * ↑b
Theorem: FltRegular.is_principal
Proof state before:
case intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
this : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ (CyclotomicField ⟨p, ⋯⟩ ℚ)
hζ : ζ ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
I : Ideal (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hI : span {↑a + ζ * ↑b} = I ^ p
⊢ ∃ u α, ↑u * α ^ p = ↑a + ζ * ↑b
Tactic:
apply is_principal_aux
Proof state after:
case intro.hreg
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
this : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ (CyclotomicField ⟨p, ⋯⟩ ℚ)
hζ : ζ ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
I : Ideal (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hI : span {↑a + ζ * ↑b} = I ^ p
⊢ p.Coprime (Fintype.card (ClassGroup (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))))

case intro.hI
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
this : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ (CyclotomicField ⟨p, ⋯⟩ ℚ)
hζ : ζ ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
I : Ideal (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hI : span {↑a + ζ * ↑b} = I ^ p
⊢ span {↑a + ζ * ↑b} = ?intro.I ^ p

case intro.I
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
this : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ (CyclotomicField ⟨p, ⋯⟩ ℚ)
hζ : ζ ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
I : Ideal (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hI : span {↑a + ζ * ↑b} = I ^ p
⊢ Ideal (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
Theorem: FltRegular.is_principal
Proof state before:
case intro.hreg
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
this : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ (CyclotomicField ⟨p, ⋯⟩ ℚ)
hζ : ζ ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
I : Ideal (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hI : span {↑a + ζ * ↑b} = I ^ p
⊢ p.Coprime (Fintype.card (ClassGroup (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))))
Tactic:
rwa [IsRegularPrime, IsRegularNumber] at hreg
Proof state after:
no goals
Theorem: FltRegular.is_principal
Proof state before:
case intro.hI
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hreg : IsRegularPrime p
hp5 : 5 ≤ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
this : IsCyclotomicExtension {⟨p, ⋯⟩} ℚ (CyclotomicField ⟨p, ⋯⟩ ℚ)
hζ : ζ ∈ nthRootsFinset p (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
I : Ideal (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))
hI : span {↑a + ζ * ↑b} = I ^ p
⊢ span {↑a + ζ * ↑b} = ?intro.I ^ p
Tactic:
exact hI
Proof state after:
no goals
Theorem: FltRegular.ex_fin_div
Proof state before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
⊢ ∃ k₁ k₂, ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p] ∧ ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
Tactic:
let ζ' := (ζ : K)
Proof state after:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
⊢ ∃ k₁ k₂, ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p] ∧ ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
Theorem: FltRegular.ex_fin_div
Proof state before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
⊢ ∃ k₁ k₂, ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p] ∧ ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
Tactic:
have hζ' : IsPrimitiveRoot ζ' P := IsPrimitiveRoot.coe_submonoidClass_iff.2 hζ
Proof state after:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
⊢ ∃ k₁ k₂, ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p] ∧ ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
Theorem: FltRegular.ex_fin_div
Proof state before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
⊢ ∃ k₁ k₂, ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p] ∧ ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
Tactic:
have h : ζ = (hζ'.unit' : R) := by rfl
Proof state after:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
⊢ ∃ k₁ k₂, ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p] ∧ ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
Theorem: FltRegular.ex_fin_div
Proof state before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
⊢ ∃ k₁ k₂, ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p] ∧ ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
Tactic:
have hP : P ≠ (2 : ℕ+) := by
  intro hP
  rw [← PNat.coe_inj, PNat.mk_coe] at hP
  rw [hP] at hp5
  contradiction
Proof state after:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
⊢ ∃ k₁ k₂, ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p] ∧ ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
Theorem: FltRegular.ex_fin_div
Proof state before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
⊢ ∃ k₁ k₂, ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p] ∧ ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
Tactic:
haveI := (⟨hpri.out⟩ : Fact (P : ℕ).Prime)
Proof state after:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
⊢ ∃ k₁ k₂, ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p] ∧ ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
Theorem: FltRegular.ex_fin_div
Proof state before:
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
⊢ ∃ k₁ k₂, ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p] ∧ ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
Tactic:
obtain ⟨u, α, hu⟩ := is_principal hreg hp5 hgcd caseI H hζ
Proof state after:
case intro.intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ζ * ↑b
⊢ ∃ k₁ k₂, ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p] ∧ ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
Theorem: FltRegular.ex_fin_div
Proof state before:
case intro.intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ζ * ↑b
⊢ ∃ k₁ k₂, ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p] ∧ ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
Tactic:
rw [h, mul_comm _ (↑b : R), ← pow_one hζ'.unit'] at hu
Proof state after:
case intro.intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
⊢ ∃ k₁ k₂, ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p] ∧ ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
Theorem: FltRegular.ex_fin_div
Proof state before:
case intro.intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
⊢ ∃ k₁ k₂, ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p] ∧ ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
Tactic:
obtain ⟨k, hk⟩ := FltRegular.CaseI.exists_int_sum_eq_zero hζ' hP hpri.out a b 1 hu.symm
Proof state after:
case intro.intro.intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hk : ↑a + ↑b * ↑(hζ'.unit' ^ 1) - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑(hζ'.unit' ^ (-1))) ∈ span {↑↑⟨p, ⋯⟩}
⊢ ∃ k₁ k₂, ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p] ∧ ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
Theorem: FltRegular.ex_fin_div
Proof state before:
case intro.intro.intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hk : ↑a + ↑b * ↑(hζ'.unit' ^ 1) - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑(hζ'.unit' ^ (-1))) ∈ span {↑↑⟨p, ⋯⟩}
⊢ ∃ k₁ k₂, ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p] ∧ ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
Tactic:
simp only [zpow_one, zpow_neg, PNat.mk_coe, mem_span_singleton, ← h] at hk
Proof state after:
case intro.intro.intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hk : ↑p ∣ ↑a + ↑b * ζ - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹)
⊢ ∃ k₁ k₂, ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p] ∧ ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
Theorem: FltRegular.ex_fin_div
Proof state before:
case intro.intro.intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hk : ↑p ∣ ↑a + ↑b * ζ - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹)
⊢ ∃ k₁ k₂, ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p] ∧ ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
Tactic:
have hpcoe : (p : ℤ) ≠ 0 := by simp [hpri.out.ne_zero]
Proof state after:
case intro.intro.intro
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hk : ↑p ∣ ↑a + ↑b * ζ - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹)
hpcoe : ↑p ≠ 0
⊢ ∃ k₁ k₂, ↑↑k₂ ≡ ↑↑k₁ - 1 [ZMOD ↑p] ∧ ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑k₁ - ↑b * ζ ^ ↑k₂
Theorem: FltRegular.ex_fin_div
Proof state before:
case intro.intro.intro.refine'_4
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hk : ↑p ∣ ↑a + ↑b * ζ - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹)
hpcoe : ↑p ≠ 0
⊢ ↑p ∣ ↑a + ↑b * ζ - ↑a * ζ ^ ↑⟨(2 * k % ↑p).natAbs, ⋯⟩ - ↑b * ζ ^ ↑⟨((2 * k - 1) % ↑p).natAbs, ⋯⟩
Tactic:
simp only [add_sub_assoc, sub_sub] at hk ⊢
Proof state after:
case intro.intro.intro.refine'_4
p : ℕ
hpri : Fact p.Prime
a b c : ℤ
ζ : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hp5 : 5 ≤ p
hreg : IsRegularPrime p
hζ : IsPrimitiveRoot ζ p
hgcd : {a, b, c}.gcd id = 1
caseI : ¬↑p ∣ a * b * c
H : a ^ p + b ^ p = c ^ p
ζ' : CyclotomicField ⟨p, ⋯⟩ ℚ := ↑ζ
hζ' : IsPrimitiveRoot ζ' ↑⟨p, ⋯⟩
h : ζ = ↑hζ'.unit'
hP : ⟨p, ⋯⟩ ≠ 2
this : Fact (↑⟨p, ⋯⟩).Prime
u : (𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ))ˣ
α : 𝓞 (CyclotomicField ⟨p, ⋯⟩ ℚ)
hu : ↑u * α ^ p = ↑a + ↑b * ↑(hζ'.unit' ^ 1)
k : ℤ
hpcoe : ↑p ≠ 0
hk : ↑p ∣ ↑a + (↑b * ζ - ↑(hζ'.unit' ^ (2 * k)) * (↑a + ↑b * ↑hζ'.unit'⁻¹))
⊢ ↑p ∣ ↑a + (↑b * ζ - (↑a * ζ ^ (2 * k % ↑p).natAbs + ↑b * ζ ^ ((2 * k - 1) % ↑p).natAbs))