English
A specialized version states llcomp applied to maps equals the nested application of the maps: llcomp g f m = g(f(m)).
Русский
Уточненная версия говорит, что применение llcomp к картам эквивалентно вложенному применению: llcomp g f m = g(f(m)).
LaTeX
$$$$llcomp\_{\sigma} (g) (f) (m) = g(f(m)).$$$$
Lean4
/-- Composing a linear map `P →ₛₗ[σ₃₄] Q` and a bilinear map `M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P` to
form a bilinear map `M →ₛₗ[σ₁₄] N →ₛₗ[σ₂₄] Q`.
See `LinearMap.compr₂` for a version of this definition, which does not support semi-linear maps but
which does support towers of scalars. -/
def compr₂ₛₗ (f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P) (g : P →ₛₗ[σ₃₄] Q) : M →ₛₗ[σ₁₄] N →ₛₗ[σ₂₄] Q :=
llcomp _ N P Q g ∘ₛₗ f
