compRight — Mathlib

English

Post-composition by a fixed linear map f gives a linear map that sends g to f ∘ g; i.e., composing on the right with f is linear in g.

Русский

Постсложение фиксированного линейного отображения f дает линейное отображение от g в f ∘ g; т.е. композиция справа по f линейна по g.

LaTeX

$$compRight(f) (g) = f ∘ g$$

Lean4

/-- Composition by `f : M₂ → M₃` is a linear map from the space of linear maps `M → M₂`
to the space of linear maps `M → M₃`. -/
def compRight (f : M₁ →ₗ[R] M₂) : (M →ₗ[R] M₁) →ₗ[S] M →ₗ[R] M₂
    where
  toFun g := f.comp g
  map_add' _ _ := LinearMap.ext fun _ ↦ map_add f _ _
  map_smul' _ _ := LinearMap.ext fun _ ↦ map_smul_of_tower ..

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