support_mul_X — Mathlib

English

The support of the product p · X_s equals the image of the support of p under the embedding that adds 1 to the exponent of s.

Русский

Поддержка произведения p · X_s равна образу поддержки p под отображением, добавляющим единицу к степени в координате s.

LaTeX

$$(p \\cdot X s).\\text{support} = p.\\text{support}.map(\\text{addRightEmbedding}(Finsupp.single s 1))$$

Lean4

@[simp]
theorem support_mul_X (s : σ) (p : MvPolynomial σ R) :
    (p * X s).support = p.support.map (addRightEmbedding (Finsupp.single s 1)) :=
  AddMonoidAlgebra.support_mul_single p _ (by simp) _

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