theorem IsCyclotomicExtension.CyclotomicUnit.Nat.one_lt_of_ne (n : ℕ) : n ≠ 0 → n ≠ 1 → 1 < n

theorem IsCyclotomicExtension.CyclotomicUnit.associated_one_sub_pow_primitive_root_of_coprime (A : Type w) [CommRing A] [IsDomain A] {n : ℕ} {j : ℕ} {k : ℕ} {ζ : A} (hζ : IsPrimitiveRoot ζ n) (hk : Nat.Coprime k n) (hj : Nat.Coprime j n) : Associated (1 - ζ ^ j) (1 - ζ ^ k)

theorem IsCyclotomicExtension.CyclotomicUnit.IsPrimitiveRoot.sum_pow_unit (A : Type w) [CommRing A] [IsDomain A] {n : ℕ} {k : ℕ} {ζ : A} (hn : 2 ≤ n) (hk : Nat.Coprime k n) (hζ : IsPrimitiveRoot ζ n) : IsUnit (Finset.sum (Finset.range k) fun i => ζ ^ i)

theorem IsCyclotomicExtension.CyclotomicUnit.IsPrimitiveRoot.zeta_pow_sub_eq_unit_zeta_sub_one (A : Type w) [CommRing A] [IsDomain A] {p : ℕ} {i : ℕ} {j : ℕ} {ζ : A} (hn : 2 ≤ p) (hp : Nat.Prime p) (hi : i < p) (hj : j < p) (hij : i ≠ j) (hζ : IsPrimitiveRoot ζ p) : ∃ u, ζ ^ i - ζ ^ j = ↑u * (1 - ζ)

theorem IsPrimitiveRoot.associated_sub_one {A : Type u_1} [CommRing A] [IsDomain A] {p : ℕ} (hp : Nat.Prime p) {ζ : A} (hζ : IsPrimitiveRoot ζ p) {η₁ : A} (hη₁ : η₁ ∈ Polynomial.nthRootsFinset p A) {η₂ : A} (hη₂ : η₂ ∈ Polynomial.nthRootsFinset p A) (e : η₁ ≠ η₂) : Associated (ζ - 1) (η₁ - η₂)