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

Proved

MatrixBlockRank.rank_fromRows_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 columns, of sizes $n_1 \times l$ and $n_2 \times l$ . Write $\begin{pmatrix} M \\ N \end{pmatrix}$ for the matrix obtained by stacking them, with rows indexed by the disjoint union of the two row index types. Then

\operatorname{rank} \begin{pmatrix} M \\ N \end{pmatrix} \;\le\; \operatorname{rank} M + \operatorname{rank} N .

This is the row-stacked counterpart of the bound for a horizontally partitioned matrix, and follows from it because transposition preserves rank and exchanges the two block constructions.

Both forms are used to show that a partitioned matrix fails to have full rank when its blocks are individually too small, which is how one certifies that a pencil test cannot be satisfied.

Formalization Note. Here the shared column index type must be finite, since the transposition step needs the rank of the transpose to be defined on both sides.

Preamble

import Mathlib
open Matrix

Formal statement

namespace MatrixBlockRank

theorem rank_fromRows_le {𝕜 : Type*} [Field 𝕜] {l n₁ n₂ : Type*}
    [Fintype l] [Fintype n₁] [Fintype n₂]
    (M : Matrix n₁ l 𝕜) (N : Matrix n₂ l 𝕜) :
    (Matrix.fromRows 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