Additional lemmas for cyclotomic fields

This file proves divisibility results for cyclotomic integers, traces, and norms that are used by the surrounding FLT development.

theorem exists_zeta_sub_one_dvd_sub_Int {K : Type u_1} {p : ℕ} [hpri : Fact (Nat.Prime p)] [Field K] [CharZero K] [IsCyclotomicExtension {p} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ p) (a : NumberField.RingOfIntegers K) : ∃ (b : ℤ), hζ.toInteger - 1 ∣ a - ↑b

theorem exists_dvd_pow_sub_Int_pow {K : Type u_1} {p : ℕ} [hpri : Fact (Nat.Prime p)] [Field K] [CharZero K] [IsCyclotomicExtension {p} ℚ K] (hp : p ≠ 2) (a : NumberField.RingOfIntegers K) : ∃ (b : ℤ), ↑p ∣ a ^ p - ↑b ^ p

theorem quotient_zero_sub_one_comp_aut {K : Type u_1} {p : ℕ} [hpri : Fact (Nat.Prime p)] [Field K] [CharZero K] [IsCyclotomicExtension {p} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ p) (σ : NumberField.RingOfIntegers K →+* NumberField.RingOfIntegers K) : (Ideal.Quotient.mk (Ideal.span {hζ.toInteger - 1})).comp σ = Ideal.Quotient.mk (Ideal.span {hζ.toInteger - 1})

theorem zeta_sub_one_dvd_trace_sub_smul {K : Type u_1} {p : ℕ} [hpri : Fact (Nat.Prime p)] [Field K] [CharZero K] [IsCyclotomicExtension {p} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ p) (x : NumberField.RingOfIntegers K) : hζ.toInteger - 1 ∣ ↑((Algebra.trace ℤ (NumberField.RingOfIntegers K)) x) - (p - 1) • x

theorem zeta_sub_one_pow_dvd_norm_sub_pow {K : Type u_1} {p : ℕ} [hpri : Fact (Nat.Prime p)] [Field K] [CharZero K] [IsCyclotomicExtension {p} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ p) (x : NumberField.RingOfIntegers K) : (hζ.toInteger - 1) ^ p ∣ ↑((Algebra.norm ℤ) (1 + p • x)) - 1 + p • x

theorem norm_add_one_smul_of_isUnit {K : Type u_2} [Field K] [NumberField K] {p : ℕ} (hpri : Nat.Prime p) (hp : p ≠ 2) (x : NumberField.RingOfIntegers K) (hx : IsUnit (1 + p • x)) : (Algebra.norm ℤ) (1 + p • x) = 1