Helper

row_free_tr

File dumas2017dual/lib/rouche_capelli.v
Section counting
Type Lemma
Proof Lines 1

Signature

Lemma row_free_tr p q (M : 'M[K]_(p,q)) : p = q -> row_free M^T = row_free M.

Description

Row freedom is transpose-invariant for square matrices: row_free(M^T) = row_free(M) when p = q.

Uses (0)

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

Used By (0)

No lemmas in the stats use this lemma.

Coq Source Code

View on GitHub 
Loading source code...
← Back to Stats