proposition: Lemma cfun_base_free A : free (cfun_base G A).
proof: Proof. have b_i (i : 'I_#|classes G ::&: A|) : (cfun_base G A)`_i = '1_(enum_val i). by rewrite /enum_val -!tnth_nth tnth_map. apply/freeP => s S0 i; move/cfunP/(_ (repr (enum_val i))): S0. rewrite sum_cfunE (bigD1 i) //= big1 ?addr0 => [|j]. rewrite b_i !cfunE; have /setIdP[/imsetP[x Gx ->] _] := enum_valP i. by rewrite cfun_repr cfun_classE Gx class_refl mulr1. apply: contraNeq; rewrite b_i !cfunE mulf_eq0 => /norP[_]. rewrite -(inj_eq enum_val_inj). have /setIdP[/imsetP[x _ ->] _] := enum_valP i; rewrite cfun_repr. have /setIdP[/imsetP[y Gy ->] _] := enum_valP j; rewrite cfun_classE Gy. by rewrite pnatr_eq0 -lt0n lt0b => /class_eqP->. 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)