dfinsuppFamily_smul — Mathlib

English

Scaling the input by a scalar resizes the piFamily output accordingly: piFamily (s • f) = s • piFamily f.

Русский

Умножение входа на скаляр приводит к соответствующему изменению выхода piFamily: piFamily (s • f) = s • piFamily f.

LaTeX

$$$\piFamily (instHSMul.hSMul\s f) = s \cdot \piFamily f$$$

Lean4

@[simp]
theorem dfinsuppFamily_smul [Monoid S] [∀ p, DistribMulAction S (N p)] [∀ p, SMulCommClass R S (N p)] (s : S)
    (f : Π (p : Π i, κ i), MultilinearMap R (fun i ↦ M i (p i)) (N p)) :
    dfinsuppFamily (s • f) = s • dfinsuppFamily f := by ext; simp

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