support_mul — Mathlib

English

For any a,b in k[G], the support of their product is contained in the Minkowski sum of their supports: supp(a b) ⊆ supp(a) + supp(b).

Русский

Для любых элементов a,b в k[G] опора произведения a b содержится в сумме опор: supp(a b) ⊆ supp(a) + supp(b).

LaTeX

$$$\\operatorname{supp}(a b) \\subseteq \\operatorname{supp}(a) + \\operatorname{supp}(b)$$$

Lean4

theorem support_mul [DecidableEq G] [Add G] (a b : k[G]) : (a * b).support ⊆ a.support + b.support :=
  @MonoidAlgebra.support_mul k (Multiplicative G) _ _ _ _ _

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