cyclotomic'_splits — Mathlib

English

For any field K, cyclotomic' n K splits completely over K.

Русский

Для любого поля K полином cyclotomic' n K распадается на линейные множители над K.

LaTeX

$$$\operatorname{Splits}(\mathrm{id}_K, \operatorname{cyclotomic}'(n,K))$$$

Lean4

/-- `cyclotomic' n K` splits. -/
theorem cyclotomic'_splits (n : ℕ) : Splits (RingHom.id K) (cyclotomic' n K) :=
  by
  apply splits_prod (RingHom.id K)
  intro z _
  simp only [splits_X_sub_C (RingHom.id K)]

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