nonempty_equiv_iff_lift_rank_eq — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- Two vector spaces are isomorphic if and only if they have the same dimension. -/
theorem nonempty_equiv_iff_lift_rank_eq :
    Nonempty (M ≃ₗ[R] M') ↔ Cardinal.lift.{v'} (Module.rank R M) = Cardinal.lift.{v} (Module.rank R M') :=
  ⟨fun ⟨h⟩ => LinearEquiv.lift_rank_eq h, fun h => nonempty_linearEquiv_of_lift_rank_eq h⟩

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