theorem FltRegular.CaseI.coe_unitGalConj {p : ℕ+} {K : Type u_1} [Field K] [CharZero K] [IsCyclotomicExtension {p} ℚ K] (x : { x // x ∈ NumberField.ringOfIntegers K }ˣ) : ↑(↑(unitGalConj K p) x) = ↑(intGal ↑(galConj K p)) ↑x

theorem FltRegular.CaseI.pow_sub_intGalConj_mem {p : ℕ+} {K : Type u_1} [Field K] [CharZero K] [IsCyclotomicExtension {p} ℚ K] (hp : Nat.Prime ↑p) (α : { x // x ∈ NumberField.ringOfIntegers K }) : α ^ ↑p - ↑(intGal ↑(galConj K p)) (α ^ ↑p) ∈ Ideal.span {↑↑p}

theorem FltRegular.CaseI.exists_int_sum_eq_zero'_aux {p : ℕ+} {K : Type u_1} [Field K] [CharZero K] [IsCyclotomicExtension {p} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) (x : ℤ) (y : ℤ) (i : ℤ) : ↑(intGal ↑(galConj K p)) (↑x + ↑y * ↑(IsPrimitiveRoot.unit' hζ ^ i)) = ↑x + ↑y * ↑(IsPrimitiveRoot.unit' hζ ^ (-i))

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

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