Rank plus nullity equals the dimension of the domain (Three.II.2)

Proved

hefferon_rank_plus_nullity

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

linear-algebralinear-maprank-nullity

Let $f : V \to W$ be a linear map between vector spaces over a field $K$ , with $V$ finite-dimensional. Then the dimension of the range space of $f$ plus the dimension of its null space equals the dimension of $V$ .

Preamble

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

open Matrix

Formal statement

theorem hefferon_rank_plus_nullity
    {K V W : Type*} [Field K]
    [AddCommGroup V] [Module K V] [FiniteDimensional K V]
    [AddCommGroup W] [Module K W] (f : V →ₗ[K] W) :
    Module.finrank K (LinearMap.range f) + Module.finrank K (LinearMap.ker f) =
      Module.finrank K V := by
  sorry

Source

Jim Hefferon, *Linear Algebra*, Saint Michael's College, 2020 printing, Chapter Three, Section II.2, Theorem 2.14, p. 213

View graph