Any two bases of a space have the same size (Two.III.2)

Proved

hefferon_any_two_bases_have_the_same_size

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

basisdimensionlinear-algebra

Let $V$ be a vector space over a field $K$ . If $V$ has a basis indexed by a finite set $\iota$ and also a basis indexed by a finite set $\kappa$ , then $\iota$ and $\kappa$ have the same number of elements. Hence the dimension of a finite-dimensional vector space is well defined.

Preamble

import Definitions.Def_hefferon_prelude

open Matrix
open HefferonLinAlg

Formal statement

theorem hefferon_any_two_bases_have_the_same_size
    {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
    {ι κ : Type*} [Fintype ι] [Fintype κ] (B : Module.Basis ι K V) (C : Module.Basis κ K V) :
    Fintype.card ι = Fintype.card κ := by
  sorry

Source

Jim Hefferon, *Linear Algebra*, Saint Michael's College, 2020 printing, Chapter Two, Section III.2, Theorem 2.4, p. 139

View graph