nonempty_linearEquiv_of_finrank_eq

English

If M and M' are finite-dimensional over R, then Nonempty (M ≃ₗ[R] M') iff finrank_R M = finrank_R M'.

Русский

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

LaTeX

$$[Module.Finite R M] [Module.Finite R M'] \\: (Nonempty (M ≃ₗ[R] M') \\leftrightarrow \\mathrm{finrank}_R M = \\mathrm{finrank}_R M')$$

Lean4

/-- Two finite and free modules are isomorphic if they have the same (finite) rank. -/
theorem nonempty_linearEquiv_of_finrank_eq [Module.Finite R M] [Module.Finite R M']
    (cond : finrank R M = finrank R M') : Nonempty (M ≃ₗ[R] M') :=
  nonempty_linearEquiv_of_lift_rank_eq <| by simp only [← finrank_eq_rank, cond, lift_natCast]

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