proposition: Lemma module_baseAspace (E0 : {subfield L0}) : (F1 <= E0)%VS -> {E | E0 = baseAspace E & E0 =i E}.
proof: Proof. rewrite -sup_field_module => /module_baseVspace[E defE0 memE0]. suffices algE: is_aspace E by exists (ASpace algE); first apply: val_inj. rewrite /is_aspace has_algid1 -?memE0 ?mem1v //. by apply/prodvP=> u v; rewrite -!memE0; apply: memvM. 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)