nonempty_linearEquiv_of_rank_eq — Mathlib

English

If the ranks of M and M' are equal, there exists a linear equivalence M ≃ₗ[R] M'.

Русский

Если ранги M и M' равны, существует линейное эквивалентное отображение M ≃ₗ[R] M'.

LaTeX

$$$\\operatorname{Module.rank}_R M = \\operatorname{Module.rank}_R M' \\Rightarrow \\text{Nonempty}(M \\simeq_R M')$$$

Lean4

/-- Two vector spaces are isomorphic if they have the same dimension. -/
theorem nonempty_linearEquiv_of_rank_eq (cond : Module.rank R M = Module.rank R M₁) : Nonempty (M ≃ₗ[R] M₁) :=
  nonempty_linearEquiv_of_lift_rank_eq <| congr_arg _ cond

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