divMonomial_add — Mathlib

English

If a and b are exponent vectors with a+b = s, then dividing by s is the same as dividing by a and then by b: x /^{mon} (a+b) = (x /^{mon} a) /^{mon} b.

Русский

Если a и b заданы так, что a+b = s, то деление по s эквивалентно последовательному делению по a, затем по b.

LaTeX

$$$ x /^{mon} (a+b) = (x /^{mon} a) /^{mon} b $$$

Lean4

theorem divMonomial_add (a b : σ →₀ ℕ) (x : MvPolynomial σ R) : x /ᵐᵒⁿᵒᵐⁱᵃˡ (a + b) = x /ᵐᵒⁿᵒᵐⁱᵃˡ a /ᵐᵒⁿᵒᵐⁱᵃˡ b :=
  x.divOf_add _ _

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