proposition: Theorem charf'_GL2_abelian F gT (G : {group gT}) (rG : mx_representation F G 2) : odd #|G| -> mx_faithful rG -> [char F]^'.-group G -> abelian G.
proof: Proof. move=> oddG ffG char'G; apply/commG1P/eqP. rewrite trivg_card1 (pnat_1 _ (pgroupS _ char'G)) ?comm_subG //=. exact: der1_odd_GL2_charf ffG. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div fintype) mathcomp(bigop prime binomial finset fingroup morphism perm automorphism) mathcomp(quotient action gfunctor commutator gproduct) mathcomp(ssralg finalg zmodp cyclic center pgroup gseries nilpotent) mathcomp(sylow abelian maximal hall) mathcomp(matrix mxalgebra mxrepresentation mxabelem) odd_order(BGsection1)