## Stream: math-comp users

### Topic: row_free vs free

#### Quentin Canu (Oct 01 2021 at 11:55):

Hello everyone ! I am currently struggling with the following lemma :

``````Lemma row_free_free {m n : nat} (A : 'M[R]_(m,n)) : row_free A = free [seq row i A | i <- enum 'I_m].
``````

It should be elementary, but even by unfolding `free` `span` and everything, I still experience issues with the whole `Vector.InternalTheory` module. Do you have an idea on the way to prove this ?

#### Cyril Cohen (Oct 01 2021 at 12:33):

Do not unfold, use the theory of both, e.g. `freeP` and `mulmx_free_eq0` / `inj_row_free`.

#### Cyril Cohen (Oct 01 2021 at 12:51):

``````Lemma row_free_free {R : fieldType} {m n : nat} (A : 'M[R]_(m,n)) :
row_free A = free [tuple row i A | i < m].
Proof.
apply/idP/freeP => [/mulmx_free_eq0 mulAeq0 k|mulA0].
under eq_bigr do rewrite -tnth_nth tnth_map tnth_ord_tuple.
move=> kA0 i; have /eqP : \row_i k i *m A = 0.
by rewrite mulmx_sum_row; under eq_bigr do rewrite mxE.
by rewrite mulAeq0 => /eqP/rowP/(_ i); rewrite !mxE.
apply/inj_row_free => v; rewrite mulmx_sum_row => vA0.
apply/rowP => i; rewrite mxE mulA0//.
by under eq_bigr do rewrite -tnth_nth tnth_map tnth_ord_tuple.
Qed.
``````

#### Quentin Canu (Oct 01 2021 at 13:06):

Thank you very much !

Last updated: Feb 08 2023 at 08:02 UTC