proposition: Lemma base_aspaceOver (E : {subfield L}) : (F <= E)%VS -> baseVspace (vspaceOver F E) =i E.
proof: Proof. by rewrite -sup_field_module; apply: base_moduleOver. 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)