Cyclotomic lemmas for Case I

This file establishes the complex-conjugation congruence used in the first case of Fermat's Last Theorem for regular primes.

theorem FltRegular.CaseI.pow_sub_intGalConj_mem {p : ℕ} {K : Type u_1} [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] (α : NumberField.RingOfIntegers K) [Fact (Nat.Prime p)] (hp : 2 < p) : α ^ p - (NumberField.IsCMField.ringOfIntegersComplexConj K) (α ^ p) ∈ Ideal.span {↑p}

The difference between a p-th power and its complex conjugate is divisible by p.

theorem FltRegular.CaseI.exists_int_sum_eq_zero'_aux {p : ℕ} [NeZero p] {K : Type u_1} [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ p) (x y i : ℤ) (hp : 2 < p) : (NumberField.IsCMField.ringOfIntegersComplexConj K) (↑x + ↑y * ↑(⋯.unit ^ i)) = ↑x + ↑y * ↑(⋯.unit ^ (-i))

Complex conjugation negates the exponent of the distinguished cyclotomic unit.

theorem FltRegular.CaseI.exists_int_sum_eq_zero' {p : ℕ} [NeZero p] {K : Type u_1} [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ p) (x y i : ℤ) {u : (NumberField.RingOfIntegers K)ˣ} {α : NumberField.RingOfIntegers K} (h : ↑x + ↑y * ↑(⋯.unit ^ i) = ↑u * α ^ p) [Fact (Nat.Prime p)] (hp : 2 < p) : ∃ (k : ℕ), ↑x + ↑y * ↑(⋯.unit ^ i) - ↑((⋯.unit ^ k) ^ 2) * (↑x + ↑y * ↑(⋯.unit ^ (-i))) ∈ Ideal.span {↑p}

A natural exponent giving the Case I complex-conjugation congruence modulo p.

theorem FltRegular.CaseI.exists_int_sum_eq_zero {p : ℕ} [NeZero p] {K : Type u_1} [Field K] [NumberField K] [IsCyclotomicExtension {p} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ p) (x y i : ℤ) {u : (NumberField.RingOfIntegers K)ˣ} {α : NumberField.RingOfIntegers K} (h : ↑x + ↑y * ↑(⋯.unit ^ i) = ↑u * α ^ p) [Fact (Nat.Prime p)] (hp : 2 < p) : ∃ (k : ℤ), ↑x + ↑y * ↑(⋯.unit ^ i) - ↑(⋯.unit ^ (2 * k)) * (↑x + ↑y * ↑(⋯.unit ^ (-i))) ∈ Ideal.span {↑p}

An integer exponent giving the Case I complex-conjugation congruence modulo p.