English
If the lift ranks of M and M' are equal, there exists a linear equivalence M ≃ₗ[R] M'.
Русский
Если равны поднесённые ранги M и M', существует линейное эквивалентное отображение M ≃ₗ M'.
LaTeX
$$$ (\\operatorname{lift}(\\operatorname{rank}_R M) = \\operatorname{lift}(\\operatorname{rank}_R M')) \\Rightarrow (M \\simeq_R M')$$$
Lean4
/-- Two vector spaces are isomorphic if they have the same dimension. -/
theorem nonempty_linearEquiv_of_lift_rank_eq
(cnd : Cardinal.lift.{v'} (Module.rank R M) = Cardinal.lift.{v} (Module.rank R M')) : Nonempty (M ≃ₗ[R] M') :=
by
obtain ⟨⟨α, B⟩⟩ := Module.Free.exists_basis (R := R) (M := M)
obtain ⟨⟨β, B'⟩⟩ := Module.Free.exists_basis (R := R) (M := M')
have : Cardinal.lift.{v', v} #α = Cardinal.lift.{v, v'} #β := by rw [B.mk_eq_rank'', cnd, B'.mk_eq_rank'']
exact (Cardinal.lift_mk_eq.{v, v', 0}.1 this).map (B.equiv B')
