ofRankEq — Mathlib

English

There exists a linear equivalence between M and M' if and only if the lifted ranks are equal.

Русский

Существует линейное эквивалентное отображение между M и M' тогда и только тогда, когда их поднятые ранги равны.

LaTeX

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

Lean4

/-- Two vector spaces are isomorphic if they have the same dimension. -/
def ofRankEq (cond : Module.rank R M = Module.rank R M₁) : M ≃ₗ[R] M₁ :=
  Classical.choice (nonempty_linearEquiv_of_rank_eq cond)

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