card_roots — Mathlib

English

For a nonzero polynomial p ∈ R[X], the cardinality of p.roots is at most deg p (cast to WithBot ℕ).

Русский

Для ненулевого p ∈ R[X] мощность множества p.roots не превосходит deg p (соответствующее приведение к WithBot ℕ).

LaTeX

$$(Multiset.card (roots p) : WithBot ℕ) ≤ degree p.$$

Lean4

theorem card_roots (hp0 : p ≠ 0) : (Multiset.card (roots p) : WithBot ℕ) ≤ degree p := by
  classical
  unfold roots
  rw [dif_neg hp0]
  exact (Classical.choose_spec (exists_multiset_roots hp0)).1

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