def FltRegular.CaseI.SlightlyEasier : Prop

Statement of case I with additional assumptions.

Equations

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

def FltRegular.CaseI.Statement : Prop

Statement of case I.

Equations

• FltRegular.CaseI.Statement = ∀ ⦃a b c : ℤ⦄ {p : ℕ} [hpri : Fact (Nat.Prime p)], IsRegularPrime p → ¬↑p ∣ a * b * c → a ^ p + b ^ p ≠ c ^ p

theorem FltRegular.CaseI.may_assume : FltRegular.CaseI.SlightlyEasier → FltRegular.CaseI.Statement

theorem FltRegular.ab_coprime {p : ℕ} {a : ℤ} {b : ℤ} {c : ℤ} (H : a ^ p + b ^ p = c ^ p) (hpzero : p ≠ 0) (hgcd : Finset.gcd {a, b, c} id = 1) : IsCoprime a b

instance FltRegular.foo1 (p : ℕ) [hpri : Fact (Nat.Prime p)] : IsDomain { x // x ∈ NumberField.ringOfIntegers (CyclotomicField { val := p, property := (_ : 0 < p) } ℚ) }

Equations

• FltRegular.foo1 = FltRegular.foo1.proof_1

instance FltRegular.foo2 (p : ℕ) [hpri : Fact (Nat.Prime p)] : IsDedekindDomain { x // x ∈ NumberField.ringOfIntegers (CyclotomicField { val := p, property := (_ : 0 < p) } ℚ) }

Equations

• FltRegular.foo2 = FltRegular.foo2.proof_1

instance FltRegular.foo3 (p : ℕ) [hpri : Fact (Nat.Prime p)] : IsDomain (Ideal { x // x ∈ NumberField.ringOfIntegers (CyclotomicField { val := p, property := (_ : 0 < p) } ℚ) })

Equations

• FltRegular.foo3 = FltRegular.foo3.proof_1

noncomputable instance FltRegular.foo4 (p : ℕ) [hpri : Fact (Nat.Prime p)] : NormalizedGCDMonoid (Ideal { x // x ∈ NumberField.ringOfIntegers (CyclotomicField { val := p, property := (_ : 0 < p) } ℚ) })

Equations

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

noncomputable instance FltRegular.foo5 (p : ℕ) [hpri : Fact (Nat.Prime p)] : GCDMonoid (Ideal { x // x ∈ NumberField.ringOfIntegers (CyclotomicField { val := p, property := (_ : 0 < p) } ℚ) })

Equations

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

theorem FltRegular.exists_ideal {p : ℕ} [hpri : Fact (Nat.Prime p)] {a : ℤ} {b : ℤ} {c : ℤ} (h5p : 5 ≤ p) (H : a ^ p + b ^ p = c ^ p) (hgcd : Finset.gcd {a, b, c} id = 1) (caseI : ¬↑p ∣ a * b * c) {ζ : { x // x ∈ NumberField.ringOfIntegers (CyclotomicField { val := p, property := (_ : 0 < p) } ℚ) }} (hζ : ζ ∈ Polynomial.nthRootsFinset p { x // x ∈ NumberField.ringOfIntegers (CyclotomicField { val := p, property := (_ : 0 < p) } ℚ) }) : ∃ I, Ideal.span {↑a + ζ * ↑b} = I ^ p

theorem FltRegular.IsPrincipal_of_IsPrincipal_pow_of_Coprime {p : ℕ} (A : Type u_1) [CommRing A] [IsDedekindDomain A] [Fintype (ClassGroup A)] (H : Nat.Coprime p (Fintype.card (ClassGroup A))) (I : Ideal A) (hI : Submodule.IsPrincipal (I ^ p)) : Submodule.IsPrincipal I

theorem FltRegular.is_principal_aux {p : ℕ} [hpri : Fact (Nat.Prime p)] (K' : Type u_1) [Field K'] [CharZero K'] [IsCyclotomicExtension {{ val := p, property := (_ : 0 < p) }} ℚ K'] [Fintype (ClassGroup { x // x ∈ NumberField.ringOfIntegers K' })] {a : ℤ} {b : ℤ} {ζ : { x // x ∈ NumberField.ringOfIntegers K' }} (hreg : Nat.Coprime p (Fintype.card (ClassGroup { x // x ∈ NumberField.ringOfIntegers K' }))) (I : Ideal { x // x ∈ NumberField.ringOfIntegers K' }) (hI : Ideal.span {↑a + ζ * ↑b} = I ^ p) : ∃ u α, ↑u * α ^ p = ↑a + ζ * ↑b

theorem FltRegular.is_principal {p : ℕ} [hpri : Fact (Nat.Prime p)] {a : ℤ} {b : ℤ} {c : ℤ} {ζ : { x // x ∈ NumberField.ringOfIntegers (CyclotomicField { val := p, property := (_ : 0 < p) } ℚ) }} (hreg : IsRegularPrime p) (hp5 : 5 ≤ p) (hgcd : Finset.gcd {a, b, c} id = 1) (caseI : ¬↑p ∣ a * b * c) (H : a ^ p + b ^ p = c ^ p) (hζ : IsPrimitiveRoot ζ p) : ∃ u α, ↑u * α ^ p = ↑a + ζ * ↑b

theorem FltRegular.ex_fin_div {p : ℕ} [hpri : Fact (Nat.Prime p)] {a : ℤ} {b : ℤ} {c : ℤ} {ζ : { x // x ∈ NumberField.ringOfIntegers (CyclotomicField { val := p, property := (_ : 0 < p) } ℚ) }} (hp5 : 5 ≤ p) (hreg : IsRegularPrime p) (hζ : IsPrimitiveRoot ζ p) (hgcd : Finset.gcd {a, b, c} 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₂

def FltRegular.f (a : ℤ) (b : ℤ) (k₁ : ℕ) (k₂ : ℕ) : ℕ → ℤ

Auxiliary function

Equations

• FltRegular.f a b k₁ k₂ x = if x = 0 then a else if x = 1 then b else if x = k₁ then -a else if x = k₂ then -b else 0

theorem FltRegular.auxf' {p : ℕ} (hp5 : 5 ≤ p) (a : ℤ) (b : ℤ) (k₁ : Fin p) (k₂ : Fin p) : ∃ i, i ∈ Finset.range p ∧ FltRegular.f a b (↑k₁) (↑k₂) i = 0

theorem FltRegular.auxf {p : ℕ} (hp5 : 5 ≤ p) (a : ℤ) (b : ℤ) (k₁ : Fin p) (k₂ : Fin p) : ∃ i, FltRegular.f a b ↑k₁ ↑k₂ ↑i = 0

theorem FltRegular.caseI_easier {p : ℕ} [hpri : Fact (Nat.Prime p)] {a : ℤ} {b : ℤ} {c : ℤ} (hreg : IsRegularPrime p) (hp5 : 5 ≤ p) (hgcd : Finset.gcd {a, b, c} id = 1) (hab : ¬a ≡ b [ZMOD ↑p]) (caseI : ¬↑p ∣ a * b * c) : a ^ p + b ^ p ≠ c ^ p

Case I with additional assumptions.

theorem FltRegular.caseI {a : ℤ} {b : ℤ} {c : ℤ} {p : ℕ} [Fact (Nat.Prime p)] (hreg : IsRegularPrime p) (caseI : ¬↑p ∣ a * b * c) : a ^ p + b ^ p ≠ c ^ p

CaseI.