prod_pow_sub_one_eq_order — Mathlib

English

If μ is a primitive nth root of unity in a commutative ring R and k < n, then n is divisible by some element z*(μ-1)^k with z in ℤ[μ].

Русский

Если μ — примитивный n-й корень единицы в коммутативном кольце R и k < n, то n делится на нечто вида z*(μ-1)^k с z ∈ ℤ[μ].

LaTeX

$$∃ z ∈ adjoin ℤ { μ }, n = z * (μ - 1)^k$$

Lean4

/-- 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 prod_pow_sub_one_eq_order {n : ℕ} {μ : R} (hμ : IsPrimitiveRoot μ (n + 1)) :
    (-1) ^ n * ∏ k ∈ range n, (μ ^ (k + 1) - 1) = n + 1 :=
  by
  have : (-1 : R) ^ n = ∏ k ∈ range n, -1 := by rw [prod_const, card_range]
  simp only [this, ← prod_mul_distrib, neg_one_mul, neg_sub, ← prod_one_sub_pow_eq_order hμ]

Похожие утверждения