llcomp — Mathlib

English

The bilinear composition llcomp satisfies (llcomp f g) applied to m equals f applied to g(m).

Русский

Композиция llcomp удовлетворяет (llcomp f g)(m) = f(g(m)).

LaTeX

$$$$(\text{llcomp}\; f\; g)(m) = f\bigl(g(m)\bigr).$$$$

Lean4

/-- Composing linear maps as a bilinear map from `(M →ₛₗ[σ₁₂] N) × (N →ₛₗ[σ₂₃] P)`
to `M →ₛₗ[σ₁₃] P`. -/
def llcomp : (N →ₛₗ[σ₂₃] P) →ₗ[R₃] (M →ₛₗ[σ₁₂] N) →ₛₗ[σ₂₃] M →ₛₗ[σ₁₃] P :=
  flip
    { toFun := lcompₛₗ _ P σ₂₃
      map_add' := fun _f _f' => ext₂ fun g _x => g.map_add _ _
      map_smul' := fun (_c : R₂) _f => ext₂ fun g _x => g.map_smulₛₗ _ _ }

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