support_X_mul — Mathlib

English

Analogously, the support of X_s · p is the image of the support of p under the embedding that adds 1 to the exponent of s on the left.

Русский

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

LaTeX

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

Lean4

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

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