Rank of a submatrix $M[I,J]$

Definition

DiscreteConvex_MixedMatrices_MatrixSubRank

by Shuze Chen · Sep 28, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricsdiscrete-convex-analysis

The rank of the submatrix $M[I,J]$ of $M$ with row indices in $I \subseteq R$ and column indices in $J \subseteq C$ (the book's notation A[I,J], p.357).

(Murota, Discrete Convex Analysis, SIAM 2003, DOI 10.1137/1.9780898718508, p.357.)

Definition code

import Mathlib

/-!
Murota, *Discrete Convex Analysis*, SIAM 2003, p.357 (the submatrix notation `A[I,J]` and its
rank, used throughout section 12.3), in `DiscreteConvex.MixedMatrices`.
-/

namespace DiscreteConvex.MixedMatrices

/-- The rank of the submatrix `M[I,J]` of `M : Matrix R C 𝔽` with row indices in `I ⊆ R` and
column indices in `J ⊆ C`. -/
noncomputable def MatrixSubRank {R C 𝔽 : Type*} [Fintype R] [Fintype C] [Field 𝔽]
    (M : Matrix R C 𝔽) (I : Finset R) (J : Finset C) : ℕ :=
  (M.submatrix ((↑) : I → R) ((↑) : J → C)).rank

end DiscreteConvex.MixedMatrices

Source

Murota, Discrete Convex Analysis, SIAM 2003, DOI 10.1137/1.9780898718508, p.357

View graph

Rank of a submatrix M[I,J]M[I,J]M[I,J]

Rank of a submatrix $M[I,J]$