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: Oct 13 2024 at 01:02 UTC