Stream: math-comp users

Topic: row_free vs free


view this post on Zulip 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 ?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Quentin Canu (Oct 01 2021 at 13:06):

Thank you very much !


Last updated: Mar 28 2024 at 09:01 UTC