compMultilinearMap_compLinearMap — Mathlib

English

The composition with a linear map followed by a linearization equals the sequential composition: g.compMultilinearMap (f.compLinearMap f') = (g.compMultilinearMap f).compLinearMap f'.

Русский

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

LaTeX

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

Lean4

/-- The two types of composition are associative. -/
theorem compMultilinearMap_compLinearMap (g : M₂ →ₗ[R] M₃) (f : MultilinearMap R M₁ M₂) (f' : ∀ i, M₁' i →ₗ[R] M₁ i) :
    g.compMultilinearMap (f.compLinearMap f') = (g.compMultilinearMap f).compLinearMap f' :=
  rfl

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