support_smul — Mathlib

English

The support of a product is contained in the sum of supports of the factors.

Русский

Опора произведения содержится в сумме опор множителей.

LaTeX

$$$\\\\forall p,q: MvPolynomial\\\\sigma\\\\,R, \\\\operatorname{support}(p q) \\\\subseteq \\\\operatorname{support}(p) + \\\\operatorname{support}(q)$$$

Lean4

theorem support_smul {S₁ : Type*} [SMulZeroClass S₁ R] {a : S₁} {f : MvPolynomial σ R} : (a • f).support ⊆ f.support :=
  Finsupp.support_smul

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