English
There is a natural A-linear map from the R-linear endomorphisms M → A to the functions M → A, given by forgetting the R-linear structure: f ↦ f.toFun. This map is A-linear.
Русский
Существует естественный A-линейный отображение из пространства R-линейных отображений M→A в множество функций M→A, задаваемое f ↦ f.toFun; такое отображение является A-линейным.
LaTeX
$$$\mathrm{ltoFun} : (M\\to_{\\!R} A) \\to_{\\!A} (M \\to A),\\quad \\mathrm{ltoFun}(f) = f\\,\\text{(как функция)}$$$
Lean4
/-- `A`-linearly coerce an `R`-linear map from `M` to `A` to a function, given an algebra `A` over
a commutative semiring `R` and `M` a module over `R`. -/
def ltoFun (R : Type u) (M : Type v) (A : Type w) [CommSemiring R] [AddCommMonoid M] [Module R M] [CommSemiring A]
[Algebra R A] : (M →ₗ[R] A) →ₗ[A] M → A where
toFun f := f.toFun
map_add' _ _ := rfl
map_smul' _ _ := rfl
