card_roots_sub_C — Mathlib

English

For any a ∈ R with hp0 : 0 < deg p, (p − C a).roots has cardinal at most deg p.

Русский

Для любого a ∈ R при hp0 : 0 < deg p множество (p − C a).roots имеет мощность не более deg p.

LaTeX

$$card_roots (p) is bounded: (Multiset.card (p - C a).roots : WithBot ℕ) ≤ degree p, given hp0.$$

Lean4

theorem card_roots_sub_C {p : R[X]} {a : R} (hp0 : 0 < degree p) :
    (Multiset.card (p - C a).roots : WithBot ℕ) ≤ degree p :=
  calc
    (Multiset.card (p - C a).roots : WithBot ℕ) ≤ degree (p - C a) :=
      card_roots <| mt sub_eq_zero.1 fun h => not_le_of_gt hp0 <| h.symm ▸ degree_C_le
    _ = degree p := by rw [sub_eq_add_neg, ← C_neg]; exact degree_add_C hp0

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