prod_multiset_X_sub_C_of_monic_of_roots_card_eq

English

If p is monic and the number of roots equals the degree, then p equals the product over its roots of (X − a).

Русский

Если p моничный и число корней равно степени, то p равно произведению по корням (X − a).

LaTeX

$$p.Monic → (p.roots.card = p.natDegree) → (p.roots.map (λ a, X − C a)).prod = p$$

Lean4

/-- A monic polynomial `p` that has as many roots as its degree
can be written `p = ∏(X - a)`, for `a` in `p.roots`. -/
theorem prod_multiset_X_sub_C_of_monic_of_roots_card_eq (hp : p.Monic) (hroots : Multiset.card p.roots = p.natDegree) :
    (p.roots.map fun a => X - C a).prod = p :=
  by
  convert C_leadingCoeff_mul_prod_multiset_X_sub_C hroots
  rw [hp.leadingCoeff, C_1, one_mul]

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