eq_prod_roots_of_splits — Mathlib

English

If f ∈ K[X] splits over i and deg f ≠ 0, then the roots multiset of f.map i is nonempty.

Русский

Если f ∈ K[X] распадается над i и deg f ≠ 0, то множество корней f.map i непусто.

LaTeX

$$$\\forall f:\\ K[X],\\; \\text{Splits }(i,f) \\land \\deg(f) \\neq 0 \\Rightarrow (f.map i).\\text{roots} \\neq 0.$$$

Lean4

theorem eq_prod_roots_of_splits {p : K[X]} {i : K →+* L} (hsplit : Splits i p) :
    p.map i = C (i p.leadingCoeff) * ((p.map i).roots.map fun a => X - C a).prod :=
  by
  rw [← leadingCoeff_map]; symm
  apply C_leadingCoeff_mul_prod_multiset_X_sub_C
  rw [natDegree_map]; exact (natDegree_eq_card_roots hsplit).symm

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