degreeOf_mul_X_self — Mathlib

English

Degree of j in f · X_j is bounded by degreeOf j f plus 1, with certain monotonicity properties.

Русский

Степень j в f X_j не выше deg_j f+1, с определённой монотонностью

LaTeX

$$$\deg_j(f X_j) \le \deg_j f + 1$$$

Lean4

theorem degreeOf_mul_X_self (j : σ) (f : MvPolynomial σ R) : degreeOf j (f * X j) ≤ degreeOf j f + 1 := by
  classical
  simp only [degreeOf]
  apply (Multiset.count_le_of_le j degrees_mul_le).trans
  simp only [Multiset.count_add, add_le_add_iff_left]
  convert Multiset.count_le_of_le j <| degrees_X' j
  rw [Multiset.count_singleton_self]

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