English
If μ is a primitive (n+1)-th root of unity in a domain, then the product (-1)^n ∏_{k=0}^{n-1} (μ^{k+1} - 1) equals n+1.
Русский
Если μ является примитивным (n+1)-м корнем единства в области, то произведение (-1)^n ∏_{k=0}^{n-1} (μ^{k+1} - 1) равно n+1.
LaTeX
$$$(-1)^n \prod_{k=0}^{n-1} (μ^{k+1} - 1) = n+1$$$
Lean4
/-- 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 prod_one_sub_pow_eq_order {n : ℕ} {μ : R} (hμ : IsPrimitiveRoot μ (n + 1)) :
∏ k ∈ range n, (1 - μ ^ (k + 1)) = n + 1 :=
by
have := X_pow_sub_C_eq_prod hμ n.zero_lt_succ (one_pow (n + 1))
rw [C_1, ← mul_geom_sum, prod_range_succ', pow_zero, mul_one, mul_comm, eq_comm] at this
replace this := mul_right_cancel₀ (Polynomial.X_sub_C_ne_zero 1) this
apply_fun Polynomial.eval 1 at this
simpa only [mul_one, map_pow, eval_prod, eval_sub, eval_X, eval_pow, eval_C, eval_geom_sum, one_pow, sum_const,
card_range, nsmul_eq_mul, Nat.cast_add, Nat.cast_one] using this
