eval_eq_prod_roots_sub_of_monic_of_splits_id

English

If h ∈ K[X] splits over i and its mapped roots are a singleton {i x}, then h = C(h.leadingCoeff) (X − C x).

Русский

Если h ∈ K[X] распадается над i и корни h.map i образуют одноэлементное множество {i x}, тогда h = C(h.leadingCoeff)(X − C x).

LaTeX

$$$\\forall i:\\ K \\to L,\\; h:\\ Polynomial K,\\; h.Splits(i) \\Rightarrow (h.map i).\\text{roots} = {i x} \\Rightarrow h = C(h.leadingCoeff) \\cdot (X - C x).$$$

Lean4

theorem eval_eq_prod_roots_sub_of_monic_of_splits_id {p : K[X]} (m : Monic p) (hsplit : Splits (RingHom.id K) p)
    (v : K) : eval v p = (p.roots.map fun a ↦ v - a).prod := by simp [eval_eq_prod_roots_sub_of_splits_id hsplit, m]

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