of_rank_eq_nat

Mathlib.LinearAlgebra.FiniteDimensional.Basic

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

English

If the rank of V over K is a natural n, then V is finite-dimensional.

Русский

Если ранг V над K равен натуральному числу n, то V конечно-мерно.

LaTeX

$$$ \operatorname{ofRankEqNat} : \ \forall n, \ finrank K V = n \Rightarrow FiniteDimensional K V $$$

Lean4

theorem of_rank_eq_nat {n : ℕ} (h : Module.rank K V = n) : FiniteDimensional K V :=
  Module.finite_of_rank_eq_nat h

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

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

Разделы

Аффилиация

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