mul_monomial_modMonomial — Mathlib

English

Dividing by a monomial after multiplying by monomial s 1 yields zero remainder: (monomial s 1) · x /^{mon} s = 0.

Русский

Деление после умножения на мономиал s 1 даёт остаток 0: (monomial s 1) · x /^{mon} s = 0.

LaTeX

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

Lean4

@[simp]
theorem mul_monomial_modMonomial (s : σ →₀ ℕ) (x : MvPolynomial σ R) : x * monomial s 1 %ᵐᵒⁿᵒᵐⁱᵃˡ s = 0 :=
  x.mul_of'_modOf _

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