Helper

rouche2

Section RoucheCapelliTheorems

Type Lemma

Proof Lines 10

Lemma rouche2 m n (A : 'M[R]_(m,n)) (B : 'rV_n) : \rank A = \rank (col_mx A B) -> \rank A = m -> exists! x, x *m A = B.

Rouché-Capelli Theorem (Part 2): If system is consistent and rank = #rows, then the solution is unique. Full rank means trivial kernel.

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

No lemmas in the stats use this lemma.

Loading source code...