Parent
Prerequisite for #292 and Karlin, Total Positivity, Vol. I, Chapter V, Section 1, Proposition 1.2.
Required theorem
For A : Matrix (Fin n) (Fin m) Real with injective mulVec, and every strictly increasing selected column map cols : Fin q -> Fin m, prove that some strictly increasing rows : Fin q -> Fin n gives a nonzero determinant of A.submatrix rows cols.
Proposed name: Matrix.exists_ordered_minor_ne_zero_of_mulVec_injective.
Required proof route
Use Matrix.mulVec_injective_iff to obtain linear independence of all columns, restrict to the selected columns, and extract a nonzero maximal coordinate/minor. An exterior-power proof is acceptable if it packages the coordinate determinant cleanly; an equivalent rank-versus-minor proof is also acceptable.
Acceptance criteria
- Uses full column rank/injective mulVec, not the insufficient assumption q <= rank A.
- Produces a strictly increasing row selector.
- No sorry, axiom, or theorem-shaped Prop definition.
- Reusable independently of Gaussian matrices and sign consistency.
- Full CI is green.
Mathlib currently has the injectivity-to-column-independence bridge and square determinant/invertibility lemmas, but no confirmed rectangular nonzero-minor extraction theorem.
Parent
Prerequisite for #292 and Karlin, Total Positivity, Vol. I, Chapter V, Section 1, Proposition 1.2.
Required theorem
For A : Matrix (Fin n) (Fin m) Real with injective mulVec, and every strictly increasing selected column map cols : Fin q -> Fin m, prove that some strictly increasing rows : Fin q -> Fin n gives a nonzero determinant of A.submatrix rows cols.
Proposed name: Matrix.exists_ordered_minor_ne_zero_of_mulVec_injective.
Required proof route
Use Matrix.mulVec_injective_iff to obtain linear independence of all columns, restrict to the selected columns, and extract a nonzero maximal coordinate/minor. An exterior-power proof is acceptable if it packages the coordinate determinant cleanly; an equivalent rank-versus-minor proof is also acceptable.
Acceptance criteria
Mathlib currently has the injectivity-to-column-independence bridge and square determinant/invertibility lemmas, but no confirmed rectangular nonzero-minor extraction theorem.