finiteDimensional_finsupp — Mathlib

English

Let ι be a finite type and V a finite-dimensional vector space over a division ring K. Then the finsupp space ι →₀ V is finite-dimensional over K.

Русский

Пусть ι — конечный тип, V — конечномерное пространство над K. Тогда пространство FinSupp(ι, V) конечноразмерно над K.

LaTeX

$$$\operatorname{FiniteDimensional}_K(\iota \to_0 V)$$$

Lean4

instance finiteDimensional_finsupp {ι : Type*} [Finite ι] [FiniteDimensional K V] : FiniteDimensional K (ι →₀ V) :=
  Module.Finite.finsupp

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