finiteDimensional — Mathlib

English

If V and W are finite dimensional vector spaces over a field K, then the space of K-linear maps from V to W is finite dimensional over K.

Русский

Пусть V и W — конечномерные векторные пространства над полем K. Тогда пространство K-линейных отображений V → W { линейных преобразований } над K является конечномерным.

LaTeX

$$$\dim_K\operatorname{Hom}_K(V,W) < \infty$ given finite dimensionality of V and W.$$

Lean4

instance finiteDimensional : FiniteDimensional K (V →ₗ[K] W) :=
  Module.Finite.linearMap _ _ _ _

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