proposition: Lemma aspaceOverP (E_F : {subfield L_F}) : {E | [/\ E_F = aspaceOver E, (F <= E)%VS & E_F =i E]}.
proof: Proof. have [V [defEF modV memV]] := vspaceOverP E_F. have algE: has_algid V && (V * V <= V)%VS. rewrite has_algid1; last by rewrite -memV mem1v. by apply/prodvP=> u v; rewrite -!memV; apply: memvM. by exists (ASpace algE); rewrite -sup_field_module; split; first apply: val_inj. 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)