comp_compMultilinearMap — Mathlib

English

Composition of two linear maps with a multilinear map is associative: (g ∘ g').compMultilinearMap f = g.compMultilinearMap (g'.compMultilinearMap f).

Русский

Композиция двух линейных отображений с мультиленейным отображением ассоциативна: (g ∘ g').compMultilinearMap f = g.compMultilinearMap (g'.compMultilinearMap f).

LaTeX

$$$$(g\circ g').compMultilinearMap f = g.compMultilinearMap (g'.compMultilinearMap f).$$$$

Lean4

theorem comp_compMultilinearMap (g : M₃ →ₗ[R] M₄) (g' : M₂ →ₗ[R] M₃) (f : MultilinearMap R M₁ M₂) :
    (g.comp g').compMultilinearMap f = g.compMultilinearMap (g'.compMultilinearMap f) :=
  rfl

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