proposition: Lemma classg_base_free : row_free classg_base.
proof: Proof. rewrite -kermx_eq0; apply/rowV0P=> v /sub_kermxP; rewrite mulmx_sum_row => v0. apply/rowP=> k /[1!mxE]. have [x Gx def_k] := imsetP (enum_valP k). transitivity (@gring_proj F _ G x (vec_mx 0) 0 0); last first. by rewrite !linear0 !mxE. rewrite -{}v0 !linear_sum (bigD1 k) //= !linearZ /= rowK mxvecK def_k. rewrite linear_sum (bigD1 x) ?class_refl //= gring_projE // eqxx. rewrite !big1 ?addr0 ?mxE ?mulr1 // => [k' | y /andP[xGy ne_yx]]; first 1 last. by rewrite gring_projE ?(groupCl Gx xGy) // eq_sym (negPf ne_yx). rewrite rowK !linearZ /= mxvecK -(inj_eq enum_val_inj) def_k eq_sym. have [z Gz ->] := imsetP (enum_valP k'). move/eqP=> not_Gxz; rewrite linear_sum big1 ?scaler0 //= => y zGy. rewrite gring_projE ?(groupCl Gz zGy) //. by case: eqP zGy => // <- /class_eqP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime) mathcomp(ssralg poly polydiv finset fingroup morphism) mathcomp(perm automorphism quotient finalg action zmodp) mathcomp(commutator cyclic center pgroup matrix mxalgebra) mathcomp(mxpoly)