support_single_mul_subset — Mathlib

English

The support of a product by a fixed coefficient is contained in the image of the support under the corresponding embedding.

Русский

Опора произведения на фиксированный коэффициент содержится в образе опоры через соответствующее вложение.

LaTeX

$$(Supp( a * f ) ⊆ image (a * ·) f.support)$$

Lean4

theorem support_single_mul_subset [DecidableEq G] [Mul G] (f : MonoidAlgebra k G) (r : k) (a : G) :
    (single a r * f : MonoidAlgebra k G).support ⊆ Finset.image (a * ·) f.support :=
  (support_mul _ _).trans <|
    (Finset.image₂_subset_right support_single_subset).trans <| by rw [Finset.image₂_singleton_left]

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