proposition: Lemma memvV A u : (u^-1 \in A) = (u \in A).
proof: Proof. suffices{u} invA: invr_closed A by apply/idP/idP=> /invA; rewrite ?invrK. move=> u Au; have [Uu | /invr_out-> //] := boolP (u \is a GRing.unit). rewrite memvE -(limg_ker0 _ _ (lker0_amulr Uu)) limg_line lfunE /= mulVr //. suff ->: (amulr u @: A)%VS = A by rewrite -memvE -algid_eq1 (unitr_algid1 Au). by apply/eqP; rewrite limg_amulr -dimv_leqif_eq ?prodv_sub ?dim_cosetv_unit. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype div tuple finfun bigop ssralg) mathcomp(finalg zmodp matrix vector poly)