proposition: Lemma Frobenius_rfix_compl F gT (G K R : {group gT}) n (rG : mx_representation F G n) : [Frobenius G = K ><| R] -> [char F]^'.-group K -> ~~ (K \subset rker rG) -> rfix_mx rG R != 0.
proof: Proof. rewrite /pgroup charf'_nat => frobG nzK. have [defG _ _ ltKG ltRG]:= Frobenius_context frobG. have{ltKG ltRG} [sKG sRG]: K \subset G /\ R \subset G by rewrite !proper_sub. apply: contraNneq => fixR0; rewrite rfix_mx_rstabC // -(eqmx_scale _ nzK). pose gsum H := gring_op rG (gset_mx F G H). have fixsum (H : {group gT}): H \subset G -> (gsum H <= rfix_mx rG H)%MS. move/subsetP=> sHG; apply/rfix_mxP=> x Hx; have Gx := sHG x Hx. rewrite -gring_opG // -gring_opM ?envelop_mx_id //; congr (gring_op _ _). rewrite {2}/gset_mx (reindex_acts 'R _ Hx) ?astabsR //= mulmx_suml. by apply: eq_bigr=> y; move/sHG=> Gy; rewrite repr_mxM. have: gsum G + rG 1 *+ #|K| = gsum K + \sum_(x in K) gsum (R :^ x). rewrite -gring_opG // -sumr_const -!linear_sum -!linearD; congr gring_op. rewrite {1}/gset_mx (set_partition_big _ (Frobenius_partition frobG)) /=. rewrite big_setU1 -?addrA /=; last first. by apply: contraL (group1 K) => /imsetP[x _ ->]; rewrite conjD1g !inE eqxx. congr (_ + _); rewrite big_imset /= => [|x y Kx Ky /= eqRxy]; last first. have [/eqP/sdprodP[_ _ _ tiKR] _ _ _ /eqP snRG] := and5P frobG. apply/eqP; rewrite eq_mulgV1 -in_set1 -set1gE -tiKR -snRG setIA. by rewrite (setIidPl sKG) !inE conjsgM eqRxy actK groupM /= ?groupV. rewrite -big_split; apply: eq_bigr => x Kx /=. by rewrite addrC conjD1g -big_setD1 ?group1. have ->: gsum G = 0. apply/eqP; rewrite -submx0 -fixR0; apply: submx_trans (rfix_mxS rG sRG). exact: fixsum. rewrite repr_mx1 -scaler_nat add0r => ->. rewrite big1 ?addr0 ?fixsum // => x Kx; have Gx := subsetP sKG x Kx. apply/eqP; rewrite -submx0 (submx_trans (fixsum _ _)) ?conj_subG //. by rewrite -(mul0mx _ (rG x)) -fixR0 rfix_mx_conjsg. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div) mathcomp(fintype tuple bigop prime binomial finset ssralg fingroup finalg) mathcomp(morphism perm automorphism quotient action commutator gproduct) mathcomp(zmodp cyclic gfunctor center pgroup gseries nilpotent sylow) mathcomp(finmodule abelian frobenius maximal extremal hall) mathcomp(matrix mxalgebra mxrepresentation mxabelem) odd_order(wielandt_fixpoint BGsection1 BGsection2)