proposition: Lemma linear_of_free (rT : lmodType K) X (fX : seq rT) : {f : {linear vT -> rT} | free X -> size fX = size X -> map f X = fX}.
proof: Proof. pose f u := \sum_i coord (in_tuple X) i u *: fX`_i. have lin_f: linear f. move=> k u v; rewrite scaler_sumr -big_split; apply: eq_bigr => i _. by rewrite /= scalerA -scalerDl linearP. pose flM := GRing.isLinear.Build _ _ _ _ f lin_f. pose fL : GRing.Linear.type _ _ := HB.pack f flM. exists fL => freeX eq_szX. apply/esym/(@eq_from_nth _ 0); rewrite ?size_map eq_szX // => i ltiX. rewrite (nth_map 0) //= /f (bigD1 (Ordinal ltiX)) //=. rewrite big1 => [|j /negbTE neqji]; rewrite (coord_free (Ordinal _)) //. by rewrite eqxx scale1r addr0. by rewrite eq_sym neqji scale0r. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)