Helper

exists_nonzero_kernel

Section RoucheCapelliTheorems

Type Lemma

Proof Lines 6

Lemma exists_nonzero_kernel m n (A : 'M[R]_(m, n)) : (\rank A < m)%N -> exists y : 'rV_m, y *m A = 0 /\ y != 0.

Rank-deficient matrices have nontrivial kernels: if rank(A) < m, there exists nonzero y with yA = 0. Foundation for solution counting.

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

No lemmas in the stats use this lemma.

Loading source code...