Rank of a horizontally partitioned matrix is at most the sum of the block ranks

Proved

MatrixBlockRank.rank_fromCols_le

by mbrcic · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

block-matriceslinear-algebramatricesrank

Let $K$ be a field and let $M$ and $N$ be matrices over $K$ with the same rows, of sizes $l \times n_1$ and $l \times n_2$ . Write $[\,M \;\; N\,]$ for the matrix obtained by placing them side by side, with columns indexed by the disjoint union of the two column index types. Then

\operatorname{rank}\,[\,M \;\; N\,] \;\le\; \operatorname{rank} M + \operatorname{rank} N .

The rank of a matrix is the dimension of the image of the linear map it induces by multiplication on column vectors. The image of $[\,M \;\; N\,]$ is contained in the sum of the images of $M$ and of $N$ , because a vector indexed by the disjoint union splits into its two halves and the block matrix sends it to the sum of the two images; the dimension of a sum of two subspaces is at most the sum of their dimensions. Equality can fail in either direction of the obvious guess: the two images may overlap, in which case the inequality is strict.

The lemma is the ranks-only half of the standard fact that the column space of a block matrix is the sum of the column spaces of its blocks, and it is the form in which that fact is usually consumed: a bound on the rank of a horizontally partitioned matrix by data about its parts.

Formalization Note. No finiteness is required of the row index type, only of the two column index types, so the statement applies to matrices with infinitely many rows.

Preamble

import Mathlib
open Matrix

Formal statement

namespace MatrixBlockRank

theorem rank_fromCols_le {𝕜 : Type*} [Field 𝕜] {l n₁ n₂ : Type*}
    [Fintype n₁] [Fintype n₂]
    (M : Matrix l n₁ 𝕜) (N : Matrix l n₂ 𝕜) :
    (Matrix.fromCols M N).rank ≤ M.rank + N.rank := by
  sorry

end MatrixBlockRank

Source

Atlas-original supporting lemma, written for the AI Safety Formalization Atlas (https://github.com/mbrcic/ai-safety-formalization-atlas, Apache-2.0), module AISafetyAtlas.LinearSystems.MatrixLemmas. It exists to bound the rank of the Hautus pencil [μI - A , B] in a formalization of J. Klamka, “Uncontrollability and unobservability of multivariable systems,” IEEE Transactions on Automatic Control 17(5):725-726, 1972. The statement is standard linear algebra and is not from that paper.

View graph