linearMap — Mathlib

English

The free module structure on the space of linear maps M → N exists, induced from a natural linear equivalence.

Русский

Существует свободная структура модуля на пространстве линейных отображений M → N, порожденная естественным линейным эквивалентом.

LaTeX

$$$$ \text{Free}(S, \mathrm{Hom}_R(M, N)) $$$$

Lean4

instance linearMap [Module.Free S N] : Module.Free S (M →ₗ[R] N) :=
  Module.Free.of_equiv (linearMapEquivFun R S M N).symm

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