degreeOf_C_mul_le — Mathlib

English

Let p be a multivariate polynomial, i a variable, and c a scalar. Then multiplying p by a constant C c does not increase the degree with respect to i: deg_i(C c · p) ≤ deg_i(p).

Русский

Пусть p — многов переменный полином, i — переменная, c — скаляр. Тогда умножение p на константу C c не увеличивает степень по i: deg_i(C c · p) ≤ deg_i(p).

LaTeX

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

Lean4

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

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