modMonomial_add_divMonomial_single

English

For any x and i, the equality X_i · (x / monomial_i 1) + (x mod monomial_i 1) = x holds, expressing the division of x by the monomial with exponent 1 at i.

Русский

Для любых x и i выполняется равенство X_i · (x / мономиал_i 1) + (x mod мономиал_i 1) = x, что выражает разложение x по мономиалу с единичной степенью в i.

LaTeX

$$$$ X_i \\cdot (x /\\!\\!\\!\\!{\\text{monomial}}(Finsupp.single i 1)) + (x /\\!\\!\\!\\!{\\text{modMonomial}}(Finsupp.single i 1)) = x. $$$$

Lean4

theorem modMonomial_add_divMonomial_single (x : MvPolynomial σ R) (i : σ) :
    x %ᵐᵒⁿᵒᵐⁱᵃˡ Finsupp.single i 1 + X i * (x /ᵐᵒⁿᵒᵐⁱᵃˡ Finsupp.single i 1) = x :=
  modMonomial_add_divMonomial _ _

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