More results on primitive roots of unity

(We put these in a separate file because of the KummerExtension import.)

Assume that μ is a primitive nth root of unity in an integral domain R. Then $$ \prod_{k=1}^{n-1} (1 - \mu^k) = n \,; $$ see IsPrimitiveRoot.prod_one_sub_pow_eq_order and its variant IsPrimitiveRoot.prod_pow_sub_one_eq_order in terms of ∏ (μ^k - 1).

We use this to deduce that n is divisible by (μ - 1)^k in ℤ[μ] ⊆ R when k < n.

theorem IsPrimitiveRoot.prod_one_sub_pow_eq_order {R : Type u_1} [CommRing R] [IsDomain R] {n : ℕ} {μ : R} (hμ : IsPrimitiveRoot μ (n + 1)) : ∏ k ∈ Finset.range n, (1 - μ ^ (k + 1)) = ↑n + 1

If μ is a primitive nth root of unity in R, then ∏(1≤k<n) (1-μ^k) = n. (Stated with n+1 in place of n to avoid the condition n ≠ 0.)

theorem IsPrimitiveRoot.prod_pow_sub_one_eq_order {R : Type u_1} [CommRing R] [IsDomain R] {n : ℕ} {μ : R} (hμ : IsPrimitiveRoot μ (n + 1)) : (-1) ^ n * ∏ k ∈ Finset.range n, (μ ^ (k + 1) - 1) = ↑n + 1

If μ is a primitive nth root of unity in R, then (-1)^(n-1) * ∏(1≤k<n) (μ^k-1) = n. (Stated with n+1 in place of n to avoid the condition n ≠ 0.)

theorem IsPrimitiveRoot.self_sub_one_pow_dvd_order {R : Type u_1} [CommRing R] [IsDomain R] {k n : ℕ} (hn : k < n) {μ : R} (hμ : IsPrimitiveRoot μ n) : ∃ z ∈ Algebra.adjoin ℤ {μ}, ↑n = z * (μ - 1) ^ k

If μ is a primitive nth root of unity in R and k < n, then n is divisible by (μ-1)^k in ℤ[μ] ⊆ R.