length_eq_rank — Mathlib

English

For a vector space M over a division ring K, the length equals the rank: length_K(M) = rank_K(M) in ENat.

Русский

Для пространства над делением кольца K имеем: length_K(M) = rank_K(M) в ENat.

LaTeX

$$$\operatorname{length}_K M = (\operatorname{rank}_K M)^{\mathrm{toENat}}$$$

Lean4

theorem length_eq_rank (K M : Type*) [DivisionRing K] [AddCommGroup M] [Module K M] :
    Module.length K M = (Module.rank K M).toENat := by simp [Module.length_of_free]

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