proposition: Lemma Falgebra_FieldMixin : GRing.integral_domain_axiom aT -> GRing.field_axiom aT.
proof: Proof. move=> domT u nz_u; apply/unitrP. have kerMu: lker (amulr u) == 0%VS. rewrite eqEsubv sub0v andbT; apply/subvP=> v; rewrite memv_ker lfunE /=. by move/eqP/domT; rewrite (negPf nz_u) orbF memv0. have /memv_imgP[v _ vu1]: 1 \in limg (amulr u); last rewrite lfunE /= in vu1. suffices /eqP->: limg (amulr u) == fullv by rewrite memvf. by rewrite -dimv_leqif_eq ?subvf ?limg_dim_eq // (eqP kerMu) capv0. exists v; split=> //; apply: (lker0P kerMu). by rewrite !lfunE /= -mulrA -vu1 mulr1 mul1r. 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)