The induction step in Case II #
This file constructs the ideal and unit data that turn a Case II solution into the next solution in the induction.
theorem
m_ne_zero
{K : Type}
{p : ℕ}
[NeZero p]
[Field K]
[NumberField K]
{ζ : K}
(hζ : IsPrimitiveRoot ζ p)
{x y : NumberField.RingOfIntegers K}
(hy : ¬hζ.toInteger - 1 ∣ y)
:
theorem
coprime_c_aux
{K : Type}
{p : ℕ}
[NeZero p]
[Field K]
[NumberField K]
{ζ : K}
(hζ : IsPrimitiveRoot ζ p)
{x y : NumberField.RingOfIntegers K}
[hpri : Fact (Nat.Prime p)]
(η₁ η₂ : ↥(Polynomial.nthRootsFinset p 1))
(hη : η₁ ≠ η₂)
:
Ideal.span {x + y * ↑η₁} ⊔ Ideal.span {x + y * ↑η₂} ∣ gcd (Ideal.span {x}) (Ideal.span {y}) * Ideal.span {hζ.toInteger - 1}
theorem
x_plus_y_mul_ne_zero
{K : Type}
{p : ℕ}
[NeZero p]
[Field K]
(hp : p ≠ 2)
{ζ : K}
(hζ : IsPrimitiveRoot ζ p)
{x y z : NumberField.RingOfIntegers K}
{ε : (NumberField.RingOfIntegers K)ˣ}
{m : ℕ}
(e : x ^ p + y ^ p = ↑ε * ((hζ.toInteger - 1) ^ (m + 1) * z) ^ p)
(hz : ¬hζ.toInteger - 1 ∣ z)
(η : ↥(Polynomial.nthRootsFinset p 1))
[hpri : Fact (Nat.Prime p)]
:
theorem
one_sub_zeta_dvd_zeta_pow_sub
{K : Type}
{p : ℕ}
[NeZero p]
[Field K]
[NumberField K]
(hp : p ≠ 2)
{ζ : K}
(hζ : IsPrimitiveRoot ζ p)
{x y z : NumberField.RingOfIntegers K}
{ε : (NumberField.RingOfIntegers K)ˣ}
{m : ℕ}
(e : x ^ p + y ^ p = ↑ε * ((hζ.toInteger - 1) ^ (m + 1) * z) ^ p)
(η : ↥(Polynomial.nthRootsFinset p 1))
[hpri : Fact (Nat.Prime p)]
[IsCyclotomicExtension {p} ℚ K]
:
theorem
div_one_sub_zeta_mem
{K : Type}
{p : ℕ}
[NeZero p]
[Field K]
[NumberField K]
(hp : p ≠ 2)
{ζ : K}
(hζ : IsPrimitiveRoot ζ p)
{x y z : NumberField.RingOfIntegers K}
{ε : (NumberField.RingOfIntegers K)ˣ}
{m : ℕ}
(e : x ^ p + y ^ p = ↑ε * ((hζ.toInteger - 1) ^ (m + 1) * z) ^ p)
(η : ↥(Polynomial.nthRootsFinset p 1))
[hpri : Fact (Nat.Prime p)]
[IsCyclotomicExtension {p} ℚ K]
:
def
divZetaSubOne
{K : Type}
{p : ℕ}
[NeZero p]
[Field K]
[NumberField K]
(hp : p ≠ 2)
{ζ : K}
(hζ : IsPrimitiveRoot ζ p)
{x y z : NumberField.RingOfIntegers K}
{ε : (NumberField.RingOfIntegers K)ˣ}
{m : ℕ}
(e : x ^ p + y ^ p = ↑ε * ((hζ.toInteger - 1) ^ (m + 1) * z) ^ p)
[hpri : Fact (Nat.Prime p)]
[IsCyclotomicExtension {p} ℚ K]
:
The integral quotient (x + y * η) / (ζ - 1) for a p-th root of unity η.
Instances For
theorem
div_zeta_sub_one_mul_zeta_sub_one
{K : Type}
{p : ℕ}
[NeZero p]
[Field K]
[NumberField K]
(hp : p ≠ 2)
{ζ : K}
(hζ : IsPrimitiveRoot ζ p)
{x y z : NumberField.RingOfIntegers K}
{ε : (NumberField.RingOfIntegers K)ˣ}
{m : ℕ}
(e : x ^ p + y ^ p = ↑ε * ((hζ.toInteger - 1) ^ (m + 1) * z) ^ p)
[hpri : Fact (Nat.Prime p)]
[IsCyclotomicExtension {p} ℚ K]
(η : ↥(Polynomial.nthRootsFinset p 1))
:
theorem
div_zeta_sub_one_sub
{K : Type}
{p : ℕ}
[NeZero p]
[Field K]
[NumberField K]
(hp : p ≠ 2)
{ζ : K}
(hζ : IsPrimitiveRoot ζ p)
{x y z : NumberField.RingOfIntegers K}
{ε : (NumberField.RingOfIntegers K)ˣ}
{m : ℕ}
(e : x ^ p + y ^ p = ↑ε * ((hζ.toInteger - 1) ^ (m + 1) * z) ^ p)
[hpri : Fact (Nat.Prime p)]
[IsCyclotomicExtension {p} ℚ K]
(η₁ η₂ : ↥(Polynomial.nthRootsFinset p 1))
(hη : η₁ ≠ η₂)
:
Associated y (divZetaSubOne hp hζ e η₁ - divZetaSubOne hp hζ e η₂)
theorem
div_zeta_sub_one_Injective
{K : Type}
{p : ℕ}
[NeZero p]
[Field K]
[NumberField K]
(hp : p ≠ 2)
{ζ : K}
(hζ : IsPrimitiveRoot ζ p)
{x y z : NumberField.RingOfIntegers K}
{ε : (NumberField.RingOfIntegers K)ˣ}
{m : ℕ}
(e : x ^ p + y ^ p = ↑ε * ((hζ.toInteger - 1) ^ (m + 1) * z) ^ p)
(hy : ¬hζ.toInteger - 1 ∣ y)
[hpri : Fact (Nat.Prime p)]
[IsCyclotomicExtension {p} ℚ K]
:
Function.Injective fun (η : ↥(Polynomial.nthRootsFinset p 1)) =>
(Ideal.Quotient.mk (Ideal.span {hζ.toInteger - 1})) (divZetaSubOne hp hζ e η)
instance
instFiniteQuotientRingOfIntegersIdealSpanSingletonSetHSubToIntegerOfNat_leanPool
{K : Type}
{p : ℕ}
[NeZero p]
[Field K]
[NumberField K]
{ζ : K}
(hζ : IsPrimitiveRoot ζ p)
[hpri : Fact (Nat.Prime p)]
:
Finite (NumberField.RingOfIntegers K ⧸ Ideal.span {hζ.toInteger - 1})
theorem
div_zeta_sub_one_Bijective
{K : Type}
{p : ℕ}
[NeZero p]
[Field K]
[NumberField K]
(hp : p ≠ 2)
{ζ : K}
(hζ : IsPrimitiveRoot ζ p)
{x y z : NumberField.RingOfIntegers K}
{ε : (NumberField.RingOfIntegers K)ˣ}
{m : ℕ}
(e : x ^ p + y ^ p = ↑ε * ((hζ.toInteger - 1) ^ (m + 1) * z) ^ p)
(hy : ¬hζ.toInteger - 1 ∣ y)
[hpri : Fact (Nat.Prime p)]
[IsCyclotomicExtension {p} ℚ K]
:
Function.Bijective fun (η : ↥(Polynomial.nthRootsFinset p 1)) =>
(Ideal.Quotient.mk (Ideal.span {hζ.toInteger - 1})) (divZetaSubOne hp hζ e η)
theorem
gcd_zeta_sub_one_eq_one
{K : Type}
{p : ℕ}
[NeZero p]
[Field K]
[NumberField K]
{ζ : K}
(hζ : IsPrimitiveRoot ζ p)
{x y : NumberField.RingOfIntegers K}
(hy : ¬hζ.toInteger - 1 ∣ y)
[hpri : Fact (Nat.Prime p)]
[IsCyclotomicExtension {p} ℚ K]
:
theorem
gcd_div_div_zeta_sub_one
{K : Type}
{p : ℕ}
[NeZero p]
[Field K]
[NumberField K]
(hp : p ≠ 2)
{ζ : K}
(hζ : IsPrimitiveRoot ζ p)
{x y z : NumberField.RingOfIntegers K}
{ε : (NumberField.RingOfIntegers K)ˣ}
{m : ℕ}
(e : x ^ p + y ^ p = ↑ε * ((hζ.toInteger - 1) ^ (m + 1) * z) ^ p)
(hy : ¬hζ.toInteger - 1 ∣ y)
[hpri : Fact (Nat.Prime p)]
[IsCyclotomicExtension {p} ℚ K]
(η : ↥(Polynomial.nthRootsFinset p 1))
:
noncomputable def
divZetaSubOneDvdGcd
{K : Type}
{p : ℕ}
[NeZero p]
[Field K]
[NumberField K]
(hp : p ≠ 2)
{ζ : K}
(hζ : IsPrimitiveRoot ζ p)
{x y z : NumberField.RingOfIntegers K}
{ε : (NumberField.RingOfIntegers K)ˣ}
{m : ℕ}
(e : x ^ p + y ^ p = ↑ε * ((hζ.toInteger - 1) ^ (m + 1) * z) ^ p)
(hy : ¬hζ.toInteger - 1 ∣ y)
(η : ↥(Polynomial.nthRootsFinset p 1))
[hpri : Fact (Nat.Prime p)]
[IsCyclotomicExtension {p} ℚ K]
:
The quotient ideal obtained from the divisibility by 𝔪.
Equations
- divZetaSubOneDvdGcd hp hζ e hy η = Exists.choose ⋯
Instances For
theorem
div_zeta_sub_one_dvd_gcd_spec
{K : Type}
{p : ℕ}
[NeZero p]
[Field K]
[NumberField K]
(hp : p ≠ 2)
{ζ : K}
(hζ : IsPrimitiveRoot ζ p)
{x y z : NumberField.RingOfIntegers K}
{ε : (NumberField.RingOfIntegers K)ˣ}
{m : ℕ}
(e : x ^ p + y ^ p = ↑ε * ((hζ.toInteger - 1) ^ (m + 1) * z) ^ p)
(hy : ¬hζ.toInteger - 1 ∣ y)
(η : ↥(Polynomial.nthRootsFinset p 1))
[hpri : Fact (Nat.Prime p)]
[IsCyclotomicExtension {p} ℚ K]
:
gcd (Ideal.span {x}) (Ideal.span {y}) * (fun (η : ↥(Polynomial.nthRootsFinset p 1)) => divZetaSubOneDvdGcd hp hζ e hy η) η = Ideal.span {divZetaSubOne hp hζ e η}
theorem
m_mul_c_mul_p
{K : Type}
{p : ℕ}
[NeZero p]
[Field K]
[NumberField K]
(hp : p ≠ 2)
{ζ : K}
(hζ : IsPrimitiveRoot ζ p)
{x y z : NumberField.RingOfIntegers K}
{ε : (NumberField.RingOfIntegers K)ˣ}
{m : ℕ}
(e : x ^ p + y ^ p = ↑ε * ((hζ.toInteger - 1) ^ (m + 1) * z) ^ p)
(hy : ¬hζ.toInteger - 1 ∣ y)
(η : ↥(Polynomial.nthRootsFinset p 1))
[hpri : Fact (Nat.Prime p)]
[IsCyclotomicExtension {p} ℚ K]
:
gcd (Ideal.span {x}) (Ideal.span {y}) * (fun (η : ↥(Polynomial.nthRootsFinset p 1)) => divZetaSubOneDvdGcd hp hζ e hy η) η * Ideal.span {hζ.toInteger - 1} = Ideal.span {x + y * ↑η}
theorem
coprime_c
{K : Type}
{p : ℕ}
[NeZero p]
[Field K]
[NumberField K]
(hp : p ≠ 2)
{ζ : K}
(hζ : IsPrimitiveRoot ζ p)
{x y z : NumberField.RingOfIntegers K}
{ε : (NumberField.RingOfIntegers K)ˣ}
{m : ℕ}
(e : x ^ p + y ^ p = ↑ε * ((hζ.toInteger - 1) ^ (m + 1) * z) ^ p)
(hy : ¬hζ.toInteger - 1 ∣ y)
[hpri : Fact (Nat.Prime p)]
[IsCyclotomicExtension {p} ℚ K]
(η₁ η₂ : ↥(Polynomial.nthRootsFinset p 1))
(hη : η₁ ≠ η₂)
:
IsCoprime ((fun (η : ↥(Polynomial.nthRootsFinset p 1)) => divZetaSubOneDvdGcd hp hζ e hy η) η₁)
((fun (η : ↥(Polynomial.nthRootsFinset p 1)) => divZetaSubOneDvdGcd hp hζ e hy η) η₂)
theorem
gcd_m_p_pow_eq_one
{K : Type}
{p : ℕ}
[NeZero p]
[Field K]
[NumberField K]
{ζ : K}
(hζ : IsPrimitiveRoot ζ p)
{x y : NumberField.RingOfIntegers K}
{m : ℕ}
(hy : ¬hζ.toInteger - 1 ∣ y)
[hpri : Fact (Nat.Prime p)]
[IsCyclotomicExtension {p} ℚ K]
:
theorem
m_dvd_z
{K : Type}
{p : ℕ}
[NeZero p]
[Field K]
[NumberField K]
{ζ : K}
(hζ : IsPrimitiveRoot ζ p)
{x y z : NumberField.RingOfIntegers K}
{ε : (NumberField.RingOfIntegers K)ˣ}
{m : ℕ}
(e : x ^ p + y ^ p = ↑ε * ((hζ.toInteger - 1) ^ (m + 1) * z) ^ p)
(hy : ¬hζ.toInteger - 1 ∣ y)
[hpri : Fact (Nat.Prime p)]
[IsCyclotomicExtension {p} ℚ K]
:
noncomputable def
zDivM
{K : Type}
{p : ℕ}
[NeZero p]
[Field K]
[NumberField K]
{ζ : K}
(hζ : IsPrimitiveRoot ζ p)
{x y z : NumberField.RingOfIntegers K}
{ε : (NumberField.RingOfIntegers K)ˣ}
{m : ℕ}
(e : x ^ p + y ^ p = ↑ε * ((hζ.toInteger - 1) ^ (m + 1) * z) ^ p)
(hy : ¬hζ.toInteger - 1 ∣ y)
[hpri : Fact (Nat.Prime p)]
[IsCyclotomicExtension {p} ℚ K]
:
The ideal quotient witnessing 𝔷 = 𝔪 * zDivM.
Equations
- zDivM hζ e hy = Exists.choose ⋯
Instances For
theorem
z_div_m_spec
{K : Type}
{p : ℕ}
[NeZero p]
[Field K]
[NumberField K]
{ζ : K}
(hζ : IsPrimitiveRoot ζ p)
{x y z : NumberField.RingOfIntegers K}
{ε : (NumberField.RingOfIntegers K)ˣ}
{m : ℕ}
(e : x ^ p + y ^ p = ↑ε * ((hζ.toInteger - 1) ^ (m + 1) * z) ^ p)
(hy : ¬hζ.toInteger - 1 ∣ y)
[hpri : Fact (Nat.Prime p)]
[IsCyclotomicExtension {p} ℚ K]
:
theorem
exists_ideal_pow_eq_c_aux
{K : Type}
{p : ℕ}
[NeZero p]
[Field K]
[NumberField K]
{ζ : K}
(hζ : IsPrimitiveRoot ζ p)
{x y z : NumberField.RingOfIntegers K}
{ε : (NumberField.RingOfIntegers K)ˣ}
{m : ℕ}
(e : x ^ p + y ^ p = ↑ε * ((hζ.toInteger - 1) ^ (m + 1) * z) ^ p)
(hy : ¬hζ.toInteger - 1 ∣ y)
[hpri : Fact (Nat.Prime p)]
[IsCyclotomicExtension {p} ℚ K]
:
theorem
prod_c
{K : Type}
{p : ℕ}
[NeZero p]
[Field K]
[NumberField K]
(hp : p ≠ 2)
{ζ : K}
(hζ : IsPrimitiveRoot ζ p)
{x y z : NumberField.RingOfIntegers K}
{ε : (NumberField.RingOfIntegers K)ˣ}
{m : ℕ}
(e : x ^ p + y ^ p = ↑ε * ((hζ.toInteger - 1) ^ (m + 1) * z) ^ p)
(hy : ¬hζ.toInteger - 1 ∣ y)
[hpri : Fact (Nat.Prime p)]
[IsCyclotomicExtension {p} ℚ K]
:
∏ η ∈ (Polynomial.nthRootsFinset p 1).attach,
(fun (η : ↥(Polynomial.nthRootsFinset p 1)) => divZetaSubOneDvdGcd hp hζ e hy η) η = (zDivM hζ e hy * Ideal.span {hζ.toInteger - 1} ^ m) ^ p
theorem
exists_ideal_pow_eq_c
{K : Type}
{p : ℕ}
[NeZero p]
[Field K]
[NumberField K]
(hp : p ≠ 2)
{ζ : K}
(hζ : IsPrimitiveRoot ζ p)
{x y z : NumberField.RingOfIntegers K}
{ε : (NumberField.RingOfIntegers K)ˣ}
{m : ℕ}
(e : x ^ p + y ^ p = ↑ε * ((hζ.toInteger - 1) ^ (m + 1) * z) ^ p)
(hy : ¬hζ.toInteger - 1 ∣ y)
(η : ↥(Polynomial.nthRootsFinset p 1))
[hpri : Fact (Nat.Prime p)]
[IsCyclotomicExtension {p} ℚ K]
:
∃ (I : Ideal (NumberField.RingOfIntegers K)),
(fun (η : ↥(Polynomial.nthRootsFinset p 1)) => divZetaSubOneDvdGcd hp hζ e hy η) η = I ^ p
noncomputable def
rootDivZetaSubOneDvdGcd
{K : Type}
{p : ℕ}
[NeZero p]
[Field K]
[NumberField K]
(hp : p ≠ 2)
{ζ : K}
(hζ : IsPrimitiveRoot ζ p)
{x y z : NumberField.RingOfIntegers K}
{ε : (NumberField.RingOfIntegers K)ˣ}
{m : ℕ}
(e : x ^ p + y ^ p = ↑ε * ((hζ.toInteger - 1) ^ (m + 1) * z) ^ p)
(hy : ¬hζ.toInteger - 1 ∣ y)
(η : ↥(Polynomial.nthRootsFinset p 1))
[hpri : Fact (Nat.Prime p)]
[IsCyclotomicExtension {p} ℚ K]
:
A p-th ideal root of 𝔠 η.
Equations
- rootDivZetaSubOneDvdGcd hp hζ e hy η = ⋯.choose
Instances For
theorem
root_div_zeta_sub_one_dvd_gcd_spec
{K : Type}
{p : ℕ}
[NeZero p]
[Field K]
[NumberField K]
(hp : p ≠ 2)
{ζ : K}
(hζ : IsPrimitiveRoot ζ p)
{x y z : NumberField.RingOfIntegers K}
{ε : (NumberField.RingOfIntegers K)ˣ}
{m : ℕ}
(e : x ^ p + y ^ p = ↑ε * ((hζ.toInteger - 1) ^ (m + 1) * z) ^ p)
(hy : ¬hζ.toInteger - 1 ∣ y)
(η : ↥(Polynomial.nthRootsFinset p 1))
[hpri : Fact (Nat.Prime p)]
[IsCyclotomicExtension {p} ℚ K]
:
rootDivZetaSubOneDvdGcd hp hζ e hy η ^ p = (fun (η : ↥(Polynomial.nthRootsFinset p 1)) => divZetaSubOneDvdGcd hp hζ e hy η) η
theorem
c_div_principal_aux
{K : Type}
{p : ℕ}
[NeZero p]
[Field K]
[NumberField K]
(hp : p ≠ 2)
{ζ : K}
(hζ : IsPrimitiveRoot ζ p)
{x y z : NumberField.RingOfIntegers K}
{ε : (NumberField.RingOfIntegers K)ˣ}
{m : ℕ}
(e : x ^ p + y ^ p = ↑ε * ((hζ.toInteger - 1) ^ (m + 1) * z) ^ p)
(hy : ¬hζ.toInteger - 1 ∣ y)
[hpri : Fact (Nat.Prime p)]
[IsCyclotomicExtension {p} ℚ K]
(η₁ η₂ : ↥(Polynomial.nthRootsFinset p 1))
:
↑(Ideal.span {x + y * ↑η₁}) / ↑(Ideal.span {x + y * ↑η₂}) = ↑((fun (η : ↥(Polynomial.nthRootsFinset p 1)) => divZetaSubOneDvdGcd hp hζ e hy η) η₁) / ↑((fun (η : ↥(Polynomial.nthRootsFinset p 1)) => divZetaSubOneDvdGcd hp hζ e hy η) η₂)
theorem
c_div_principal
{K : Type}
{p : ℕ}
[NeZero p]
[Field K]
[NumberField K]
(hp : p ≠ 2)
{ζ : K}
(hζ : IsPrimitiveRoot ζ p)
{x y z : NumberField.RingOfIntegers K}
{ε : (NumberField.RingOfIntegers K)ˣ}
{m : ℕ}
(e : x ^ p + y ^ p = ↑ε * ((hζ.toInteger - 1) ^ (m + 1) * z) ^ p)
(hy : ¬hζ.toInteger - 1 ∣ y)
[hpri : Fact (Nat.Prime p)]
[IsCyclotomicExtension {p} ℚ K]
(η₁ η₂ : ↥(Polynomial.nthRootsFinset p 1))
:
(↑(↑((fun (η : ↥(Polynomial.nthRootsFinset p 1)) => divZetaSubOneDvdGcd hp hζ e hy η) η₁) / ↑((fun (η : ↥(Polynomial.nthRootsFinset p 1)) => divZetaSubOneDvdGcd hp hζ e hy η) η₂))).IsPrincipal
noncomputable def
zetaSubOneDvdRoot
{K : Type}
{p : ℕ}
[NeZero p]
[Field K]
[NumberField K]
(hp : p ≠ 2)
{ζ : K}
(hζ : IsPrimitiveRoot ζ p)
{x y z : NumberField.RingOfIntegers K}
{ε : (NumberField.RingOfIntegers K)ˣ}
{m : ℕ}
(e : x ^ p + y ^ p = ↑ε * ((hζ.toInteger - 1) ^ (m + 1) * z) ^ p)
(hy : ¬hζ.toInteger - 1 ∣ y)
[hpri : Fact (Nat.Prime p)]
[IsCyclotomicExtension {p} ℚ K]
:
↥(Polynomial.nthRootsFinset p 1)
The unique root of unity whose quotient is divisible by ζ - 1.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
zeta_sub_one_dvd_root_spec
{K : Type}
{p : ℕ}
[NeZero p]
[Field K]
[NumberField K]
(hp : p ≠ 2)
{ζ : K}
(hζ : IsPrimitiveRoot ζ p)
{x y z : NumberField.RingOfIntegers K}
{ε : (NumberField.RingOfIntegers K)ˣ}
{m : ℕ}
(e : x ^ p + y ^ p = ↑ε * ((hζ.toInteger - 1) ^ (m + 1) * z) ^ p)
(hy : ¬hζ.toInteger - 1 ∣ y)
[hpri : Fact (Nat.Prime p)]
[IsCyclotomicExtension {p} ℚ K]
:
(Ideal.Quotient.mk (Ideal.span {hζ.toInteger - 1})) (divZetaSubOne hp hζ e (zetaSubOneDvdRoot hp hζ e hy)) = 0
theorem
p_dvd_c_iff
{K : Type}
{p : ℕ}
[NeZero p]
[Field K]
[NumberField K]
(hp : p ≠ 2)
{ζ : K}
(hζ : IsPrimitiveRoot ζ p)
{x y z : NumberField.RingOfIntegers K}
{ε : (NumberField.RingOfIntegers K)ˣ}
{m : ℕ}
(e : x ^ p + y ^ p = ↑ε * ((hζ.toInteger - 1) ^ (m + 1) * z) ^ p)
(hy : ¬hζ.toInteger - 1 ∣ y)
(η : ↥(Polynomial.nthRootsFinset p 1))
[hpri : Fact (Nat.Prime p)]
[IsCyclotomicExtension {p} ℚ K]
:
Ideal.span {hζ.toInteger - 1} ∣ (fun (η : ↥(Polynomial.nthRootsFinset p 1)) => divZetaSubOneDvdGcd hp hζ e hy η) η ↔ η = zetaSubOneDvdRoot hp hζ e hy
theorem
p_pow_dvd_c_eta_zero_aux
{K : Type}
{p : ℕ}
[NeZero p]
[Field K]
[NumberField K]
(hp : p ≠ 2)
{ζ : K}
(hζ : IsPrimitiveRoot ζ p)
{x y z : NumberField.RingOfIntegers K}
{ε : (NumberField.RingOfIntegers K)ˣ}
{m : ℕ}
(e : x ^ p + y ^ p = ↑ε * ((hζ.toInteger - 1) ^ (m + 1) * z) ^ p)
(hy : ¬hζ.toInteger - 1 ∣ y)
[hpri : Fact (Nat.Prime p)]
[IsCyclotomicExtension {p} ℚ K]
[DecidableEq (NumberField.RingOfIntegers K)]
:
gcd (Ideal.span {hζ.toInteger - 1} ^ (m * p))
(∏ η ∈ (Polynomial.nthRootsFinset p 1).attach \ {zetaSubOneDvdRoot hp hζ e hy},
(fun (η : ↥(Polynomial.nthRootsFinset p 1)) => divZetaSubOneDvdGcd hp hζ e hy η) η) = 1
theorem
p_dvd_a_iff
{K : Type}
{p : ℕ}
[NeZero p]
[Field K]
[NumberField K]
(hp : p ≠ 2)
{ζ : K}
(hζ : IsPrimitiveRoot ζ p)
{x y z : NumberField.RingOfIntegers K}
{ε : (NumberField.RingOfIntegers K)ˣ}
{m : ℕ}
(e : x ^ p + y ^ p = ↑ε * ((hζ.toInteger - 1) ^ (m + 1) * z) ^ p)
(hy : ¬hζ.toInteger - 1 ∣ y)
(η : ↥(Polynomial.nthRootsFinset p 1))
[hpri : Fact (Nat.Prime p)]
[IsCyclotomicExtension {p} ℚ K]
:
Ideal.span {hζ.toInteger - 1} ∣ rootDivZetaSubOneDvdGcd hp hζ e hy η ↔ η = zetaSubOneDvdRoot hp hζ e hy
theorem
p_pow_dvd_c_eta_zero
{K : Type}
{p : ℕ}
[NeZero p]
[Field K]
[NumberField K]
(hp : p ≠ 2)
{ζ : K}
(hζ : IsPrimitiveRoot ζ p)
{x y z : NumberField.RingOfIntegers K}
{ε : (NumberField.RingOfIntegers K)ˣ}
{m : ℕ}
(e : x ^ p + y ^ p = ↑ε * ((hζ.toInteger - 1) ^ (m + 1) * z) ^ p)
(hy : ¬hζ.toInteger - 1 ∣ y)
[hpri : Fact (Nat.Prime p)]
[IsCyclotomicExtension {p} ℚ K]
:
Ideal.span {hζ.toInteger - 1} ^ (m * p) ∣ (fun (η : ↥(Polynomial.nthRootsFinset p 1)) => divZetaSubOneDvdGcd hp hζ e hy η) (zetaSubOneDvdRoot hp hζ e hy)
theorem
p_pow_dvd_a_eta_zero
{K : Type}
{p : ℕ}
[NeZero p]
[Field K]
[NumberField K]
(hp : p ≠ 2)
{ζ : K}
(hζ : IsPrimitiveRoot ζ p)
{x y z : NumberField.RingOfIntegers K}
{ε : (NumberField.RingOfIntegers K)ˣ}
{m : ℕ}
(e : x ^ p + y ^ p = ↑ε * ((hζ.toInteger - 1) ^ (m + 1) * z) ^ p)
(hy : ¬hζ.toInteger - 1 ∣ y)
[hpri : Fact (Nat.Prime p)]
[IsCyclotomicExtension {p} ℚ K]
:
Ideal.span {hζ.toInteger - 1} ^ m ∣ rootDivZetaSubOneDvdGcd hp hζ e hy (zetaSubOneDvdRoot hp hζ e hy)
noncomputable def
aEtaZeroDvdPPow
{K : Type}
{p : ℕ}
[NeZero p]
[Field K]
[NumberField K]
(hp : p ≠ 2)
{ζ : K}
(hζ : IsPrimitiveRoot ζ p)
{x y z : NumberField.RingOfIntegers K}
{ε : (NumberField.RingOfIntegers K)ˣ}
{m : ℕ}
(e : x ^ p + y ^ p = ↑ε * ((hζ.toInteger - 1) ^ (m + 1) * z) ^ p)
(hy : ¬hζ.toInteger - 1 ∣ y)
[hpri : Fact (Nat.Prime p)]
[IsCyclotomicExtension {p} ℚ K]
:
The quotient ideal after removing 𝔭 ^ m from the distinguished ideal root.
Equations
- aEtaZeroDvdPPow hp hζ e hy = Exists.choose ⋯
Instances For
theorem
a_eta_zero_dvd_p_pow_spec
{K : Type}
{p : ℕ}
[NeZero p]
[Field K]
[NumberField K]
(hp : p ≠ 2)
{ζ : K}
(hζ : IsPrimitiveRoot ζ p)
{x y z : NumberField.RingOfIntegers K}
{ε : (NumberField.RingOfIntegers K)ˣ}
{m : ℕ}
(e : x ^ p + y ^ p = ↑ε * ((hζ.toInteger - 1) ^ (m + 1) * z) ^ p)
(hy : ¬hζ.toInteger - 1 ∣ y)
[hpri : Fact (Nat.Prime p)]
[IsCyclotomicExtension {p} ℚ K]
:
Ideal.span {hζ.toInteger - 1} ^ m * aEtaZeroDvdPPow hp hζ e hy = rootDivZetaSubOneDvdGcd hp hζ e hy (zetaSubOneDvdRoot hp hζ e hy)
theorem
not_p_div_a_zero
{K : Type}
{p : ℕ}
[NeZero p]
[Field K]
[NumberField K]
(hp : p ≠ 2)
{ζ : K}
(hζ : IsPrimitiveRoot ζ p)
{x y z : NumberField.RingOfIntegers K}
{ε : (NumberField.RingOfIntegers K)ˣ}
{m : ℕ}
(e : x ^ p + y ^ p = ↑ε * ((hζ.toInteger - 1) ^ (m + 1) * z) ^ p)
(hy : ¬hζ.toInteger - 1 ∣ y)
(hz : ¬hζ.toInteger - 1 ∣ z)
[hpri : Fact (Nat.Prime p)]
[IsCyclotomicExtension {p} ℚ K]
:
theorem
one_le_m
{K : Type}
{p : ℕ}
[NeZero p]
[Field K]
[NumberField K]
(hp : p ≠ 2)
{ζ : K}
(hζ : IsPrimitiveRoot ζ p)
{x y z : NumberField.RingOfIntegers K}
{ε : (NumberField.RingOfIntegers K)ˣ}
{m : ℕ}
(e : x ^ p + y ^ p = ↑ε * ((hζ.toInteger - 1) ^ (m + 1) * z) ^ p)
(hy : ¬hζ.toInteger - 1 ∣ y)
(hz : ¬hζ.toInteger - 1 ∣ z)
[hpri : Fact (Nat.Prime p)]
[IsCyclotomicExtension {p} ℚ K]
:
theorem
exists_solution'_aux
{K : Type}
{p : ℕ}
[NeZero p]
[Field K]
[NumberField K]
(hp : p ≠ 2)
{ζ : K}
(hζ : IsPrimitiveRoot ζ p)
{x y : NumberField.RingOfIntegers K}
[hpri : Fact (Nat.Prime p)]
[IsCyclotomicExtension {p} ℚ K]
{ε₁ ε₂ : (NumberField.RingOfIntegers K)ˣ}
(hx : ¬hζ.toInteger - 1 ∣ x)
(h : ↑p ∣ ↑ε₁ * x ^ p + ↑ε₂ * y ^ p)
:
∃ (a : NumberField.RingOfIntegers K), ↑p ∣ ↑(ε₁ / ε₂) - a ^ p
theorem
a_div_principal
{K : Type}
{p : ℕ}
[NeZero p]
[Field K]
[NumberField K]
(hp : p ≠ 2)
{ζ : K}
(hζ : IsPrimitiveRoot ζ p)
{x y z : NumberField.RingOfIntegers K}
{ε : (NumberField.RingOfIntegers K)ˣ}
{m : ℕ}
(e : x ^ p + y ^ p = ↑ε * ((hζ.toInteger - 1) ^ (m + 1) * z) ^ p)
(hy : ¬hζ.toInteger - 1 ∣ y)
[hpri : Fact (Nat.Prime p)]
[IsCyclotomicExtension {p} ℚ K]
[Fintype (ClassGroup (NumberField.RingOfIntegers K))]
(hreg : p.Coprime (Fintype.card (ClassGroup (NumberField.RingOfIntegers K))))
(η₁ η₂ : ↥(Polynomial.nthRootsFinset p 1))
:
(↑(↑(rootDivZetaSubOneDvdGcd hp hζ e hy η₁) / ↑(rootDivZetaSubOneDvdGcd hp hζ e hy η₂))).IsPrincipal
theorem
isPrincipal_a_div_a_zero
{K : Type}
{p : ℕ}
[NeZero p]
[Field K]
[NumberField K]
(hp : p ≠ 2)
{ζ : K}
(hζ : IsPrimitiveRoot ζ p)
{x y z : NumberField.RingOfIntegers K}
{ε : (NumberField.RingOfIntegers K)ˣ}
{m : ℕ}
(e : x ^ p + y ^ p = ↑ε * ((hζ.toInteger - 1) ^ (m + 1) * z) ^ p)
(hy : ¬hζ.toInteger - 1 ∣ y)
(η : ↥(Polynomial.nthRootsFinset p 1))
[hpri : Fact (Nat.Prime p)]
[IsCyclotomicExtension {p} ℚ K]
[Fintype (ClassGroup (NumberField.RingOfIntegers K))]
(hreg : p.Coprime (Fintype.card (ClassGroup (NumberField.RingOfIntegers K))))
:
(↑(↑(rootDivZetaSubOneDvdGcd hp hζ e hy η) / ↑(aEtaZeroDvdPPow hp hζ e hy))).IsPrincipal
theorem
exists_not_dvd_spanSingleton_eq_a_div_a_zero
{K : Type}
{p : ℕ}
[NeZero p]
[Field K]
[NumberField K]
(hp : p ≠ 2)
{ζ : K}
(hζ : IsPrimitiveRoot ζ p)
{x y z : NumberField.RingOfIntegers K}
{ε : (NumberField.RingOfIntegers K)ˣ}
{m : ℕ}
(e : x ^ p + y ^ p = ↑ε * ((hζ.toInteger - 1) ^ (m + 1) * z) ^ p)
(hy : ¬hζ.toInteger - 1 ∣ y)
(hz : ¬hζ.toInteger - 1 ∣ z)
(η : ↥(Polynomial.nthRootsFinset p 1))
[hpri : Fact (Nat.Prime p)]
[IsCyclotomicExtension {p} ℚ K]
[Fintype (ClassGroup (NumberField.RingOfIntegers K))]
(hreg : p.Coprime (Fintype.card (ClassGroup (NumberField.RingOfIntegers K))))
(hη : η ≠ zetaSubOneDvdRoot hp hζ e hy)
:
∃ (a : NumberField.RingOfIntegers K) (b : NumberField.RingOfIntegers K),
¬hζ.toInteger - 1 ∣ a ∧ ¬hζ.toInteger - 1 ∣ b ∧ FractionalIdeal.spanSingleton (nonZeroDivisors (NumberField.RingOfIntegers K)) (↑a / ↑b) = ↑(rootDivZetaSubOneDvdGcd hp hζ e hy η) / ↑(aEtaZeroDvdPPow hp hζ e hy)
noncomputable def
aDivAZeroNum
{K : Type}
{p : ℕ}
[NeZero p]
[Field K]
[NumberField K]
(hp : p ≠ 2)
{ζ : K}
(hζ : IsPrimitiveRoot ζ p)
{x y z : NumberField.RingOfIntegers K}
{ε : (NumberField.RingOfIntegers K)ˣ}
{m : ℕ}
(e : x ^ p + y ^ p = ↑ε * ((hζ.toInteger - 1) ^ (m + 1) * z) ^ p)
(hy : ¬hζ.toInteger - 1 ∣ y)
(hz : ¬hζ.toInteger - 1 ∣ z)
(η : ↥(Polynomial.nthRootsFinset p 1))
[hpri : Fact (Nat.Prime p)]
[IsCyclotomicExtension {p} ℚ K]
[Fintype (ClassGroup (NumberField.RingOfIntegers K))]
(hreg : p.Coprime (Fintype.card (ClassGroup (NumberField.RingOfIntegers K))))
(hη : η ≠ zetaSubOneDvdRoot hp hζ e hy)
:
A numerator for the principal fractional ideal 𝔞 η / 𝔞₀.
Equations
- aDivAZeroNum hp hζ e hy hz η hreg hη = ⋯.choose
Instances For
noncomputable def
aDivAZeroDenom
{K : Type}
{p : ℕ}
[NeZero p]
[Field K]
[NumberField K]
(hp : p ≠ 2)
{ζ : K}
(hζ : IsPrimitiveRoot ζ p)
{x y z : NumberField.RingOfIntegers K}
{ε : (NumberField.RingOfIntegers K)ˣ}
{m : ℕ}
(e : x ^ p + y ^ p = ↑ε * ((hζ.toInteger - 1) ^ (m + 1) * z) ^ p)
(hy : ¬hζ.toInteger - 1 ∣ y)
(hz : ¬hζ.toInteger - 1 ∣ z)
(η : ↥(Polynomial.nthRootsFinset p 1))
[hpri : Fact (Nat.Prime p)]
[IsCyclotomicExtension {p} ℚ K]
[Fintype (ClassGroup (NumberField.RingOfIntegers K))]
(hreg : p.Coprime (Fintype.card (ClassGroup (NumberField.RingOfIntegers K))))
(hη : η ≠ zetaSubOneDvdRoot hp hζ e hy)
:
A denominator for the principal fractional ideal 𝔞 η / 𝔞₀.
Equations
- aDivAZeroDenom hp hζ e hy hz η hreg hη = ⋯.choose
Instances For
theorem
a_div_a_zero_num_spec
{K : Type}
{p : ℕ}
[NeZero p]
[Field K]
[NumberField K]
(hp : p ≠ 2)
{ζ : K}
(hζ : IsPrimitiveRoot ζ p)
{x y z : NumberField.RingOfIntegers K}
{ε : (NumberField.RingOfIntegers K)ˣ}
{m : ℕ}
(e : x ^ p + y ^ p = ↑ε * ((hζ.toInteger - 1) ^ (m + 1) * z) ^ p)
(hy : ¬hζ.toInteger - 1 ∣ y)
(hz : ¬hζ.toInteger - 1 ∣ z)
(η : ↥(Polynomial.nthRootsFinset p 1))
[hpri : Fact (Nat.Prime p)]
[IsCyclotomicExtension {p} ℚ K]
[Fintype (ClassGroup (NumberField.RingOfIntegers K))]
(hreg : p.Coprime (Fintype.card (ClassGroup (NumberField.RingOfIntegers K))))
(hη : η ≠ zetaSubOneDvdRoot hp hζ e hy)
:
¬hζ.toInteger - 1 ∣ (fun (η : ↥(Polynomial.nthRootsFinset p 1)) => aDivAZeroNum hp hζ e hy hz η hreg) η hη
theorem
a_div_a_zero_denom_spec
{K : Type}
{p : ℕ}
[NeZero p]
[Field K]
[NumberField K]
(hp : p ≠ 2)
{ζ : K}
(hζ : IsPrimitiveRoot ζ p)
{x y z : NumberField.RingOfIntegers K}
{ε : (NumberField.RingOfIntegers K)ˣ}
{m : ℕ}
(e : x ^ p + y ^ p = ↑ε * ((hζ.toInteger - 1) ^ (m + 1) * z) ^ p)
(hy : ¬hζ.toInteger - 1 ∣ y)
(hz : ¬hζ.toInteger - 1 ∣ z)
(η : ↥(Polynomial.nthRootsFinset p 1))
[hpri : Fact (Nat.Prime p)]
[IsCyclotomicExtension {p} ℚ K]
[Fintype (ClassGroup (NumberField.RingOfIntegers K))]
(hreg : p.Coprime (Fintype.card (ClassGroup (NumberField.RingOfIntegers K))))
(hη : η ≠ zetaSubOneDvdRoot hp hζ e hy)
:
¬hζ.toInteger - 1 ∣ (fun (η : ↥(Polynomial.nthRootsFinset p 1)) => aDivAZeroDenom hp hζ e hy hz η hreg) η hη
theorem
a_div_a_zero_eq
{K : Type}
{p : ℕ}
[NeZero p]
[Field K]
[NumberField K]
(hp : p ≠ 2)
{ζ : K}
(hζ : IsPrimitiveRoot ζ p)
{x y z : NumberField.RingOfIntegers K}
{ε : (NumberField.RingOfIntegers K)ˣ}
{m : ℕ}
(e : x ^ p + y ^ p = ↑ε * ((hζ.toInteger - 1) ^ (m + 1) * z) ^ p)
(hy : ¬hζ.toInteger - 1 ∣ y)
(hz : ¬hζ.toInteger - 1 ∣ z)
(η : ↥(Polynomial.nthRootsFinset p 1))
[hpri : Fact (Nat.Prime p)]
[IsCyclotomicExtension {p} ℚ K]
[Fintype (ClassGroup (NumberField.RingOfIntegers K))]
(hreg : p.Coprime (Fintype.card (ClassGroup (NumberField.RingOfIntegers K))))
(hη : η ≠ zetaSubOneDvdRoot hp hζ e hy)
:
FractionalIdeal.spanSingleton (nonZeroDivisors (NumberField.RingOfIntegers K))
(↑((fun (η : ↥(Polynomial.nthRootsFinset p 1)) => aDivAZeroNum hp hζ e hy hz η hreg) η hη) / ↑((fun (η : ↥(Polynomial.nthRootsFinset p 1)) => aDivAZeroDenom hp hζ e hy hz η hreg) η hη)) = ↑(rootDivZetaSubOneDvdGcd hp hζ e hy η) / ↑(aEtaZeroDvdPPow hp hζ e hy)
theorem
a_mul_denom_eq_a_zero_mul_num
{K : Type}
{p : ℕ}
[NeZero p]
[Field K]
[NumberField K]
(hp : p ≠ 2)
{ζ : K}
(hζ : IsPrimitiveRoot ζ p)
{x y z : NumberField.RingOfIntegers K}
{ε : (NumberField.RingOfIntegers K)ˣ}
{m : ℕ}
(e : x ^ p + y ^ p = ↑ε * ((hζ.toInteger - 1) ^ (m + 1) * z) ^ p)
(hy : ¬hζ.toInteger - 1 ∣ y)
(hz : ¬hζ.toInteger - 1 ∣ z)
(η : ↥(Polynomial.nthRootsFinset p 1))
[hpri : Fact (Nat.Prime p)]
[IsCyclotomicExtension {p} ℚ K]
[Fintype (ClassGroup (NumberField.RingOfIntegers K))]
(hreg : p.Coprime (Fintype.card (ClassGroup (NumberField.RingOfIntegers K))))
(hη : η ≠ zetaSubOneDvdRoot hp hζ e hy)
:
rootDivZetaSubOneDvdGcd hp hζ e hy η * Ideal.span {(fun (η : ↥(Polynomial.nthRootsFinset p 1)) => aDivAZeroDenom hp hζ e hy hz η hreg) η hη} = aEtaZeroDvdPPow hp hζ e hy * Ideal.span {(fun (η : ↥(Polynomial.nthRootsFinset p 1)) => aDivAZeroNum hp hζ e hy hz η hreg) η hη}
theorem
associated_eta_zero
{K : Type}
{p : ℕ}
[NeZero p]
[Field K]
[NumberField K]
(hp : p ≠ 2)
{ζ : K}
(hζ : IsPrimitiveRoot ζ p)
{x y z : NumberField.RingOfIntegers K}
{ε : (NumberField.RingOfIntegers K)ˣ}
{m : ℕ}
(e : x ^ p + y ^ p = ↑ε * ((hζ.toInteger - 1) ^ (m + 1) * z) ^ p)
(hy : ¬hζ.toInteger - 1 ∣ y)
(hz : ¬hζ.toInteger - 1 ∣ z)
(η : ↥(Polynomial.nthRootsFinset p 1))
[hpri : Fact (Nat.Prime p)]
[IsCyclotomicExtension {p} ℚ K]
[Fintype (ClassGroup (NumberField.RingOfIntegers K))]
(hreg : p.Coprime (Fintype.card (ClassGroup (NumberField.RingOfIntegers K))))
(hη : η ≠ zetaSubOneDvdRoot hp hζ e hy)
:
Associated
((x + y * ↑(zetaSubOneDvdRoot hp hζ e hy)) * (fun (η : ↥(Polynomial.nthRootsFinset p 1)) => aDivAZeroNum hp hζ e hy hz η hreg) η hη ^ p)
((x + y * ↑η) * (hζ.toInteger - 1) ^ (m * p) * (fun (η : ↥(Polynomial.nthRootsFinset p 1)) => aDivAZeroDenom hp hζ e hy hz η hreg) η hη ^ p)
noncomputable def
associatedEtaZeroUnit
{K : Type}
{p : ℕ}
[NeZero p]
[Field K]
[NumberField K]
(hp : p ≠ 2)
{ζ : K}
(hζ : IsPrimitiveRoot ζ p)
{x y z : NumberField.RingOfIntegers K}
{ε : (NumberField.RingOfIntegers K)ˣ}
{m : ℕ}
(e : x ^ p + y ^ p = ↑ε * ((hζ.toInteger - 1) ^ (m + 1) * z) ^ p)
(hy : ¬hζ.toInteger - 1 ∣ y)
(hz : ¬hζ.toInteger - 1 ∣ z)
(η : ↥(Polynomial.nthRootsFinset p 1))
[hpri : Fact (Nat.Prime p)]
[IsCyclotomicExtension {p} ℚ K]
[Fintype (ClassGroup (NumberField.RingOfIntegers K))]
(hreg : p.Coprime (Fintype.card (ClassGroup (NumberField.RingOfIntegers K))))
(hη : η ≠ zetaSubOneDvdRoot hp hζ e hy)
:
The unit witnessing the association in associated_eta_zero.
Equations
- associatedEtaZeroUnit hp hζ e hy hz η hreg hη = Exists.choose ⋯
Instances For
theorem
associated_eta_zero_unit_spec
{K : Type}
{p : ℕ}
[NeZero p]
[Field K]
[NumberField K]
(hp : p ≠ 2)
{ζ : K}
(hζ : IsPrimitiveRoot ζ p)
{x y z : NumberField.RingOfIntegers K}
{ε : (NumberField.RingOfIntegers K)ˣ}
{m : ℕ}
(e : x ^ p + y ^ p = ↑ε * ((hζ.toInteger - 1) ^ (m + 1) * z) ^ p)
(hy : ¬hζ.toInteger - 1 ∣ y)
(hz : ¬hζ.toInteger - 1 ∣ z)
[hpri : Fact (Nat.Prime p)]
[IsCyclotomicExtension {p} ℚ K]
[Fintype (ClassGroup (NumberField.RingOfIntegers K))]
(hreg : p.Coprime (Fintype.card (ClassGroup (NumberField.RingOfIntegers K))))
(η : ↥(Polynomial.nthRootsFinset p 1))
(hη : η ≠ zetaSubOneDvdRoot hp hζ e hy)
:
↑((fun (η : ↥(Polynomial.nthRootsFinset p 1)) => associatedEtaZeroUnit hp hζ e hy hz η hreg) η hη) * (x + y * ↑(zetaSubOneDvdRoot hp hζ e hy)) * (fun (η : ↥(Polynomial.nthRootsFinset p 1)) => aDivAZeroNum hp hζ e hy hz η hreg) η hη ^ p = (x + y * ↑η) * (hζ.toInteger - 1) ^ (m * p) * (fun (η : ↥(Polynomial.nthRootsFinset p 1)) => aDivAZeroDenom hp hζ e hy hz η hreg) η hη ^ p
theorem
formula
{K : Type}
{p : ℕ}
[NeZero p]
[Field K]
[NumberField K]
(hp : p ≠ 2)
{ζ : K}
(hζ : IsPrimitiveRoot ζ p)
{x y z : NumberField.RingOfIntegers K}
{ε : (NumberField.RingOfIntegers K)ˣ}
{m : ℕ}
(e : x ^ p + y ^ p = ↑ε * ((hζ.toInteger - 1) ^ (m + 1) * z) ^ p)
(hy : ¬hζ.toInteger - 1 ∣ y)
(hz : ¬hζ.toInteger - 1 ∣ z)
[hpri : Fact (Nat.Prime p)]
[IsCyclotomicExtension {p} ℚ K]
[Fintype (ClassGroup (NumberField.RingOfIntegers K))]
(hreg : p.Coprime (Fintype.card (ClassGroup (NumberField.RingOfIntegers K))))
(η₁ : ↥(Polynomial.nthRootsFinset p 1))
(hη₁ : η₁ ≠ zetaSubOneDvdRoot hp hζ e hy)
(η₂ : ↥(Polynomial.nthRootsFinset p 1))
(hη₂ : η₂ ≠ zetaSubOneDvdRoot hp hζ e hy)
:
(↑η₂ - ↑(zetaSubOneDvdRoot hp hζ e hy)) * ↑((fun (η : ↥(Polynomial.nthRootsFinset p 1)) => associatedEtaZeroUnit hp hζ e hy hz η hreg) η₁ hη₁) * ((fun (η : ↥(Polynomial.nthRootsFinset p 1)) => aDivAZeroNum hp hζ e hy hz η hreg) η₁ hη₁ * (fun (η : ↥(Polynomial.nthRootsFinset p 1)) => aDivAZeroDenom hp hζ e hy hz η hreg) η₂ hη₂) ^ p + (↑(zetaSubOneDvdRoot hp hζ e hy) - ↑η₁) * ↑((fun (η : ↥(Polynomial.nthRootsFinset p 1)) => associatedEtaZeroUnit hp hζ e hy hz η hreg) η₂ hη₂) * ((fun (η : ↥(Polynomial.nthRootsFinset p 1)) => aDivAZeroNum hp hζ e hy hz η hreg) η₂ hη₂ * (fun (η : ↥(Polynomial.nthRootsFinset p 1)) => aDivAZeroDenom hp hζ e hy hz η hreg) η₁ hη₁) ^ p = (↑η₂ - ↑η₁) * ((hζ.toInteger - 1) ^ m * ((fun (η : ↥(Polynomial.nthRootsFinset p 1)) => aDivAZeroDenom hp hζ e hy hz η hreg) η₁ hη₁ * (fun (η : ↥(Polynomial.nthRootsFinset p 1)) => aDivAZeroDenom hp hζ e hy hz η hreg) η₂ hη₂)) ^ p
theorem
exists_solution
{K : Type}
{p : ℕ}
[NeZero p]
[Field K]
[NumberField K]
(hp : p ≠ 2)
{ζ : K}
(hζ : IsPrimitiveRoot ζ p)
{x y z : NumberField.RingOfIntegers K}
{ε : (NumberField.RingOfIntegers K)ˣ}
{m : ℕ}
(e : x ^ p + y ^ p = ↑ε * ((hζ.toInteger - 1) ^ (m + 1) * z) ^ p)
(hy : ¬hζ.toInteger - 1 ∣ y)
(hz : ¬hζ.toInteger - 1 ∣ z)
[hpri : Fact (Nat.Prime p)]
[IsCyclotomicExtension {p} ℚ K]
[Fintype (ClassGroup (NumberField.RingOfIntegers K))]
(hreg : p.Coprime (Fintype.card (ClassGroup (NumberField.RingOfIntegers K))))
:
∃ (x' : NumberField.RingOfIntegers K) (y' : NumberField.RingOfIntegers K) (z' : NumberField.RingOfIntegers K) (ε₁ :
(NumberField.RingOfIntegers K)ˣ) (ε₂ : (NumberField.RingOfIntegers K)ˣ) (ε₃ : (NumberField.RingOfIntegers K)ˣ),
¬hζ.toInteger - 1 ∣ x' ∧ ¬hζ.toInteger - 1 ∣ y' ∧ ¬hζ.toInteger - 1 ∣ z' ∧ ↑ε₁ * x' ^ p + ↑ε₂ * y' ^ p = ↑ε₃ * ((hζ.toInteger - 1) ^ m * z') ^ p
theorem
exists_solution'
{K : Type}
{p : ℕ}
[NeZero p]
[Field K]
[NumberField K]
(hp : p ≠ 2)
{ζ : K}
(hζ : IsPrimitiveRoot ζ p)
{x y z : NumberField.RingOfIntegers K}
{ε : (NumberField.RingOfIntegers K)ˣ}
{m : ℕ}
(e : x ^ p + y ^ p = ↑ε * ((hζ.toInteger - 1) ^ (m + 1) * z) ^ p)
(hy : ¬hζ.toInteger - 1 ∣ y)
(hz : ¬hζ.toInteger - 1 ∣ z)
[hpri : Fact (Nat.Prime p)]
[IsCyclotomicExtension {p} ℚ K]
[Fintype (ClassGroup (NumberField.RingOfIntegers K))]
(hreg : p.Coprime (Fintype.card (ClassGroup (NumberField.RingOfIntegers K))))
: