smul_compMultilinearMap — Mathlib

English

The two types of composition are associative: (g ∘ g').compMultilinearMap f = g.compMultilinearMap (g'.compMultilinearMap f).

Русский

Два типа композиции совместимы по ассоциативности: (g ∘ g').compMultilinearMap f = g.compMultilinearMap (g'.compMultilinearMap f).

LaTeX

$$$$ (g.comp g').compMultilinearMap f = g.compMultilinearMap (g'.compMultilinearMap f). $$$$

Lean4

@[simp]
theorem smul_compMultilinearMap [Monoid S] [DistribMulAction S M₃] [SMulCommClass R S M₃] (g : M₂ →ₗ[R] M₃) (s : S)
    (f : MultilinearMap R M₁ M₂) : (s • g).compMultilinearMap f = s • g.compMultilinearMap f :=
  rfl

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