support_divMonomial — Mathlib · SciLib

English

The support of the quotient equals the preimage under the addition map of the support of the original polynomial.

Русский

Поддержка частного после деления по мономиалу равна предобразу опорного множества исходного полинома по сложению степеней.

LaTeX

$$$\\operatorname{support}(x /^{mon} s) = \\operatorname{preimage}(\\,\\operatorname{add}\\_\\text{right}\\, s)\\,\\operatorname{support}(x)$$$

Lean4

@[simp]
theorem support_divMonomial (s : σ →₀ ℕ) (x : MvPolynomial σ R) :
    (x /ᵐᵒⁿᵒᵐⁱᵃˡ s).support = x.support.preimage _ (add_right_injective s).injOn :=
  rfl

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