length_eq_finrank — Mathlib

English

For a finite-dimensional K-vector space M, length_K(M) equals finrank_K(M) cast to ENat.

Русский

Для конечно-размерного пространства над K: длина равна финранку, приведённому к ENat.

LaTeX

$$$\operatorname{length}_K M = \operatorname{finrank}_K M$.cast$$

Lean4

theorem length_eq_finrank (K M : Type*) [DivisionRing K] [AddCommGroup M] [Module K M] [Module.Finite K M] :
    Module.length K M = Module.finrank K M := by simp [Module.length_of_free]

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