coeff_modMonomial_of_le — Mathlib

English

If s ≤ s' then the coefficient of s' in x modulo s is zero.

Русский

Если s ≤ s', то коэффициент при s' в x modulo s равен нулю.

LaTeX

$$$\\operatorname{coeff}_{s'}(x \\modMonomial s) = 0 \\quad \\text{if } s \\le s'$$$

Lean4

@[simp]
theorem coeff_modMonomial_of_le {s' s : σ →₀ ℕ} (x : MvPolynomial σ R) (h : s ≤ s') : coeff s' (x %ᵐᵒⁿᵒᵐⁱᵃˡ s) = 0 :=
  x.modOf_apply_of_exists_add _ _ <| exists_add_of_le h

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