divMonomial_monomial_mul — Mathlib

English

Dividing v by monomial a after multiplying by monomial a 1 yields the original v: monomial a 1 · x /^{mon} a = x.

Русский

Деление после умножения на мономиал a 1 возвращает исходный полином: monomial a 1 · x /^{mon} a = x.

LaTeX

$$$\\operatorname{monomial}(a) \\; 1 \\cdot x /^{mon} a = x$$$

Lean4

@[simp]
theorem divMonomial_monomial_mul (a : σ →₀ ℕ) (x : MvPolynomial σ R) : monomial a 1 * x /ᵐᵒⁿᵒᵐⁱᵃˡ a = x :=
  x.of'_mul_divOf _

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