nonempty_linearEquiv_iff_finrank_eq

English

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

Русский

Для конечномерных M и 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 and only if they have the same (finite) rank. -/
theorem nonempty_linearEquiv_iff_finrank_eq [Module.Finite R M] [Module.Finite R M'] :
    Nonempty (M ≃ₗ[R] M') ↔ finrank R M = finrank R M' :=
  ⟨fun ⟨h⟩ => h.finrank_eq, fun h => nonempty_linearEquiv_of_finrank_eq h⟩

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