coeff_modMonomial_of_not_le — Mathlib

English

If s is not ≤ s', the coefficient of s' in the remainder mod s equals the original coefficient of s' in x.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem coeff_modMonomial_of_not_le {s' s : σ →₀ ℕ} (x : MvPolynomial σ R) (h : ¬s ≤ s') :
    coeff s' (x %ᵐᵒⁿᵒᵐⁱᵃˡ s) = coeff s' x :=
  x.modOf_apply_of_not_exists_add s s'
    (by
      rintro ⟨d, rfl⟩
      exact h le_self_add)

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