prod_cyclotomic'_eq_X_pow_sub_one

English

The product of cyclotomic' i K over all divisors i of n equals X^n - 1.

Русский

Произведение cyclotomic' i K по всем делителям i числа n равно X^n - 1.

LaTeX

$$$\prod_{i \in \operatorname{divisors}(n)} \operatorname{cyclotomic}'(i,K) = X^n - 1$$$

Lean4

/-- If there is a primitive `n`-th root of unity in `K`, then
`∏ i ∈ Nat.divisors n, cyclotomic' i K = X ^ n - 1`. -/
theorem prod_cyclotomic'_eq_X_pow_sub_one {K : Type*} [CommRing K] [IsDomain K] {ζ : K} {n : ℕ} (hpos : 0 < n)
    (h : IsPrimitiveRoot ζ n) : ∏ i ∈ Nat.divisors n, cyclotomic' i K = X ^ n - 1 := by
  classical
  have hd : (n.divisors : Set ℕ).PairwiseDisjoint fun k => primitiveRoots k K := fun x _ y _ hne =>
    IsPrimitiveRoot.disjoint hne
  simp only [X_pow_sub_one_eq_prod hpos h, cyclotomic', ← Finset.prod_biUnion hd,
    IsPrimitiveRoot.nthRoots_one_eq_biUnion_primitiveRoots]

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