coeff_divMonomial — Mathlib

English

The coefficient of s' in the quotient x /ᵐᵒⁿᵒᵐⁱᵃˡ s equals the coefficient of s + s' in x.

Русский

Коэффициент при s' в частном x /ᵐᵒⁿᵒᵐⁱᵃˡ s совпадает с коэффициентом при s + s' в x.

LaTeX

$$$\\operatorname{coeff}_{s'}(x /^{mon} s) = \\operatorname{coeff}_{s+s'}(x)$$$

Lean4

@[simp]
theorem coeff_divMonomial (s : σ →₀ ℕ) (x : MvPolynomial σ R) (s' : σ →₀ ℕ) :
    coeff s' (x /ᵐᵒⁿᵒᵐⁱᵃˡ s) = coeff (s + s') x :=
  rfl

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