eq_prod_roots_of_monic_of_splits_id

English

If p splits over id_K, then p equals the product of its linear factors X − a over its roots a ∈ p.roots mapped by id.

Русский

Если p распадается над id_K, то p равна произведению линейных множителей X − a по корням a ∈ p.roots отображённым через id_K.

LaTeX

$$$\\forall p:\\ Polynomial K,\\; \\text{Splits}(\\mathrm{id}_K, p) \\Rightarrow p = C(p.leadingCoeff) \\cdot \\prod_{a \\in p.\\text{roots}} (X - C(a)).$$$

Lean4

theorem eq_prod_roots_of_monic_of_splits_id {p : K[X]} (m : Monic p) (hsplit : Splits (RingHom.id K) p) :
    p = (p.roots.map fun a => X - C a).prod :=
  by
  convert eq_prod_roots_of_splits_id hsplit
  simp [m]

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