compMultilinearMap_smul — Mathlib

English

Under a compatible scalar action, the composition respects the scalar: (g ∘ f) scaled equals scaling of the composition.

Русский

При совместимом скалярном действии композиция сохраняет скалярное домножение: масштабирование композиции равно композиции с масштабированием.

LaTeX

$$$$ (s \cdot g).compMultilinearMap f = s \cdot (g.compMultilinearMap f). $$$$

Lean4

@[simp]
theorem compMultilinearMap_smul [DistribSMul S M₂] [DistribSMul S M₃] [SMulCommClass R S M₂] [SMulCommClass R S M₃]
    [CompatibleSMul M₂ M₃ S R] (g : M₂ →ₗ[R] M₃) (s : S) (f : MultilinearMap R M₁ M₂) :
    g.compMultilinearMap (s • f) = s • g.compMultilinearMap f :=
  MultilinearMap.ext fun _ => g.map_smul_of_tower _ _

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