C_leadingCoeff_mul_prod_multiset_X_sub_C

English

If p has as many roots as its degree, then p equals its leading coefficient times the product over its roots of (X − a).

Русский

Если у p столько же корней, сколько deg(p), то p = leadingCoeff(p) · ∏_{a∈roots} (X − a).

LaTeX

$$C p.leadingCoeff * ∏_{a ∈ p.roots} (X − C a) = p, при условии, что card(p.roots) = p.natDegree$$

Lean4

/-- A polynomial `p` that has as many roots as its degree
can be written `p = p.leadingCoeff * ∏(X - a)`, for `a` in `p.roots`. -/
theorem C_leadingCoeff_mul_prod_multiset_X_sub_C (hroots : Multiset.card p.roots = p.natDegree) :
    C p.leadingCoeff * (p.roots.map fun a => X - C a).prod = p :=
  (eq_leadingCoeff_mul_of_monic_of_dvd_of_natDegree_le (monic_multisetProd_X_sub_C p.roots) p.prod_multiset_X_sub_C_dvd
      ((natDegree_multiset_prod_X_sub_C_eq_card _).trans hroots).ge).symm

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