of_finrank_pos

Mathlib.LinearAlgebra.FiniteDimensional.Defs

URI: https://scilib.ai/kg/mathlib#FiniteDimensional.of_finrank_pos

English

If finrank_K V > 0, then V is finite-dimensional over K.

Русский

Если finrank_K V > 0, то V конечномерно над K.

LaTeX

$$$0 < \operatorname{finrank}_K V \Rightarrow \operatorname{FiniteDimensional}_K V$$$

Lean4

theorem of_finrank_pos (h : 0 < finrank K V) : FiniteDimensional K V :=
  Module.finite_of_finrank_pos h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru