English
There is a bilinear-like structure yielding a linear map applyₗ' that ties a vector v and a linear map to a higher-order map; it satisfies standard linearity in both arguments.
Русский
Существуют подобные линейности конструкции applyₗ', связывающие вектор и линейное отображение с высшими отображениями; выполняются стандартные свойства линейности по обоим аргументам.
LaTeX
$$applyₗ' : M →+ (M →ₗ[R] M₂) →ₗ[S] M₂ with toFun(v) f = f(v)$$
Lean4
/-- Applying a linear map at `v : M`, seen as a linear map from `M →ₗ[R] M₂` to `M₂`.
See also `LinearMap.applyₗ'` for a version that works with two different semirings.
This is the `LinearMap` version of `toAddMonoidHom.eval`. -/
@[simps]
def applyₗ : M →ₗ[R] (M →ₗ[R] M₂) →ₗ[R] M₂ :=
{ applyₗ' R with
toFun := fun v => { applyₗ' R v with toFun := fun f => f v }
map_smul' := fun _ _ => LinearMap.ext fun f => map_smul f _ _ }
