X_pow_sub_one_splits — Mathlib

English

If there is a primitive nth root of unity in K, then X^n - 1 splits over K.

Русский

Если в K существует примитивный корень n-й степени единицы, то X^n - 1 распадается над K.

LaTeX

$$$\operatorname{Splits}(\mathrm{id}_K, X^n - 1)$$$

Lean4

/-- If there is a primitive `n`-th root of unity in `K`, then `X ^ n - 1` splits. -/
theorem X_pow_sub_one_splits {ζ : K} {n : ℕ} (h : IsPrimitiveRoot ζ n) : Splits (RingHom.id K) (X ^ n - C (1 : K)) := by
  rw [splits_iff_card_roots, ← nthRoots, IsPrimitiveRoot.card_nthRoots_one h, natDegree_X_pow_sub_C]

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