card_le_degree_of_subset_roots — Mathlib

English

If Z is a finite set of roots contained in p.roots, then |Z| ≤ deg p.

Русский

Если Z — конечное множество корней, содержащихся в p.roots, то |Z| ≤ deg p.

LaTeX

$$For Z : Finset R with Z.val ⊆ p.roots, we have #Z ≤ p.natDegree.$$

Lean4

theorem card_le_degree_of_subset_roots {p : R[X]} {Z : Finset R} (h : Z.val ⊆ p.roots) : #Z ≤ p.natDegree :=
  (Multiset.card_le_card (Finset.val_le_iff_val_subset.2 h)).trans (Polynomial.card_roots' p)

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