ofLiftRankEq — Mathlib

English

Given equality of lift ranks, return a LinearEquiv between M and M'.

Русский

При равенстве лифт рангов возвращается линейное эквивелентное отображение.

LaTeX

$$$\\operatorname{ofLiftRankEq} (\\text{cond} : \\operatorname{lift}(\\operatorname{rank}_R M) = \\operatorname{lift}(\\operatorname{rank}_R M')) : M \\simeq_R M'$$$

Lean4

/-- Two vector spaces are isomorphic if they have the same dimension. -/
def ofLiftRankEq (cond : Cardinal.lift.{v'} (Module.rank R M) = Cardinal.lift.{v} (Module.rank R M')) : M ≃ₗ[R] M' :=
  Classical.choice (nonempty_linearEquiv_of_lift_rank_eq cond)

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