Helper

cancel_row_free

Section counting

Type Lemma

Proof Lines 8

Lemma cancel_row_free p q (g : {linear 'rV[K]_p -> 'rV[K]_q}) (h : {linear 'rV[K]_q -> 'rV[K]_p}) : cancel g h -> row_free (lin1_mx g).

Cancellation implies row freedom: if g has a left inverse h, then the matrix representation of g has full row rank (row_free).

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

No lemmas in the stats use this lemma.

Loading source code...