English
For linear maps over a k-algebra, if the source and target are finite dimensional, then the space of such maps is finite dimensional over k.
Русский
Для линейных отображений над k-алгеброй, если исходное и целевое пространства конечномерны, то множество таких отображений имеет конечную размерность над k.
LaTeX
$$$\operatorname{Hom}_A(V,W)$ is finite dimensional over K when V and W are finite dimensional over K and A is a k-algebra with the given structure.$$
Lean4
/-- Linear maps over a `k`-algebra are finite dimensional (over `k`) if both the source and
target are, as they form a subspace of all `k`-linear maps. -/
instance finiteDimensional' : FiniteDimensional K (V →ₗ[A] W) :=
FiniteDimensional.of_injective (restrictScalarsₗ K A V W K) (restrictScalars_injective _)
