proposition: Lemma mem_vspaceOver V : vspaceOver V =i (F * V)%VS.
proof: Proof. move=> y; apply/idP/idP; last rewrite unlock; move/coord_span->. rewrite (@memv_suml F0 L) // => i _. by rewrite memv_mul ?subvsP // vbasis_mem ?memt_nth. rewrite memv_suml // => ij _; rewrite -tnth_nth; set x := tnth _ ij. have/allpairsP[[u z] /= [Fu Vz {x}->]]: x \in _ := mem_tnth ij _. by rewrite scalerAl (memvZ (Subvs _)) ?memvZ ?memv_span //= vbasis_mem. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype tuple finfun bigop ssralg countalg) mathcomp(finalg zmodp matrix vector falgebra poly polydiv) mathcomp(mxpoly generic_quotient)