degreeOf_sub_lt — Mathlib

English

If k > 0 and certain coefficient equalities hold near level k with respect to x, then degreeOf x (p − q) < k.

Русский

Если k > 0 и при некоторой близости к уровню k относительно x выполняются равенства коэффициентов, то degreeOf x (p − q) < k.

LaTeX

$$$\\text{degreeOf } x (p - q) < k$ under the stated hypotheses$$

Lean4

theorem degreeOf_sub_lt {x : σ} {f g : MvPolynomial σ R} {k : ℕ} (h : 0 < k)
    (hf : ∀ m : σ →₀ ℕ, m ∈ f.support → k ≤ m x → coeff m f = coeff m g)
    (hg : ∀ m : σ →₀ ℕ, m ∈ g.support → k ≤ m x → coeff m f = coeff m g) : degreeOf x (f - g) < k :=
  by
  rw [degreeOf_lt_iff h]
  grind [degreeOf_lt_iff, mem_support_iff, coeff_sub]

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