support_mul — Mathlib

English

The support of a product in a monoid algebra is contained in the product of supports, i.e., Supp(a·b) ⊆ Supp(a)·Supp(b).

Русский

Опора произведения в моноидальной алгебре содержится внутри произведения опор факторов: Supp(a·b) ⊆ Supp(a)·Supp(b).

LaTeX

$$Supp( a * b ) ⊆ Supp(a) * Supp(b)$$

Lean4

theorem support_mul [Mul G] [DecidableEq G] (a b : MonoidAlgebra k G) : (a * b).support ⊆ a.support * b.support :=
  by
  rw [MonoidAlgebra.mul_def]
  exact
    support_sum.trans <|
      biUnion_subset.2 fun _x hx ↦
        support_sum.trans <|
          biUnion_subset.2 fun _y hy ↦ support_single_subset.trans <| singleton_subset_iff.2 <| mem_image₂_of_mem hx hy

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