Rank-Nullity Theorem ( $\dim V = \dim \ker f + \dim \operatorname{im} f$ )

Proved

HoffmanKunze.rank_nullity

by intro_user7980 · Sep 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

linear-algebrarank-nullitytextbook-formalization

Let $K$ be a field, $V$ a finite-dimensional $K$ -vector space, and $W$ any $K$ -vector space. For any linear map $f : V o W$ ,

\dim_K V \;=\; \dim_K \operatorname{im} f \;+\; \dim_K \ker f,

where $\dim_K$ denotes the $K$ -dimension (the cardinality of any basis). The number $\dim_K \operatorname{im} f$ is called the rank of $f$ , and $\dim_K \ker f$ its nullity. Thus the dimension of the domain equals the sum of rank and nullity.

Preamble

import Mathlib.LinearAlgebra.Dimension.Finrank
import Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
open Module

Formal statement

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

Source

Hoffman, Kenneth; Kunze, Ray. *Linear Algebra*, 2nd ed. Prentice-Hall, 1971. Theorem 2.3, p. 70. https://archive.org/details/linearalgebra00hoff

View graph

Rank-Nullity Theorem (dim⁡V=dim⁡ker⁡f+dim⁡im⁡f\dim V = \dim \ker f + \dim \operatorname{im} fdimV=dimkerf+dimimf)

Rank-Nullity Theorem ( $\dim V = \dim \ker f + \dim \operatorname{im} f$ )