proposition: Lemma primeChar_vectAxiom : {v2r : R -> 'rV_n | linear v2r & bijective v2r}.
proof: Proof. have /isog_isom/=[f /isomP[injf im_f]]: [set: R] \isog [set: 'rV['F_p]_n]. rewrite (@isog_abelem_card _ _ p) fin_Fp_lmod_abelem //=. by rewrite !cardsT card_primeChar card_mx mul1n card_Fp. exists f; last by exists (invm injf) => x; rewrite ?invmE ?invmK ?im_f ?inE. move=> a x y; rewrite [a *: _]mulr_natl morphM ?morphX ?inE // zmodXgE. by congr (_ + _); rewrite -scaler_nat natr_Zp. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype div tuple bigop prime finset fingroup) mathcomp(ssralg poly polydiv morphism action countalg) mathcomp(finalg zmodp cyclic center pgroup abelian matrix) mathcomp(mxpoly vector falgebra fieldext separable galois)