add_divMonomial — Mathlib

English

Division by a monomial is additive: (x+y) /ᵐᵒⁿᵒᵐⁱᵃˡ s = x /ᵐᵒⁿᵒᵐⁱᵃˡ s + y /ᵐᵒⁿᵒᵐⁱᵃˡ s.

Русский

Деление по мономиалу сохраняет сложение: (x+y) / mon ≈ x / mon + y / mon.

LaTeX

$$$ (x+y) /^{mon} s = x /^{mon} s + y /^{mon} s $$$

Lean4

theorem add_divMonomial (x y : MvPolynomial σ R) (s : σ →₀ ℕ) : (x + y) /ᵐᵒⁿᵒᵐⁱᵃˡ s = x /ᵐᵒⁿᵒᵐⁱᵃˡ s + y /ᵐᵒⁿᵒᵐⁱᵃˡ s :=
  map_add (N := _ →₀ _) _ _ _

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