degreeOf_mul_C_le — Mathlib

English

For any p, i, c, the degree with respect to i of p times a constant C c does not exceed the degree of p: deg_i(p · C c) ≤ deg_i(p).

Русский

Для любого p, i, c степень по i от p·C c не превосходит степень по i от p: deg_i(p·C c) ≤ deg_i(p).

LaTeX

$$$\operatorname{degree}_i(p \cdot C\,c) \le \operatorname{degree}_i(p)$$$

Lean4

theorem degreeOf_mul_C_le (p : MvPolynomial σ R) (i : σ) (c : R) : (p * C c).degreeOf i ≤ p.degreeOf i :=
  by
  unfold degreeOf
  convert Multiset.count_le_of_le i degrees_mul_le
  simp only [degrees_C, add_zero]

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