of_finrank_eq_succ — Mathlib

English

If finrank_K V = n + 1 for some natural number n, then V is finite-dimensional over K.

Русский

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

LaTeX

$$$\operatorname{finrank}_K V = n + 1 \Rightarrow \operatorname{FiniteDimensional}_K V$$$

Lean4

theorem of_finrank_eq_succ {n : ℕ} (hn : finrank K V = n.succ) : FiniteDimensional K V :=
  Module.finite_of_finrank_eq_succ hn

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