Main

mxrank_sub_eqmx

Section RoucheCapelliTheorems

Type Lemma

Proof Lines 3

Lemma mxrank_sub_eqmx m n p (A : 'M[R]_(m,n)) (B : 'M[R]_(p,n)) : \rank A = \rank B -> (A <= B)%MS -> (A == B)%MS.

Equal rank + submx implies equivalence: if rank(A) = rank(B) and A ≤ B, then A ≡ B. Key lemma for establishing row space equality.

This lemma does not use any other lemmas from the stats.

No lemmas in the stats use this lemma.

Loading source code...