degree_update_le — Mathlib

English

Updating a coefficient in a polynomial cannot increase its degree beyond max(degree p, n).

Русский

Изменение коэффициента в многочлене не может увеличить степень выше max(deg p, n).

LaTeX

$$$\deg(p.update(n, a)) \le \max(\deg(p), n)$$$

Lean4

theorem degree_update_le (p : R[X]) (n : ℕ) (a : R) : degree (p.update n a) ≤ max (degree p) n := by
  classical
  rw [degree, support_update]
  split_ifs
  · exact (Finset.max_mono (erase_subset _ _)).trans (le_max_left _ _)
  · rw [max_insert, max_comm]
    exact le_rfl

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