eq_prod_roots_of_splits_id — Mathlib

English

If p ∈ K[X] splits over id_K, then p.map i equals the leadingCoeff factor times the product over roots of X minus C a.

Русский

Если p ∈ K[X] распадается над id_K, то p.map i равняется C(i(p.leadingCoeff)) умноженному на произведение по корням X − C a.

LaTeX

$$$\\forall p:\\ Polynomial K,\\; (p.Splits\\; \\mathrm{id}_K) \\Rightarrow p.map i = C(i(p.leadingCoeff)) \\cdot \\left( (p.map i).\\text{roots}.map (\\lambda a. X - C a)\\right).prod.$$$

Lean4

theorem eq_prod_roots_of_splits_id {p : K[X]} (hsplit : Splits (RingHom.id K) p) :
    p = C p.leadingCoeff * (p.roots.map fun a => X - C a).prod := by simpa using eq_prod_roots_of_splits hsplit

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