More results on primitive roots of unity #
(We put these in a separate file because of the KummerExtension
import.)
Assume that μ
is a primitive n
th root of unity in an integral domain R
. Then
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))
:
If μ
is a primitive n
th 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))
:
If μ
is a primitive n
th 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)
:
If μ
is a primitive n
th root of unity in R
and k < n
, then n
is divisible
by (μ-1)^k
in ℤ[μ] ⊆ R
.