dfinsuppFamily_compLinearMap_lsingle

English

Scaling the family of multilinear maps by a scalar s scales the entire dfinsuppFamily accordingly: dfinsuppFamily (s • f) = s • dfinsuppFamily f.

Русский

Умножение всей семьи мультилейных отображений на скаляр s пропорционально масштабирует и dfinsuppFamily: dfinsuppFamily (s • f) = s • dfinsuppFamily f.

LaTeX

$$$\dfinsuppFamily (s \cdot f) = s \cdot \dfinsuppFamily f$$$

Lean4

@[simp]
theorem dfinsuppFamily_compLinearMap_lsingle [∀ i, DecidableEq (κ i)]
    (f : Π (p : Π i, κ i), MultilinearMap R (fun i ↦ M i (p i)) (N p)) (p : ∀ i, κ i) :
    (dfinsuppFamily f).compLinearMap (fun i => DFinsupp.lsingle (p i)) =
      (DFinsupp.lsingle p).compMultilinearMap (f p) :=
  MultilinearMap.ext <| dfinsuppFamily_single f p

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