Linear representative selection
Abstract
Dimension inequalities yield spanning representatives and nonzero matrix minors.
Theorem 1.1 (spanning_representatives).
Proof. Machine-checked in Lean as D5/S3/Combinatorics/Matroids/LinearRado.spanning_representatives (✓ std3). ∎
Citation. Richard Rado (1942). A theorem on independence relations. DOI: 10.1093/qmath/os-13.1.83. URL: https://doi.org/10.1093/qmath/os-13.1.83.
Commentary.
The linear form of Rado’s theorem selects one vector from each subspace. Its deficit version gives a spanning family: add an auxiliary space of dimension k − Module.finrank F W, choose independent representatives there, and project to W. The finite-set proof separates a proper set with equality in the dimension inequality; otherwise it passes to the quotient by a line.
Theorem 1.2 (exists_nonsingular_rows).
Proof. Machine-checked in Lean as D5/S3/Combinatorics/Matroids/LinearRado.exists_nonsingular_rows (✓ std3). ∎
Source. Repository-derived.
Commentary.
A finite family spanning a coordinate space contains a basis. Selecting its row indices gives a square submatrix with nonzero determinant.
Theorem 1.3 (independent_support_matching).
Proof. Machine-checked in Lean as D5/S3/Combinatorics/Matroids/LinearRado.independent_support_matching (✓ std3). ∎
Source. Repository-derived.
Commentary.
A linearly independent family of coordinate vectors has an injective selection of nonzero coordinates. A nonsingular maximal minor has a nonzero term in its determinant expansion, and the corresponding permutation supplies the selection.