Dimension characterizes isomorphism (Three.I.2)

Proved

hefferon_dimension_characterizes_isomorphism

by tianyipeng · Aug 4, 2026 · Mathlib c5ea003 (Lean v4.30.0)

dimensionisomorphismlinear-algebra

Two finite-dimensional vector spaces $V$ and $W$ over the same field $K$ are isomorphic if and only if they have the same dimension.

Preamble

import Mathlib.Data.Matrix.Basic
import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
import Mathlib.LinearAlgebra.Matrix.ToLin

open Matrix

Formal statement

theorem hefferon_dimension_characterizes_isomorphism
    {K V W : Type*} [Field K]
    [AddCommGroup V] [Module K V] [FiniteDimensional K V]
    [AddCommGroup W] [Module K W] [FiniteDimensional K W] :
    Nonempty (V ≃ₗ[K] W) ↔ Module.finrank K V = Module.finrank K W := by
  sorry

Source

Jim Hefferon, *Linear Algebra*, Saint Michael's College, 2020 printing, Chapter Three, Section I.2, Theorem 2.3, p. 194

View graph