degreeOf_le_totalDegree — Mathlib

English

Let f be a multivariate polynomial and i an index variable; then the degree of X_i in f is not greater than the total degree of f.

Русский

Пусть f — многочлен в нескольких переменных, и i — индекс переменной; степень X_i в f не превосходит общей степени f.

LaTeX

$$$\\\\forall f : MvPolynomial σ R, \\\\forall i, \\\\ degreeOf i f \\\\le totalDegree f$$$

Lean4

theorem degreeOf_le_totalDegree (f : MvPolynomial σ R) (i : σ) : f.degreeOf i ≤ f.totalDegree :=
  degreeOf_le_iff.mpr fun d hd ↦
    (eq_or_ne (d i) 0).elim (by cutsat) fun h ↦
      (Finset.single_le_sum (by cutsat) <| Finsupp.mem_support_iff.mpr h).trans (le_totalDegree hd)

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