Helper

kernel_coeff_exists

Section RoucheCapelliTheorems

Type Lemma

Proof Lines 6

Lemma kernel_coeff_exists m n p (A : 'M[R]_(m, n)) (X : 'M[R]_(n, p)) : A *m X = 0 -> exists P : 'M[R]_(p, n), X^T = P *m kermx A^T.

Kernel coefficient existence: if AX = 0, then X^T can be written as P * ker(A^T) for some P. Explicit decomposition in kernel basis.

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

No lemmas in the stats use this lemma.

Loading source code...