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 ?

Do not unfold, use the theory of both, e.g. `freeP`

and `mulmx_free_eq0`

/ `inj_row_free`

.

```
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.
```

Thank you very much !

Last updated: Feb 08 2023 at 08:02 UTC