llcomp_apply' — Mathlib

English

llcomp is the bilinear map that takes a linear map N → P and a linear map M → N and returns their composition M → P.

Русский

llcomp — билинейное отображение, которое берет линейное отображение N → P и линейное отображение M → N и возвращает их композицию M → P.

LaTeX

$$$$\text{llcomp}: (N \to P) \to_l[R] (M \to N) \to_l[R] (M \to P)$$ with $(llcomp\ f\ g)(m) = f(g(m)).$$$

Lean4

theorem llcomp_apply' (f : N →ₛₗ[σ₂₃] P) (g : M →ₛₗ[σ₁₂] N) : llcomp _ M N P f g = f ∘ₛₗ g :=
  rfl

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