smul — Mathlib

English

Smul of sums matches the product of sums under bilinear action.

Русский

Смул сумм совпадает с произведением сумм при билинейном действии.

LaTeX

$$$ (s.smul t).hsum = (of R).symm (s.hsum \cdot (of R) (t.hsum)) $$$

Lean4

/-- An elementwise scalar multiplication of one summable family on another. -/
@[simps]
def smul (s : SummableFamily Γ R α) (t : SummableFamily Γ' V β) : SummableFamily Γ' V (α × β)
    where
  toFun ab := (of R).symm (s (ab.1) • ((of R) (t (ab.2))))
  isPWO_iUnion_support' := isPWO_iUnion_support_prod_smul s.isPWO_iUnion_support t.isPWO_iUnion_support
  finite_co_support' g := finite_co_support_prod_smul s t g

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