ofFinrankEq — Mathlib

English

For finite-dimensional M and M', there is a nonempty linear equivalence iff finrank_R M = finrank_R M'.

Русский

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

LaTeX

$$$[Module.Finite\\ R\\ M] [Module.Finite\\ R\\ M'] : (Nonempty (M \\simeq_R M') \\iff finrank_R M = finrank_R M')$$$

Lean4

/-- Two finite and free modules are isomorphic if they have the same (finite) rank. -/
noncomputable def ofFinrankEq [Module.Finite R M] [Module.Finite R M'] (cond : finrank R M = finrank R M') :
    M ≃ₗ[R] M' :=
  Classical.choice <| FiniteDimensional.nonempty_linearEquiv_of_finrank_eq cond

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