fg_iff_finiteDimensional — Mathlib

English

In a finite-dimensional space, the finite-dimensional dimension equals the rank as a cardinal.

Русский

В конечномерном пространстве размерность равна рангу как кардинал.

LaTeX

$$(\operatorname{finrank}_K V) = \operatorname{Module.rank}_K V$$

Lean4

/-- A submodule is finitely generated if and only if it is finite-dimensional -/
theorem fg_iff_finiteDimensional (s : Submodule K V) : s.FG ↔ FiniteDimensional K s :=
  (fg_top s).symm.trans Module.finite_def.symm

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