compLinearMap_assoc — Mathlib

English

The value of a composed map on an argument equals applying f then g.

Русский

Значение композиции на аргументе равно применению f затем g.

LaTeX

$$$ (f \circ_{\mathrm{Alt}} g)(v) = f( g(v) ) $$$

Lean4

/-- Composing an alternating map twice with the same linear map in each argument is
the same as composing with their composition. -/
theorem compLinearMap_assoc (f : M [⋀^ι]→ₗ[R] N) (g₁ : M₂ →ₗ[R] M) (g₂ : M₃ →ₗ[R] M₂) :
    (f.compLinearMap g₁).compLinearMap g₂ = f.compLinearMap (g₁ ∘ₗ g₂) :=
  rfl

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