divMonomial_add_modMonomial — Mathlib

English

The remainder plus the monomial times the quotient equals the original polynomial: x % mon s + monomial s 1 * (x / monomial s) = x.

Русский

Остаток плюс мономиал умноженный на частное равны исходному полиному.

LaTeX

$$$x \\%^{mon} s + \\operatorname{monomial}(s)\\,1 \\cdot (x /^{mon} s) = x$$$

Lean4

theorem divMonomial_add_modMonomial (x : MvPolynomial σ R) (s : σ →₀ ℕ) :
    monomial s 1 * (x /ᵐᵒⁿᵒᵐⁱᵃˡ s) + x %ᵐᵒⁿᵒᵐⁱᵃˡ s = x :=
  AddMonoidAlgebra.divOf_add_modOf x s

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