proposition: Lemma cfCycTIbase_free : free cfWVbase.
proof: Proof. apply/freeP=> s /= s_alpha_0 ij; case def_ij: (enum_val ij) => [i j]. have /andP[nzi nzj]: (i != 0) && (j != 0). by rewrite -!in_setC1 -in_setX -def_ij enum_valP. have:= congr1 (cfdotr (w_ i j)) s_alpha_0; rewrite raddf_sum raddf0 => <-. rewrite (bigD1 ij) //= nth_image def_ij cfdotZl cfdot_alpha_w // !eqxx mulr1. rewrite big1 ?addr0 // => ij1; rewrite nth_image -(inj_eq enum_val_inj) def_ij. case: (enum_val ij1) => i1 j1 /= => ne_ij1_ij. by rewrite cfdotZl cfdot_alpha_w // mulr_natr mulrb ifN. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice fintype) mathcomp(tuple finfun bigop order prime ssralg matrix poly finset) mathcomp(fingroup morphism perm automorphism quotient action finalg zmodp) mathcomp(gfunctor center gproduct cyclic pgroup abelian frobenius) mathcomp(mxalgebra mxrepresentation vector falgebra fieldext galois) mathcomp(ssrnum rat algC algnum classfun character) mathcomp(integral_char inertia vcharacter) odd_order(PFsection1 PFsection2)