proposition: Fact cfun_vect_iso : Vector.axiom #|classes G| classfun.
proof: Proof. exists (fun phi => \row_i phi (repr (enum_val i))) => [a phi psi|]. by apply/rowP=> i; rewrite !(mxE, cfunE). set n := #|_|; pose eK x : 'I_n := enum_rank_in (classes1 _) (x ^: G). have rV2vP v : is_class_fun G [ffun x => v (eK x) *+ (x \in G)]. apply: intro_class_fun => [x y Gx Gy | x /negbTE/=-> //]. by rewrite groupJr // /eK classGidl. exists (fun v : 'rV_n => Cfun 0 (rV2vP (v 0))) => [phi | v]. apply/cfun_in_genP=> x Gx; rewrite cfunE Gx mxE enum_rankK_in ?mem_classes //. by have [y Gy ->] := repr_class <<B>> x; rewrite cfunJgen. apply/rowP=> i; rewrite mxE cfunE; have /imsetP[x Gx def_i] := enum_valP i. rewrite def_i; have [y Gy ->] := repr_class <<B>> x. by rewrite groupJ // /eK classGidl // -def_i enum_valK_in. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime order) mathcomp(ssralg poly finset fingroup morphism perm) mathcomp(automorphism quotient finalg action gproduct) mathcomp(zmodp commutator cyclic center pgroup sylow) mathcomp(matrix vector falgebra ssrnum algC algnum) mathcomp(archimedean)