theorem zeta_sub_one_dvd {K : Type u_1} {p : ℕ+} [Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) {x : { x // x ∈ NumberField.ringOfIntegers K }} {y : { x // x ∈ NumberField.ringOfIntegers K }} {z : { x // x ∈ NumberField.ringOfIntegers K }} {ε : { x // x ∈ NumberField.ringOfIntegers K }ˣ} {m : ℕ} (e : x ^ ↑p + y ^ ↑p = ↑ε * ((↑(IsPrimitiveRoot.unit' hζ) - 1) ^ (m + 1) * z) ^ ↑p) : ↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ x ^ ↑p + y ^ ↑p

theorem one_sub_zeta_dvd_zeta_pow_sub {K : Type u_1} {p : ℕ+} [hpri : Fact (PNat.Prime p)] [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] (hp : p ≠ 2) {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) {x : { x // x ∈ NumberField.ringOfIntegers K }} {y : { x // x ∈ NumberField.ringOfIntegers K }} {z : { x // x ∈ NumberField.ringOfIntegers K }} {ε : { x // x ∈ NumberField.ringOfIntegers K }ˣ} {m : ℕ} (e : x ^ ↑p + y ^ ↑p = ↑ε * ((↑(IsPrimitiveRoot.unit' hζ) - 1) ^ (m + 1) * z) ^ ↑p) (η : { x // x ∈ Polynomial.nthRootsFinset ↑p { x // x ∈ NumberField.ringOfIntegers K } }) : ↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ x + y * ↑η

theorem div_one_sub_zeta_mem {K : Type u_1} {p : ℕ+} [hpri : Fact (PNat.Prime p)] [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] (hp : p ≠ 2) {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) {x : { x // x ∈ NumberField.ringOfIntegers K }} {y : { x // x ∈ NumberField.ringOfIntegers K }} {z : { x // x ∈ NumberField.ringOfIntegers K }} {ε : { x // x ∈ NumberField.ringOfIntegers K }ˣ} {m : ℕ} (e : x ^ ↑p + y ^ ↑p = ↑ε * ((↑(IsPrimitiveRoot.unit' hζ) - 1) ^ (m + 1) * z) ^ ↑p) (η : { x // x ∈ Polynomial.nthRootsFinset ↑p { x // x ∈ NumberField.ringOfIntegers K } }) : ↑(x + y * ↑η) / (ζ - 1) ∈ NumberField.ringOfIntegers K

def div_zeta_sub_one {K : Type u_1} {p : ℕ+} [hpri : Fact (PNat.Prime p)] [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] (hp : p ≠ 2) {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) {x : { x // x ∈ NumberField.ringOfIntegers K }} {y : { x // x ∈ NumberField.ringOfIntegers K }} {z : { x // x ∈ NumberField.ringOfIntegers K }} {ε : { x // x ∈ NumberField.ringOfIntegers K }ˣ} {m : ℕ} (e : x ^ ↑p + y ^ ↑p = ↑ε * ((↑(IsPrimitiveRoot.unit' hζ) - 1) ^ (m + 1) * z) ^ ↑p) : { x // x ∈ Polynomial.nthRootsFinset ↑p { x // x ∈ NumberField.ringOfIntegers K } } → { x // x ∈ NumberField.ringOfIntegers K }

Equations

• div_zeta_sub_one hp hζ e η = { val := (↑x + ↑y * ↑↑η) / (ζ - 1), property := (_ : ↑(x + y * ↑η) / (ζ - 1) ∈ NumberField.ringOfIntegers K) }

theorem div_zeta_sub_one_mul_zeta_sub_one {K : Type u_1} {p : ℕ+} [hpri : Fact (PNat.Prime p)] [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] (hp : p ≠ 2) {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) {x : { x // x ∈ NumberField.ringOfIntegers K }} {y : { x // x ∈ NumberField.ringOfIntegers K }} {z : { x // x ∈ NumberField.ringOfIntegers K }} {ε : { x // x ∈ NumberField.ringOfIntegers K }ˣ} {m : ℕ} (e : x ^ ↑p + y ^ ↑p = ↑ε * ((↑(IsPrimitiveRoot.unit' hζ) - 1) ^ (m + 1) * z) ^ ↑p) (η : { x // x ∈ Polynomial.nthRootsFinset ↑p { x // x ∈ NumberField.ringOfIntegers K } }) : div_zeta_sub_one hp hζ e η * (↑(IsPrimitiveRoot.unit' hζ) - 1) = x + y * ↑η

theorem div_zeta_sub_one_sub {K : Type u_1} {p : ℕ+} [hpri : Fact (PNat.Prime p)] [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] (hp : p ≠ 2) {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) {x : { x // x ∈ NumberField.ringOfIntegers K }} {y : { x // x ∈ NumberField.ringOfIntegers K }} {z : { x // x ∈ NumberField.ringOfIntegers K }} {ε : { x // x ∈ NumberField.ringOfIntegers K }ˣ} {m : ℕ} (e : x ^ ↑p + y ^ ↑p = ↑ε * ((↑(IsPrimitiveRoot.unit' hζ) - 1) ^ (m + 1) * z) ^ ↑p) (η₁ : { x // x ∈ Polynomial.nthRootsFinset ↑p { x // x ∈ NumberField.ringOfIntegers K } }) (η₂ : { x // x ∈ Polynomial.nthRootsFinset ↑p { x // x ∈ NumberField.ringOfIntegers K } }) (hη : η₁ ≠ η₂) : Associated y (div_zeta_sub_one hp hζ e η₁ - div_zeta_sub_one hp hζ e η₂)

theorem div_zeta_sub_one_Injective {K : Type u_1} {p : ℕ+} [hpri : Fact (PNat.Prime p)] [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] (hp : p ≠ 2) {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) {x : { x // x ∈ NumberField.ringOfIntegers K }} {y : { x // x ∈ NumberField.ringOfIntegers K }} {z : { x // x ∈ NumberField.ringOfIntegers K }} {ε : { x // x ∈ NumberField.ringOfIntegers K }ˣ} {m : ℕ} (e : x ^ ↑p + y ^ ↑p = ↑ε * ((↑(IsPrimitiveRoot.unit' hζ) - 1) ^ (m + 1) * z) ^ ↑p) (hy : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ y) : Function.Injective fun η => ↑(Ideal.Quotient.mk (Ideal.span {↑(IsPrimitiveRoot.unit' hζ) - 1})) (div_zeta_sub_one hp hζ e η)

instance instFiniteQuotientSubtypeMemSubalgebraIntToCommSemiringInstCommRingIntToSemiringToCommSemiringToCommRingToEuclideanDomainAlgebraIntToRingToDivisionRingInstMembershipInstSetLikeSubalgebraRingOfIntegersIdealToSemiringInstHasQuotientIdealToSemiringToCommSemiringToCommRingSpanSingletonSetInstSingletonSetHSubInstHSubSubToSubNegMonoidToAddGroupToAddGroupWithOneAddSubgroupClassInstSubringClassSubalgebraToCommSemiringToSemiringInstSetLikeSubalgebraValToMonoidToMonoidToMonoidWithZeroToSemiringToDivisionSemiringToSemifieldToSubmonoidToNonAssocSemiringToSubsemiringUnit'OfNat {K : Type u_1} {p : ℕ+} [hpri : Fact (PNat.Prime p)] [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) : Finite ({ x // x ∈ NumberField.ringOfIntegers K } ⧸ Ideal.span {↑(IsPrimitiveRoot.unit' hζ) - 1})

Equations

• One or more equations did not get rendered due to their size.

theorem div_zeta_sub_one_Bijective {K : Type u_1} {p : ℕ+} [hpri : Fact (PNat.Prime p)] [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] (hp : p ≠ 2) {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) {x : { x // x ∈ NumberField.ringOfIntegers K }} {y : { x // x ∈ NumberField.ringOfIntegers K }} {z : { x // x ∈ NumberField.ringOfIntegers K }} {ε : { x // x ∈ NumberField.ringOfIntegers K }ˣ} {m : ℕ} (e : x ^ ↑p + y ^ ↑p = ↑ε * ((↑(IsPrimitiveRoot.unit' hζ) - 1) ^ (m + 1) * z) ^ ↑p) (hy : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ y) : Function.Bijective fun η => ↑(Ideal.Quotient.mk (Ideal.span {↑(IsPrimitiveRoot.unit' hζ) - 1})) (div_zeta_sub_one hp hζ e η)

theorem div_zeta_sub_one_eq_zero_iff {K : Type u_1} {p : ℕ+} [hpri : Fact (PNat.Prime p)] [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] (hp : p ≠ 2) {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) {x : { x // x ∈ NumberField.ringOfIntegers K }} {y : { x // x ∈ NumberField.ringOfIntegers K }} {z : { x // x ∈ NumberField.ringOfIntegers K }} {ε : { x // x ∈ NumberField.ringOfIntegers K }ˣ} {m : ℕ} (e : x ^ ↑p + y ^ ↑p = ↑ε * ((↑(IsPrimitiveRoot.unit' hζ) - 1) ^ (m + 1) * z) ^ ↑p) (η : { x // x ∈ Polynomial.nthRootsFinset ↑p { x // x ∈ NumberField.ringOfIntegers K } }) : ↑(Ideal.Quotient.mk (Ideal.span {↑(IsPrimitiveRoot.unit' hζ) - 1})) (div_zeta_sub_one hp hζ e η) = 0 ↔ (↑(IsPrimitiveRoot.unit' hζ) - 1) ^ 2 ∣ x + y * ↑η

theorem existsUnique_zeta_sub_one_pow_two_dvd {K : Type u_1} {p : ℕ+} [hpri : Fact (PNat.Prime p)] [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] (hp : p ≠ 2) {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) {x : { x // x ∈ NumberField.ringOfIntegers K }} {y : { x // x ∈ NumberField.ringOfIntegers K }} {z : { x // x ∈ NumberField.ringOfIntegers K }} {ε : { x // x ∈ NumberField.ringOfIntegers K }ˣ} {m : ℕ} (e : x ^ ↑p + y ^ ↑p = ↑ε * ((↑(IsPrimitiveRoot.unit' hζ) - 1) ^ (m + 1) * z) ^ ↑p) (hy : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ y) : ∃! η, (↑(IsPrimitiveRoot.unit' hζ) - 1) ^ 2 ∣ x + y * ↑η

theorem gcd_zeta_sub_one_eq_one {K : Type u_1} {p : ℕ+} [hpri : Fact (PNat.Prime p)] [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] (hp : p ≠ 2) {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) {x : { x // x ∈ NumberField.ringOfIntegers K }} {y : { x // x ∈ NumberField.ringOfIntegers K }} (hy : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ y) : gcd (gcd (Ideal.span {x}) (Ideal.span {y})) (Ideal.span {↑(IsPrimitiveRoot.unit' hζ) - 1}) = 1

theorem gcd_div_div_zeta_sub_one {K : Type u_1} {p : ℕ+} [hpri : Fact (PNat.Prime p)] [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] (hp : p ≠ 2) {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) {x : { x // x ∈ NumberField.ringOfIntegers K }} {y : { x // x ∈ NumberField.ringOfIntegers K }} {z : { x // x ∈ NumberField.ringOfIntegers K }} {ε : { x // x ∈ NumberField.ringOfIntegers K }ˣ} {m : ℕ} (e : x ^ ↑p + y ^ ↑p = ↑ε * ((↑(IsPrimitiveRoot.unit' hζ) - 1) ^ (m + 1) * z) ^ ↑p) (hy : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ y) (η : { x // x ∈ Polynomial.nthRootsFinset ↑p { x // x ∈ NumberField.ringOfIntegers K } }) : gcd (Ideal.span {x}) (Ideal.span {y}) ∣ Ideal.span {div_zeta_sub_one hp hζ e η}

noncomputable def div_zeta_sub_one_dvd_gcd {K : Type u_1} {p : ℕ+} [hpri : Fact (PNat.Prime p)] [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] (hp : p ≠ 2) {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) {x : { x // x ∈ NumberField.ringOfIntegers K }} {y : { x // x ∈ NumberField.ringOfIntegers K }} {z : { x // x ∈ NumberField.ringOfIntegers K }} {ε : { x // x ∈ NumberField.ringOfIntegers K }ˣ} {m : ℕ} (e : x ^ ↑p + y ^ ↑p = ↑ε * ((↑(IsPrimitiveRoot.unit' hζ) - 1) ^ (m + 1) * z) ^ ↑p) (hy : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ y) (η : { x // x ∈ Polynomial.nthRootsFinset ↑p { x // x ∈ NumberField.ringOfIntegers K } }) : Ideal { x // x ∈ NumberField.ringOfIntegers K }

Equations

• div_zeta_sub_one_dvd_gcd hp hζ e hy η = Exists.choose (_ : gcd (Ideal.span {x}) (Ideal.span {y}) ∣ Ideal.span {div_zeta_sub_one hp hζ e η})

theorem div_zeta_sub_one_dvd_gcd_spec {K : Type u_1} {p : ℕ+} [hpri : Fact (PNat.Prime p)] [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] (hp : p ≠ 2) {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) {x : { x // x ∈ NumberField.ringOfIntegers K }} {y : { x // x ∈ NumberField.ringOfIntegers K }} {z : { x // x ∈ NumberField.ringOfIntegers K }} {ε : { x // x ∈ NumberField.ringOfIntegers K }ˣ} {m : ℕ} (e : x ^ ↑p + y ^ ↑p = ↑ε * ((↑(IsPrimitiveRoot.unit' hζ) - 1) ^ (m + 1) * z) ^ ↑p) (hy : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ y) (η : { x // x ∈ Polynomial.nthRootsFinset ↑p { x // x ∈ NumberField.ringOfIntegers K } }) : gcd (Ideal.span {x}) (Ideal.span {y}) * div_zeta_sub_one_dvd_gcd hp hζ e hy η = Ideal.span {div_zeta_sub_one hp hζ e η}

theorem m_mul_c_mul_p {K : Type u_1} {p : ℕ+} [hpri : Fact (PNat.Prime p)] [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] (hp : p ≠ 2) {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) {x : { x // x ∈ NumberField.ringOfIntegers K }} {y : { x // x ∈ NumberField.ringOfIntegers K }} {z : { x // x ∈ NumberField.ringOfIntegers K }} {ε : { x // x ∈ NumberField.ringOfIntegers K }ˣ} {m : ℕ} (e : x ^ ↑p + y ^ ↑p = ↑ε * ((↑(IsPrimitiveRoot.unit' hζ) - 1) ^ (m + 1) * z) ^ ↑p) (hy : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ y) (η : { x // x ∈ Polynomial.nthRootsFinset ↑p { x // x ∈ NumberField.ringOfIntegers K } }) : gcd (Ideal.span {x}) (Ideal.span {y}) * div_zeta_sub_one_dvd_gcd hp hζ e hy η * Ideal.span {↑(IsPrimitiveRoot.unit' hζ) - 1} = Ideal.span {x + y * ↑η}

theorem m_ne_zero {K : Type u_1} {p : ℕ+} [Field K] [NumberField K] {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) {x : { x // x ∈ NumberField.ringOfIntegers K }} {y : { x // x ∈ NumberField.ringOfIntegers K }} {z : { x // x ∈ NumberField.ringOfIntegers K }} {ε : { x // x ∈ NumberField.ringOfIntegers K }ˣ} {m : ℕ} (e : x ^ ↑p + y ^ ↑p = ↑ε * ((↑(IsPrimitiveRoot.unit' hζ) - 1) ^ (m + 1) * z) ^ ↑p) (hy : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ y) : gcd (Ideal.span {x}) (Ideal.span {y}) ≠ 0

theorem p_ne_zero {K : Type u_1} {p : ℕ+} [hpri : Fact (PNat.Prime p)] [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) : Ideal.span {↑(IsPrimitiveRoot.unit' hζ) - 1} ≠ 0

theorem coprime_c_aux {K : Type u_1} {p : ℕ+} [hpri : Fact (PNat.Prime p)] [Field K] [NumberField K] {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) {x : { x // x ∈ NumberField.ringOfIntegers K }} {y : { x // x ∈ NumberField.ringOfIntegers K }} (η₁ : { x // x ∈ Polynomial.nthRootsFinset ↑p { x // x ∈ NumberField.ringOfIntegers K } }) (η₂ : { x // x ∈ Polynomial.nthRootsFinset ↑p { x // x ∈ NumberField.ringOfIntegers K } }) (hη : η₁ ≠ η₂) : Ideal.span {x + y * ↑η₁} ⊔ Ideal.span {x + y * ↑η₂} ∣ gcd (Ideal.span {x}) (Ideal.span {y}) * Ideal.span {↑(IsPrimitiveRoot.unit' hζ) - 1}

theorem coprime_c {K : Type u_1} {p : ℕ+} [hpri : Fact (PNat.Prime p)] [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] (hp : p ≠ 2) {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) {x : { x // x ∈ NumberField.ringOfIntegers K }} {y : { x // x ∈ NumberField.ringOfIntegers K }} {z : { x // x ∈ NumberField.ringOfIntegers K }} {ε : { x // x ∈ NumberField.ringOfIntegers K }ˣ} {m : ℕ} (e : x ^ ↑p + y ^ ↑p = ↑ε * ((↑(IsPrimitiveRoot.unit' hζ) - 1) ^ (m + 1) * z) ^ ↑p) (hy : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ y) (η₁ : { x // x ∈ Polynomial.nthRootsFinset ↑p { x // x ∈ NumberField.ringOfIntegers K } }) (η₂ : { x // x ∈ Polynomial.nthRootsFinset ↑p { x // x ∈ NumberField.ringOfIntegers K } }) (hη : η₁ ≠ η₂) : IsCoprime (div_zeta_sub_one_dvd_gcd hp hζ e hy η₁) (div_zeta_sub_one_dvd_gcd hp hζ e hy η₂)

theorem span_pow_add_pow_eq {K : Type u_1} {p : ℕ+} [Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) {x : { x // x ∈ NumberField.ringOfIntegers K }} {y : { x // x ∈ NumberField.ringOfIntegers K }} {z : { x // x ∈ NumberField.ringOfIntegers K }} {ε : { x // x ∈ NumberField.ringOfIntegers K }ˣ} {m : ℕ} (e : x ^ ↑p + y ^ ↑p = ↑ε * ((↑(IsPrimitiveRoot.unit' hζ) - 1) ^ (m + 1) * z) ^ ↑p) : Ideal.span {x ^ ↑p + y ^ ↑p} = (Ideal.span {↑(IsPrimitiveRoot.unit' hζ) - 1} ^ (m + 1) * Ideal.span {z}) ^ ↑p

theorem gcd_m_p_pow_eq_one {K : Type u_1} {p : ℕ+} [hpri : Fact (PNat.Prime p)] [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] (hp : p ≠ 2) {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) {x : { x // x ∈ NumberField.ringOfIntegers K }} {y : { x // x ∈ NumberField.ringOfIntegers K }} {m : ℕ} (hy : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ y) : gcd (gcd (Ideal.span {x}) (Ideal.span {y})) (Ideal.span {↑(IsPrimitiveRoot.unit' hζ) - 1} ^ (m + 1)) = 1

theorem m_dvd_z {K : Type u_1} {p : ℕ+} [hpri : Fact (PNat.Prime p)] [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] (hp : p ≠ 2) {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) {x : { x // x ∈ NumberField.ringOfIntegers K }} {y : { x // x ∈ NumberField.ringOfIntegers K }} {z : { x // x ∈ NumberField.ringOfIntegers K }} {ε : { x // x ∈ NumberField.ringOfIntegers K }ˣ} {m : ℕ} (e : x ^ ↑p + y ^ ↑p = ↑ε * ((↑(IsPrimitiveRoot.unit' hζ) - 1) ^ (m + 1) * z) ^ ↑p) (hy : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ y) : gcd (Ideal.span {x}) (Ideal.span {y}) ∣ Ideal.span {z}

noncomputable def z_div_m {K : Type u_1} {p : ℕ+} [hpri : Fact (PNat.Prime p)] [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] (hp : p ≠ 2) {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) {x : { x // x ∈ NumberField.ringOfIntegers K }} {y : { x // x ∈ NumberField.ringOfIntegers K }} {z : { x // x ∈ NumberField.ringOfIntegers K }} {ε : { x // x ∈ NumberField.ringOfIntegers K }ˣ} {m : ℕ} (e : x ^ ↑p + y ^ ↑p = ↑ε * ((↑(IsPrimitiveRoot.unit' hζ) - 1) ^ (m + 1) * z) ^ ↑p) (hy : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ y) : Ideal { x // x ∈ NumberField.ringOfIntegers K }

Equations

• z_div_m hp hζ e hy = Exists.choose (_ : gcd (Ideal.span {x}) (Ideal.span {y}) ∣ Ideal.span {z})

theorem z_div_m_spec {K : Type u_1} {p : ℕ+} [hpri : Fact (PNat.Prime p)] [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] (hp : p ≠ 2) {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) {x : { x // x ∈ NumberField.ringOfIntegers K }} {y : { x // x ∈ NumberField.ringOfIntegers K }} {z : { x // x ∈ NumberField.ringOfIntegers K }} {ε : { x // x ∈ NumberField.ringOfIntegers K }ˣ} {m : ℕ} (e : x ^ ↑p + y ^ ↑p = ↑ε * ((↑(IsPrimitiveRoot.unit' hζ) - 1) ^ (m + 1) * z) ^ ↑p) (hy : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ y) : Ideal.span {z} = gcd (Ideal.span {x}) (Ideal.span {y}) * z_div_m hp hζ e hy

theorem exists_ideal_pow_eq_c_aux {K : Type u_1} {p : ℕ+} [hpri : Fact (PNat.Prime p)] [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] (hp : p ≠ 2) {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) {x : { x // x ∈ NumberField.ringOfIntegers K }} {y : { x // x ∈ NumberField.ringOfIntegers K }} {z : { x // x ∈ NumberField.ringOfIntegers K }} {ε : { x // x ∈ NumberField.ringOfIntegers K }ˣ} {m : ℕ} (e : x ^ ↑p + y ^ ↑p = ↑ε * ((↑(IsPrimitiveRoot.unit' hζ) - 1) ^ (m + 1) * z) ^ ↑p) (hy : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ y) : gcd (Ideal.span {x}) (Ideal.span {y}) ^ ↑p * (z_div_m hp hζ e hy * Ideal.span {↑(IsPrimitiveRoot.unit' hζ) - 1} ^ m) ^ ↑p * Ideal.span {↑(IsPrimitiveRoot.unit' hζ) - 1} ^ ↑p = (Ideal.span {↑(IsPrimitiveRoot.unit' hζ) - 1} ^ (m + 1) * Ideal.span {z}) ^ ↑p

theorem prod_c {K : Type u_1} {p : ℕ+} [hpri : Fact (PNat.Prime p)] [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] (hp : p ≠ 2) {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) {x : { x // x ∈ NumberField.ringOfIntegers K }} {y : { x // x ∈ NumberField.ringOfIntegers K }} {z : { x // x ∈ NumberField.ringOfIntegers K }} {ε : { x // x ∈ NumberField.ringOfIntegers K }ˣ} {m : ℕ} (e : x ^ ↑p + y ^ ↑p = ↑ε * ((↑(IsPrimitiveRoot.unit' hζ) - 1) ^ (m + 1) * z) ^ ↑p) (hy : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ y) : (Finset.prod (Finset.attach (Polynomial.nthRootsFinset ↑p { x // x ∈ NumberField.ringOfIntegers K })) fun η => div_zeta_sub_one_dvd_gcd hp hζ e hy η) = (z_div_m hp hζ e hy * Ideal.span {↑(IsPrimitiveRoot.unit' hζ) - 1} ^ m) ^ ↑p

theorem exists_ideal_pow_eq_c {K : Type u_1} {p : ℕ+} [hpri : Fact (PNat.Prime p)] [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] (hp : p ≠ 2) {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) {x : { x // x ∈ NumberField.ringOfIntegers K }} {y : { x // x ∈ NumberField.ringOfIntegers K }} {z : { x // x ∈ NumberField.ringOfIntegers K }} {ε : { x // x ∈ NumberField.ringOfIntegers K }ˣ} {m : ℕ} (e : x ^ ↑p + y ^ ↑p = ↑ε * ((↑(IsPrimitiveRoot.unit' hζ) - 1) ^ (m + 1) * z) ^ ↑p) (hy : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ y) (η : { x // x ∈ Polynomial.nthRootsFinset ↑p { x // x ∈ NumberField.ringOfIntegers K } }) : ∃ I, div_zeta_sub_one_dvd_gcd hp hζ e hy η = I ^ ↑p

noncomputable def root_div_zeta_sub_one_dvd_gcd {K : Type u_1} {p : ℕ+} [hpri : Fact (PNat.Prime p)] [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] (hp : p ≠ 2) {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) {x : { x // x ∈ NumberField.ringOfIntegers K }} {y : { x // x ∈ NumberField.ringOfIntegers K }} {z : { x // x ∈ NumberField.ringOfIntegers K }} {ε : { x // x ∈ NumberField.ringOfIntegers K }ˣ} {m : ℕ} (e : x ^ ↑p + y ^ ↑p = ↑ε * ((↑(IsPrimitiveRoot.unit' hζ) - 1) ^ (m + 1) * z) ^ ↑p) (hy : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ y) (η : { x // x ∈ Polynomial.nthRootsFinset ↑p { x // x ∈ NumberField.ringOfIntegers K } }) : Ideal { x // x ∈ NumberField.ringOfIntegers K }

Equations

• root_div_zeta_sub_one_dvd_gcd hp hζ e hy η = Exists.choose (_ : ∃ I, div_zeta_sub_one_dvd_gcd hp hζ e hy η = I ^ ↑p)

theorem root_div_zeta_sub_one_dvd_gcd_spec {K : Type u_1} {p : ℕ+} [hpri : Fact (PNat.Prime p)] [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] (hp : p ≠ 2) {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) {x : { x // x ∈ NumberField.ringOfIntegers K }} {y : { x // x ∈ NumberField.ringOfIntegers K }} {z : { x // x ∈ NumberField.ringOfIntegers K }} {ε : { x // x ∈ NumberField.ringOfIntegers K }ˣ} {m : ℕ} (e : x ^ ↑p + y ^ ↑p = ↑ε * ((↑(IsPrimitiveRoot.unit' hζ) - 1) ^ (m + 1) * z) ^ ↑p) (hy : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ y) (η : { x // x ∈ Polynomial.nthRootsFinset ↑p { x // x ∈ NumberField.ringOfIntegers K } }) : root_div_zeta_sub_one_dvd_gcd hp hζ e hy η ^ ↑p = div_zeta_sub_one_dvd_gcd hp hζ e hy η

theorem c_div_principal_aux {K : Type u_1} {p : ℕ+} [hpri : Fact (PNat.Prime p)] [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] (hp : p ≠ 2) {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) {x : { x // x ∈ NumberField.ringOfIntegers K }} {y : { x // x ∈ NumberField.ringOfIntegers K }} {z : { x // x ∈ NumberField.ringOfIntegers K }} {ε : { x // x ∈ NumberField.ringOfIntegers K }ˣ} {m : ℕ} (e : x ^ ↑p + y ^ ↑p = ↑ε * ((↑(IsPrimitiveRoot.unit' hζ) - 1) ^ (m + 1) * z) ^ ↑p) (hy : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ y) (η₁ : { x // x ∈ Polynomial.nthRootsFinset ↑p { x // x ∈ NumberField.ringOfIntegers K } }) (η₂ : { x // x ∈ Polynomial.nthRootsFinset ↑p { x // x ∈ NumberField.ringOfIntegers K } }) : ↑(Ideal.span {x + y * ↑η₁}) / ↑(Ideal.span {x + y * ↑η₂}) = ↑(div_zeta_sub_one_dvd_gcd hp hζ e hy η₁) / ↑(div_zeta_sub_one_dvd_gcd hp hζ e hy η₂)

theorem c_div_principal {K : Type u_1} {p : ℕ+} [hpri : Fact (PNat.Prime p)] [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] (hp : p ≠ 2) {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) {x : { x // x ∈ NumberField.ringOfIntegers K }} {y : { x // x ∈ NumberField.ringOfIntegers K }} {z : { x // x ∈ NumberField.ringOfIntegers K }} {ε : { x // x ∈ NumberField.ringOfIntegers K }ˣ} {m : ℕ} (e : x ^ ↑p + y ^ ↑p = ↑ε * ((↑(IsPrimitiveRoot.unit' hζ) - 1) ^ (m + 1) * z) ^ ↑p) (hy : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ y) (η₁ : { x // x ∈ Polynomial.nthRootsFinset ↑p { x // x ∈ NumberField.ringOfIntegers K } }) (η₂ : { x // x ∈ Polynomial.nthRootsFinset ↑p { x // x ∈ NumberField.ringOfIntegers K } }) : Submodule.IsPrincipal ↑(↑(div_zeta_sub_one_dvd_gcd hp hζ e hy η₁) / ↑(div_zeta_sub_one_dvd_gcd hp hζ e hy η₂))

theorem a_div_principal {K : Type u_1} {p : ℕ+} [hpri : Fact (PNat.Prime p)] [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] (hp : p ≠ 2) [Fintype (ClassGroup { x // x ∈ NumberField.ringOfIntegers K })] (hreg : Nat.Coprime (↑p) (Fintype.card (ClassGroup { x // x ∈ NumberField.ringOfIntegers K }))) {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) {x : { x // x ∈ NumberField.ringOfIntegers K }} {y : { x // x ∈ NumberField.ringOfIntegers K }} {z : { x // x ∈ NumberField.ringOfIntegers K }} {ε : { x // x ∈ NumberField.ringOfIntegers K }ˣ} {m : ℕ} (e : x ^ ↑p + y ^ ↑p = ↑ε * ((↑(IsPrimitiveRoot.unit' hζ) - 1) ^ (m + 1) * z) ^ ↑p) (hy : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ y) (η₁ : { x // x ∈ Polynomial.nthRootsFinset ↑p { x // x ∈ NumberField.ringOfIntegers K } }) (η₂ : { x // x ∈ Polynomial.nthRootsFinset ↑p { x // x ∈ NumberField.ringOfIntegers K } }) : Submodule.IsPrincipal ↑(↑(root_div_zeta_sub_one_dvd_gcd hp hζ e hy η₁) / ↑(root_div_zeta_sub_one_dvd_gcd hp hζ e hy η₂))

noncomputable def zeta_sub_one_dvd_root {K : Type u_1} {p : ℕ+} [hpri : Fact (PNat.Prime p)] [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] (hp : p ≠ 2) {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) {x : { x // x ∈ NumberField.ringOfIntegers K }} {y : { x // x ∈ NumberField.ringOfIntegers K }} {z : { x // x ∈ NumberField.ringOfIntegers K }} {ε : { x // x ∈ NumberField.ringOfIntegers K }ˣ} {m : ℕ} (e : x ^ ↑p + y ^ ↑p = ↑ε * ((↑(IsPrimitiveRoot.unit' hζ) - 1) ^ (m + 1) * z) ^ ↑p) (hy : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ y) : { x // x ∈ Polynomial.nthRootsFinset ↑p { x // x ∈ NumberField.ringOfIntegers K } }

Equations

• One or more equations did not get rendered due to their size.

theorem zeta_sub_one_dvd_root_spec {K : Type u_1} {p : ℕ+} [hpri : Fact (PNat.Prime p)] [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] (hp : p ≠ 2) {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) {x : { x // x ∈ NumberField.ringOfIntegers K }} {y : { x // x ∈ NumberField.ringOfIntegers K }} {z : { x // x ∈ NumberField.ringOfIntegers K }} {ε : { x // x ∈ NumberField.ringOfIntegers K }ˣ} {m : ℕ} (e : x ^ ↑p + y ^ ↑p = ↑ε * ((↑(IsPrimitiveRoot.unit' hζ) - 1) ^ (m + 1) * z) ^ ↑p) (hy : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ y) : ↑(Ideal.Quotient.mk (Ideal.span {↑(IsPrimitiveRoot.unit' hζ) - 1})) (div_zeta_sub_one hp hζ e (zeta_sub_one_dvd_root hp hζ e hy)) = 0

theorem p_dvd_c_iff {K : Type u_1} {p : ℕ+} [hpri : Fact (PNat.Prime p)] [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] (hp : p ≠ 2) {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) {x : { x // x ∈ NumberField.ringOfIntegers K }} {y : { x // x ∈ NumberField.ringOfIntegers K }} {z : { x // x ∈ NumberField.ringOfIntegers K }} {ε : { x // x ∈ NumberField.ringOfIntegers K }ˣ} {m : ℕ} (e : x ^ ↑p + y ^ ↑p = ↑ε * ((↑(IsPrimitiveRoot.unit' hζ) - 1) ^ (m + 1) * z) ^ ↑p) (hy : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ y) (η : { x // x ∈ Polynomial.nthRootsFinset ↑p { x // x ∈ NumberField.ringOfIntegers K } }) : Ideal.span {↑(IsPrimitiveRoot.unit' hζ) - 1} ∣ div_zeta_sub_one_dvd_gcd hp hζ e hy η ↔ η = zeta_sub_one_dvd_root hp hζ e hy

theorem p_pow_dvd_c_eta_zero_aux {K : Type u_1} {p : ℕ+} [hpri : Fact (PNat.Prime p)] [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] (hp : p ≠ 2) {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) {x : { x // x ∈ NumberField.ringOfIntegers K }} {y : { x // x ∈ NumberField.ringOfIntegers K }} {z : { x // x ∈ NumberField.ringOfIntegers K }} {ε : { x // x ∈ NumberField.ringOfIntegers K }ˣ} {m : ℕ} (e : x ^ ↑p + y ^ ↑p = ↑ε * ((↑(IsPrimitiveRoot.unit' hζ) - 1) ^ (m + 1) * z) ^ ↑p) (hy : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ y) [DecidableEq K] : gcd (Ideal.span {↑(IsPrimitiveRoot.unit' hζ) - 1} ^ (m * ↑p)) (Finset.prod (Finset.attach (Polynomial.nthRootsFinset ↑p { x // x ∈ NumberField.ringOfIntegers K }) \ {zeta_sub_one_dvd_root hp hζ e hy}) fun η => div_zeta_sub_one_dvd_gcd hp hζ e hy η) = 1

theorem p_pow_dvd_c_eta_zero {K : Type u_1} {p : ℕ+} [hpri : Fact (PNat.Prime p)] [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] (hp : p ≠ 2) {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) {x : { x // x ∈ NumberField.ringOfIntegers K }} {y : { x // x ∈ NumberField.ringOfIntegers K }} {z : { x // x ∈ NumberField.ringOfIntegers K }} {ε : { x // x ∈ NumberField.ringOfIntegers K }ˣ} {m : ℕ} (e : x ^ ↑p + y ^ ↑p = ↑ε * ((↑(IsPrimitiveRoot.unit' hζ) - 1) ^ (m + 1) * z) ^ ↑p) (hy : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ y) : Ideal.span {↑(IsPrimitiveRoot.unit' hζ) - 1} ^ (m * ↑p) ∣ div_zeta_sub_one_dvd_gcd hp hζ e hy (zeta_sub_one_dvd_root hp hζ e hy)

theorem p_dvd_a_iff {K : Type u_1} {p : ℕ+} [hpri : Fact (PNat.Prime p)] [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] (hp : p ≠ 2) {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) {x : { x // x ∈ NumberField.ringOfIntegers K }} {y : { x // x ∈ NumberField.ringOfIntegers K }} {z : { x // x ∈ NumberField.ringOfIntegers K }} {ε : { x // x ∈ NumberField.ringOfIntegers K }ˣ} {m : ℕ} (e : x ^ ↑p + y ^ ↑p = ↑ε * ((↑(IsPrimitiveRoot.unit' hζ) - 1) ^ (m + 1) * z) ^ ↑p) (hy : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ y) (η : { x // x ∈ Polynomial.nthRootsFinset ↑p { x // x ∈ NumberField.ringOfIntegers K } }) : Ideal.span {↑(IsPrimitiveRoot.unit' hζ) - 1} ∣ root_div_zeta_sub_one_dvd_gcd hp hζ e hy η ↔ η = zeta_sub_one_dvd_root hp hζ e hy

theorem p_pow_dvd_a_eta_zero {K : Type u_1} {p : ℕ+} [hpri : Fact (PNat.Prime p)] [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] (hp : p ≠ 2) {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) {x : { x // x ∈ NumberField.ringOfIntegers K }} {y : { x // x ∈ NumberField.ringOfIntegers K }} {z : { x // x ∈ NumberField.ringOfIntegers K }} {ε : { x // x ∈ NumberField.ringOfIntegers K }ˣ} {m : ℕ} (e : x ^ ↑p + y ^ ↑p = ↑ε * ((↑(IsPrimitiveRoot.unit' hζ) - 1) ^ (m + 1) * z) ^ ↑p) (hy : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ y) : Ideal.span {↑(IsPrimitiveRoot.unit' hζ) - 1} ^ m ∣ root_div_zeta_sub_one_dvd_gcd hp hζ e hy (zeta_sub_one_dvd_root hp hζ e hy)

noncomputable def a_eta_zero_dvd_p_pow {K : Type u_1} {p : ℕ+} [hpri : Fact (PNat.Prime p)] [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] (hp : p ≠ 2) {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) {x : { x // x ∈ NumberField.ringOfIntegers K }} {y : { x // x ∈ NumberField.ringOfIntegers K }} {z : { x // x ∈ NumberField.ringOfIntegers K }} {ε : { x // x ∈ NumberField.ringOfIntegers K }ˣ} {m : ℕ} (e : x ^ ↑p + y ^ ↑p = ↑ε * ((↑(IsPrimitiveRoot.unit' hζ) - 1) ^ (m + 1) * z) ^ ↑p) (hy : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ y) : Ideal { x // x ∈ NumberField.ringOfIntegers K }

Equations

• One or more equations did not get rendered due to their size.

theorem a_eta_zero_dvd_p_pow_spec {K : Type u_1} {p : ℕ+} [hpri : Fact (PNat.Prime p)] [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] (hp : p ≠ 2) {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) {x : { x // x ∈ NumberField.ringOfIntegers K }} {y : { x // x ∈ NumberField.ringOfIntegers K }} {z : { x // x ∈ NumberField.ringOfIntegers K }} {ε : { x // x ∈ NumberField.ringOfIntegers K }ˣ} {m : ℕ} (e : x ^ ↑p + y ^ ↑p = ↑ε * ((↑(IsPrimitiveRoot.unit' hζ) - 1) ^ (m + 1) * z) ^ ↑p) (hy : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ y) : Ideal.span {↑(IsPrimitiveRoot.unit' hζ) - 1} ^ m * a_eta_zero_dvd_p_pow hp hζ e hy = root_div_zeta_sub_one_dvd_gcd hp hζ e hy (zeta_sub_one_dvd_root hp hζ e hy)

theorem not_p_div_a_zero {K : Type u_1} {p : ℕ+} [hpri : Fact (PNat.Prime p)] [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] (hp : p ≠ 2) {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) {x : { x // x ∈ NumberField.ringOfIntegers K }} {y : { x // x ∈ NumberField.ringOfIntegers K }} {z : { x // x ∈ NumberField.ringOfIntegers K }} {ε : { x // x ∈ NumberField.ringOfIntegers K }ˣ} {m : ℕ} (e : x ^ ↑p + y ^ ↑p = ↑ε * ((↑(IsPrimitiveRoot.unit' hζ) - 1) ^ (m + 1) * z) ^ ↑p) (hy : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ y) (hz : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ z) : ¬Ideal.span {↑(IsPrimitiveRoot.unit' hζ) - 1} ∣ a_eta_zero_dvd_p_pow hp hζ e hy

theorem one_le_m {K : Type u_1} {p : ℕ+} [hpri : Fact (PNat.Prime p)] [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] (hp : p ≠ 2) {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) {x : { x // x ∈ NumberField.ringOfIntegers K }} {y : { x // x ∈ NumberField.ringOfIntegers K }} {z : { x // x ∈ NumberField.ringOfIntegers K }} {ε : { x // x ∈ NumberField.ringOfIntegers K }ˣ} {m : ℕ} (e : x ^ ↑p + y ^ ↑p = ↑ε * ((↑(IsPrimitiveRoot.unit' hζ) - 1) ^ (m + 1) * z) ^ ↑p) (hy : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ y) (hz : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ z) : 1 ≤ m

theorem isPrincipal_a_div_a_zero {K : Type u_1} {p : ℕ+} [hpri : Fact (PNat.Prime p)] [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] (hp : p ≠ 2) [Fintype (ClassGroup { x // x ∈ NumberField.ringOfIntegers K })] (hreg : Nat.Coprime (↑p) (Fintype.card (ClassGroup { x // x ∈ NumberField.ringOfIntegers K }))) {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) {x : { x // x ∈ NumberField.ringOfIntegers K }} {y : { x // x ∈ NumberField.ringOfIntegers K }} {z : { x // x ∈ NumberField.ringOfIntegers K }} {ε : { x // x ∈ NumberField.ringOfIntegers K }ˣ} {m : ℕ} (e : x ^ ↑p + y ^ ↑p = ↑ε * ((↑(IsPrimitiveRoot.unit' hζ) - 1) ^ (m + 1) * z) ^ ↑p) (hy : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ y) (η : { x // x ∈ Polynomial.nthRootsFinset ↑p { x // x ∈ NumberField.ringOfIntegers K } }) : Submodule.IsPrincipal ↑(↑(root_div_zeta_sub_one_dvd_gcd hp hζ e hy η) / ↑(a_eta_zero_dvd_p_pow hp hζ e hy))

theorem exists_not_dvd_spanSingleton_eq_a_div_a_zero {K : Type u_1} {p : ℕ+} [hpri : Fact (PNat.Prime p)] [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] (hp : p ≠ 2) [Fintype (ClassGroup { x // x ∈ NumberField.ringOfIntegers K })] (hreg : Nat.Coprime (↑p) (Fintype.card (ClassGroup { x // x ∈ NumberField.ringOfIntegers K }))) {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) {x : { x // x ∈ NumberField.ringOfIntegers K }} {y : { x // x ∈ NumberField.ringOfIntegers K }} {z : { x // x ∈ NumberField.ringOfIntegers K }} {ε : { x // x ∈ NumberField.ringOfIntegers K }ˣ} {m : ℕ} (e : x ^ ↑p + y ^ ↑p = ↑ε * ((↑(IsPrimitiveRoot.unit' hζ) - 1) ^ (m + 1) * z) ^ ↑p) (hy : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ y) (hz : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ z) (η : { x // x ∈ Polynomial.nthRootsFinset ↑p { x // x ∈ NumberField.ringOfIntegers K } }) (hη : η ≠ zeta_sub_one_dvd_root hp hζ e hy) : ∃ a b, ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ a ∧ ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ b ∧ FractionalIdeal.spanSingleton (nonZeroDivisors { x // x ∈ NumberField.ringOfIntegers K }) (↑a / ↑b) = ↑(root_div_zeta_sub_one_dvd_gcd hp hζ e hy η) / ↑(a_eta_zero_dvd_p_pow hp hζ e hy)

noncomputable def a_div_a_zero_num {K : Type u_1} {p : ℕ+} [hpri : Fact (PNat.Prime p)] [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] (hp : p ≠ 2) [Fintype (ClassGroup { x // x ∈ NumberField.ringOfIntegers K })] (hreg : Nat.Coprime (↑p) (Fintype.card (ClassGroup { x // x ∈ NumberField.ringOfIntegers K }))) {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) {x : { x // x ∈ NumberField.ringOfIntegers K }} {y : { x // x ∈ NumberField.ringOfIntegers K }} {z : { x // x ∈ NumberField.ringOfIntegers K }} {ε : { x // x ∈ NumberField.ringOfIntegers K }ˣ} {m : ℕ} (e : x ^ ↑p + y ^ ↑p = ↑ε * ((↑(IsPrimitiveRoot.unit' hζ) - 1) ^ (m + 1) * z) ^ ↑p) (hy : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ y) (hz : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ z) (η : { x // x ∈ Polynomial.nthRootsFinset ↑p { x // x ∈ NumberField.ringOfIntegers K } }) (hη : η ≠ zeta_sub_one_dvd_root hp hζ e hy) : { x // x ∈ NumberField.ringOfIntegers K }

Equations

• One or more equations did not get rendered due to their size.

noncomputable def a_div_a_zero_denom {K : Type u_1} {p : ℕ+} [hpri : Fact (PNat.Prime p)] [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] (hp : p ≠ 2) [Fintype (ClassGroup { x // x ∈ NumberField.ringOfIntegers K })] (hreg : Nat.Coprime (↑p) (Fintype.card (ClassGroup { x // x ∈ NumberField.ringOfIntegers K }))) {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) {x : { x // x ∈ NumberField.ringOfIntegers K }} {y : { x // x ∈ NumberField.ringOfIntegers K }} {z : { x // x ∈ NumberField.ringOfIntegers K }} {ε : { x // x ∈ NumberField.ringOfIntegers K }ˣ} {m : ℕ} (e : x ^ ↑p + y ^ ↑p = ↑ε * ((↑(IsPrimitiveRoot.unit' hζ) - 1) ^ (m + 1) * z) ^ ↑p) (hy : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ y) (hz : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ z) (η : { x // x ∈ Polynomial.nthRootsFinset ↑p { x // x ∈ NumberField.ringOfIntegers K } }) (hη : η ≠ zeta_sub_one_dvd_root hp hζ e hy) : { x // x ∈ NumberField.ringOfIntegers K }

Equations

• One or more equations did not get rendered due to their size.

theorem a_div_a_zero_num_spec {K : Type u_1} {p : ℕ+} [hpri : Fact (PNat.Prime p)] [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] (hp : p ≠ 2) [Fintype (ClassGroup { x // x ∈ NumberField.ringOfIntegers K })] (hreg : Nat.Coprime (↑p) (Fintype.card (ClassGroup { x // x ∈ NumberField.ringOfIntegers K }))) {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) {x : { x // x ∈ NumberField.ringOfIntegers K }} {y : { x // x ∈ NumberField.ringOfIntegers K }} {z : { x // x ∈ NumberField.ringOfIntegers K }} {ε : { x // x ∈ NumberField.ringOfIntegers K }ˣ} {m : ℕ} (e : x ^ ↑p + y ^ ↑p = ↑ε * ((↑(IsPrimitiveRoot.unit' hζ) - 1) ^ (m + 1) * z) ^ ↑p) (hy : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ y) (hz : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ z) (η : { x // x ∈ Polynomial.nthRootsFinset ↑p { x // x ∈ NumberField.ringOfIntegers K } }) (hη : η ≠ zeta_sub_one_dvd_root hp hζ e hy) : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ a_div_a_zero_num hp hreg hζ e hy hz η hη

theorem a_div_a_zero_denom_spec {K : Type u_1} {p : ℕ+} [hpri : Fact (PNat.Prime p)] [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] (hp : p ≠ 2) [Fintype (ClassGroup { x // x ∈ NumberField.ringOfIntegers K })] (hreg : Nat.Coprime (↑p) (Fintype.card (ClassGroup { x // x ∈ NumberField.ringOfIntegers K }))) {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) {x : { x // x ∈ NumberField.ringOfIntegers K }} {y : { x // x ∈ NumberField.ringOfIntegers K }} {z : { x // x ∈ NumberField.ringOfIntegers K }} {ε : { x // x ∈ NumberField.ringOfIntegers K }ˣ} {m : ℕ} (e : x ^ ↑p + y ^ ↑p = ↑ε * ((↑(IsPrimitiveRoot.unit' hζ) - 1) ^ (m + 1) * z) ^ ↑p) (hy : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ y) (hz : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ z) (η : { x // x ∈ Polynomial.nthRootsFinset ↑p { x // x ∈ NumberField.ringOfIntegers K } }) (hη : η ≠ zeta_sub_one_dvd_root hp hζ e hy) : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ a_div_a_zero_denom hp hreg hζ e hy hz η hη

theorem a_div_a_zero_eq {K : Type u_1} {p : ℕ+} [hpri : Fact (PNat.Prime p)] [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] (hp : p ≠ 2) [Fintype (ClassGroup { x // x ∈ NumberField.ringOfIntegers K })] (hreg : Nat.Coprime (↑p) (Fintype.card (ClassGroup { x // x ∈ NumberField.ringOfIntegers K }))) {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) {x : { x // x ∈ NumberField.ringOfIntegers K }} {y : { x // x ∈ NumberField.ringOfIntegers K }} {z : { x // x ∈ NumberField.ringOfIntegers K }} {ε : { x // x ∈ NumberField.ringOfIntegers K }ˣ} {m : ℕ} (e : x ^ ↑p + y ^ ↑p = ↑ε * ((↑(IsPrimitiveRoot.unit' hζ) - 1) ^ (m + 1) * z) ^ ↑p) (hy : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ y) (hz : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ z) (η : { x // x ∈ Polynomial.nthRootsFinset ↑p { x // x ∈ NumberField.ringOfIntegers K } }) (hη : η ≠ zeta_sub_one_dvd_root hp hζ e hy) : FractionalIdeal.spanSingleton (nonZeroDivisors { x // x ∈ NumberField.ringOfIntegers K }) (↑(a_div_a_zero_num hp hreg hζ e hy hz η hη) / ↑(a_div_a_zero_denom hp hreg hζ e hy hz η hη)) = ↑(root_div_zeta_sub_one_dvd_gcd hp hζ e hy η) / ↑(a_eta_zero_dvd_p_pow hp hζ e hy)

theorem a_mul_denom_eq_a_zero_mul_num {K : Type u_1} {p : ℕ+} [hpri : Fact (PNat.Prime p)] [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] (hp : p ≠ 2) [Fintype (ClassGroup { x // x ∈ NumberField.ringOfIntegers K })] (hreg : Nat.Coprime (↑p) (Fintype.card (ClassGroup { x // x ∈ NumberField.ringOfIntegers K }))) {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) {x : { x // x ∈ NumberField.ringOfIntegers K }} {y : { x // x ∈ NumberField.ringOfIntegers K }} {z : { x // x ∈ NumberField.ringOfIntegers K }} {ε : { x // x ∈ NumberField.ringOfIntegers K }ˣ} {m : ℕ} (e : x ^ ↑p + y ^ ↑p = ↑ε * ((↑(IsPrimitiveRoot.unit' hζ) - 1) ^ (m + 1) * z) ^ ↑p) (hy : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ y) (hz : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ z) (η : { x // x ∈ Polynomial.nthRootsFinset ↑p { x // x ∈ NumberField.ringOfIntegers K } }) (hη : η ≠ zeta_sub_one_dvd_root hp hζ e hy) : root_div_zeta_sub_one_dvd_gcd hp hζ e hy η * Ideal.span {a_div_a_zero_denom hp hreg hζ e hy hz η hη} = a_eta_zero_dvd_p_pow hp hζ e hy * Ideal.span {a_div_a_zero_num hp hreg hζ e hy hz η hη}

theorem associated_eta_zero {K : Type u_1} {p : ℕ+} [hpri : Fact (PNat.Prime p)] [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] (hp : p ≠ 2) [Fintype (ClassGroup { x // x ∈ NumberField.ringOfIntegers K })] (hreg : Nat.Coprime (↑p) (Fintype.card (ClassGroup { x // x ∈ NumberField.ringOfIntegers K }))) {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) {x : { x // x ∈ NumberField.ringOfIntegers K }} {y : { x // x ∈ NumberField.ringOfIntegers K }} {z : { x // x ∈ NumberField.ringOfIntegers K }} {ε : { x // x ∈ NumberField.ringOfIntegers K }ˣ} {m : ℕ} (e : x ^ ↑p + y ^ ↑p = ↑ε * ((↑(IsPrimitiveRoot.unit' hζ) - 1) ^ (m + 1) * z) ^ ↑p) (hy : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ y) (hz : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ z) (η : { x // x ∈ Polynomial.nthRootsFinset ↑p { x // x ∈ NumberField.ringOfIntegers K } }) (hη : η ≠ zeta_sub_one_dvd_root hp hζ e hy) : Associated ((x + y * ↑(zeta_sub_one_dvd_root hp hζ e hy)) * a_div_a_zero_num hp hreg hζ e hy hz η hη ^ ↑p) ((x + y * ↑η) * (↑(IsPrimitiveRoot.unit' hζ) - 1) ^ (m * ↑p) * a_div_a_zero_denom hp hreg hζ e hy hz η hη ^ ↑p)

noncomputable def associated_eta_zero_unit {K : Type u_1} {p : ℕ+} [hpri : Fact (PNat.Prime p)] [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] (hp : p ≠ 2) [Fintype (ClassGroup { x // x ∈ NumberField.ringOfIntegers K })] (hreg : Nat.Coprime (↑p) (Fintype.card (ClassGroup { x // x ∈ NumberField.ringOfIntegers K }))) {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) {x : { x // x ∈ NumberField.ringOfIntegers K }} {y : { x // x ∈ NumberField.ringOfIntegers K }} {z : { x // x ∈ NumberField.ringOfIntegers K }} {ε : { x // x ∈ NumberField.ringOfIntegers K }ˣ} {m : ℕ} (e : x ^ ↑p + y ^ ↑p = ↑ε * ((↑(IsPrimitiveRoot.unit' hζ) - 1) ^ (m + 1) * z) ^ ↑p) (hy : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ y) (hz : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ z) (η : { x // x ∈ Polynomial.nthRootsFinset ↑p { x // x ∈ NumberField.ringOfIntegers K } }) (hη : η ≠ zeta_sub_one_dvd_root hp hζ e hy) : { x // x ∈ NumberField.ringOfIntegers K }ˣ

Equations

• One or more equations did not get rendered due to their size.

theorem associated_eta_zero_unit_spec {K : Type u_1} {p : ℕ+} [hpri : Fact (PNat.Prime p)] [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] (hp : p ≠ 2) [Fintype (ClassGroup { x // x ∈ NumberField.ringOfIntegers K })] (hreg : Nat.Coprime (↑p) (Fintype.card (ClassGroup { x // x ∈ NumberField.ringOfIntegers K }))) {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) {x : { x // x ∈ NumberField.ringOfIntegers K }} {y : { x // x ∈ NumberField.ringOfIntegers K }} {z : { x // x ∈ NumberField.ringOfIntegers K }} {ε : { x // x ∈ NumberField.ringOfIntegers K }ˣ} {m : ℕ} (e : x ^ ↑p + y ^ ↑p = ↑ε * ((↑(IsPrimitiveRoot.unit' hζ) - 1) ^ (m + 1) * z) ^ ↑p) (hy : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ y) (hz : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ z) (η : { x // x ∈ Polynomial.nthRootsFinset ↑p { x // x ∈ NumberField.ringOfIntegers K } }) (hη : η ≠ zeta_sub_one_dvd_root hp hζ e hy) : ↑(associated_eta_zero_unit hp hreg hζ e hy hz η hη) * (x + y * ↑(zeta_sub_one_dvd_root hp hζ e hy)) * a_div_a_zero_num hp hreg hζ e hy hz η hη ^ ↑p = (x + y * ↑η) * (↑(IsPrimitiveRoot.unit' hζ) - 1) ^ (m * ↑p) * a_div_a_zero_denom hp hreg hζ e hy hz η hη ^ ↑p

theorem x_plus_y_mul_ne_zero {K : Type u_1} {p : ℕ+} [hpri : Fact (PNat.Prime p)] [Field K] [NumberField K] (hp : p ≠ 2) {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) {x : { x // x ∈ NumberField.ringOfIntegers K }} {y : { x // x ∈ NumberField.ringOfIntegers K }} {z : { x // x ∈ NumberField.ringOfIntegers K }} {ε : { x // x ∈ NumberField.ringOfIntegers K }ˣ} {m : ℕ} (e : x ^ ↑p + y ^ ↑p = ↑ε * ((↑(IsPrimitiveRoot.unit' hζ) - 1) ^ (m + 1) * z) ^ ↑p) (hz : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ z) (η : { x // x ∈ Polynomial.nthRootsFinset ↑p { x // x ∈ NumberField.ringOfIntegers K } }) : x + y * ↑η ≠ 0

theorem stuff {K : Type u_1} {p : ℕ+} [hpri : Fact (PNat.Prime p)] [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] (hp : p ≠ 2) [Fintype (ClassGroup { x // x ∈ NumberField.ringOfIntegers K })] (hreg : Nat.Coprime (↑p) (Fintype.card (ClassGroup { x // x ∈ NumberField.ringOfIntegers K }))) {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) {x : { x // x ∈ NumberField.ringOfIntegers K }} {y : { x // x ∈ NumberField.ringOfIntegers K }} {z : { x // x ∈ NumberField.ringOfIntegers K }} {ε : { x // x ∈ NumberField.ringOfIntegers K }ˣ} {m : ℕ} (e : x ^ ↑p + y ^ ↑p = ↑ε * ((↑(IsPrimitiveRoot.unit' hζ) - 1) ^ (m + 1) * z) ^ ↑p) (hy : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ y) (hz : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ z) (η₁ : { x // x ∈ Polynomial.nthRootsFinset ↑p { x // x ∈ NumberField.ringOfIntegers K } }) (hη₁ : η₁ ≠ zeta_sub_one_dvd_root hp hζ e hy) (η₂ : { x // x ∈ Polynomial.nthRootsFinset ↑p { x // x ∈ NumberField.ringOfIntegers K } }) (hη₂ : η₂ ≠ zeta_sub_one_dvd_root hp hζ e hy) : (↑η₂ - ↑(zeta_sub_one_dvd_root hp hζ e hy)) * ↑(associated_eta_zero_unit hp hreg hζ e hy hz η₁ hη₁) * (a_div_a_zero_num hp hreg hζ e hy hz η₁ hη₁ * a_div_a_zero_denom hp hreg hζ e hy hz η₂ hη₂) ^ ↑p + (↑(zeta_sub_one_dvd_root hp hζ e hy) - ↑η₁) * ↑(associated_eta_zero_unit hp hreg hζ e hy hz η₂ hη₂) * (a_div_a_zero_num hp hreg hζ e hy hz η₂ hη₂ * a_div_a_zero_denom hp hreg hζ e hy hz η₁ hη₁) ^ ↑p = (↑η₂ - ↑η₁) * ((↑(IsPrimitiveRoot.unit' hζ) - 1) ^ m * (a_div_a_zero_denom hp hreg hζ e hy hz η₁ hη₁ * a_div_a_zero_denom hp hreg hζ e hy hz η₂ hη₂)) ^ ↑p

theorem exists_solution {K : Type u_1} {p : ℕ+} [hpri : Fact (PNat.Prime p)] [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] (hp : p ≠ 2) [Fintype (ClassGroup { x // x ∈ NumberField.ringOfIntegers K })] (hreg : Nat.Coprime (↑p) (Fintype.card (ClassGroup { x // x ∈ NumberField.ringOfIntegers K }))) {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) {x : { x // x ∈ NumberField.ringOfIntegers K }} {y : { x // x ∈ NumberField.ringOfIntegers K }} {z : { x // x ∈ NumberField.ringOfIntegers K }} {ε : { x // x ∈ NumberField.ringOfIntegers K }ˣ} {m : ℕ} (e : x ^ ↑p + y ^ ↑p = ↑ε * ((↑(IsPrimitiveRoot.unit' hζ) - 1) ^ (m + 1) * z) ^ ↑p) (hy : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ y) (hz : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ z) : ∃ x' y' z' ε₁ ε₂ ε₃, ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ x' ∧ ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ y' ∧ ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ z' ∧ ↑ε₁ * x' ^ ↑p + ↑ε₂ * y' ^ ↑p = ↑ε₃ * ((↑(IsPrimitiveRoot.unit' hζ) - 1) ^ m * z') ^ ↑p

theorem exists_solution'_aux {K : Type u_1} {p : ℕ+} [hpri : Fact (PNat.Prime p)] [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] (hp : p ≠ 2) {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) {x : { x // x ∈ NumberField.ringOfIntegers K }} {y : { x // x ∈ NumberField.ringOfIntegers K }} {ε₁ : { x // x ∈ NumberField.ringOfIntegers K }ˣ} {ε₂ : { x // x ∈ NumberField.ringOfIntegers K }ˣ} (hx : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ x) (h : ↑↑p ∣ ↑ε₁ * x ^ ↑p + ↑ε₂ * y ^ ↑p) : ∃ a, ↑↑p ∣ ↑(ε₁ / ε₂) - a ^ ↑p

theorem exists_solution' {K : Type u_1} {p : ℕ+} [hpri : Fact (PNat.Prime p)] [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] (hp : p ≠ 2) [Fintype (ClassGroup { x // x ∈ NumberField.ringOfIntegers K })] (hreg : Nat.Coprime (↑p) (Fintype.card (ClassGroup { x // x ∈ NumberField.ringOfIntegers K }))) {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) {x : { x // x ∈ NumberField.ringOfIntegers K }} {y : { x // x ∈ NumberField.ringOfIntegers K }} {z : { x // x ∈ NumberField.ringOfIntegers K }} {ε : { x // x ∈ NumberField.ringOfIntegers K }ˣ} {m : ℕ} (e : x ^ ↑p + y ^ ↑p = ↑ε * ((↑(IsPrimitiveRoot.unit' hζ) - 1) ^ (m + 1) * z) ^ ↑p) (hy : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ y) (hz : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ z) : ∃ x' y' z' ε₃, ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ y' ∧ ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ z' ∧ x' ^ ↑p + y' ^ ↑p = ↑ε₃ * ((↑(IsPrimitiveRoot.unit' hζ) - 1) ^ m * z') ^ ↑p