nonempty_equiv_iff_rank_eq — Mathlib

English

Two vector spaces are isomorphic if and only if their ranks are equal.

Русский

Две векторные пространства изоморфны тогда и только тогда, когда их ранги равны.

LaTeX

$$$\\text{Nonempty}(M \\simeq_R M') \\iff \\operatorname{rank}_R M = \\operatorname{rank}_R M'$$$

Lean4

/-- Two vector spaces are isomorphic if and only if they have the same dimension. -/
theorem nonempty_equiv_iff_rank_eq : Nonempty (M ≃ₗ[R] M₁) ↔ Module.rank R M = Module.rank R M₁ :=
  ⟨fun ⟨h⟩ => LinearEquiv.rank_eq h, fun h => nonempty_linearEquiv_of_rank_eq h⟩

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