divMonomial_add_modMonomial_single

English

Let x be a polynomial and i an index. Then X_i multiplies the quotient (x divided by the monomial with exponent 1 at i) and together with the remainder equals x; i.e. X_i · (x / monomial_i 1) + (x mod monomial_i 1) = x.

Русский

Пусть x — многочлен, а i — индекс. Тогда mинамоном X_i умножает частное от деления x на мономиал с единичной степенью на i и вместе с остатком даёт x; то есть X_i · (x / мономиал_i 1) + (x mod мономиал_i 1) = x.

LaTeX

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

Lean4

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

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