diff options
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/odd_order/BGsection15.v | 4 | ||||
| -rw-r--r-- | mathcomp/odd_order/BGsection16.v | 2 |
2 files changed, 2 insertions, 4 deletions
diff --git a/mathcomp/odd_order/BGsection15.v b/mathcomp/odd_order/BGsection15.v index 971a2c8..553feda 100644 --- a/mathcomp/odd_order/BGsection15.v +++ b/mathcomp/odd_order/BGsection15.v @@ -1248,7 +1248,7 @@ Lemma nonTI_Fitting_facts M : [/\ M \in 'M_'F :|: 'M_'P1, M`_\F = M`_\sigma & M^`(1) \subset 'F(M)]. Proof. move=> maxM nonTI; suff: [exists (y | y \notin M), 'F(M) :&: 'F(M) :^ y != 1]. - by case/exists_inP=> y notMy /nonTI_Fitting_structure[] // [[-> ?] _ []]. + by case/exists_inP=> y notMy /nonTI_Fitting_structure[] // [-> dMF] _ []. rewrite -negb_forall_in; apply: contra nonTI => /forall_inP tiF. apply/normedTI_P; rewrite normD1 setTI gFnorm setD_eq0 subG1. split=> // [|g _]; first by rewrite (trivg_Fitting (mmax_sol maxM)) mmax_neq1. @@ -1509,5 +1509,3 @@ by rewrite (subG1_contra _ ntCMsx) ?setIS //= -cent_cycle centS. Qed. End Section15. - - diff --git a/mathcomp/odd_order/BGsection16.v b/mathcomp/odd_order/BGsection16.v index 3f0cf92..32850e4 100644 --- a/mathcomp/odd_order/BGsection16.v +++ b/mathcomp/odd_order/BGsection16.v @@ -786,7 +786,7 @@ split; first by have [_ _ _ _ []] := Ptype_structure PmaxM hallK. have [<- | neqMF_Ms] := eqVneq M`_\F M`_\sigma; first exact: Fcore_sub_Fitting. have solMs: solvable M`_\sigma := solvableS (pcore_sub _ _) (mmax_sol maxM). have [D hallD] := Hall_exists #|Kstar|^' solMs. -by case: (Fcore_structure maxM) notP1maxM => _ /(_ K D)[] // [[->]]. +by case: (Fcore_structure maxM) notP1maxM => _ /(_ K D)[] // [->]. Qed. End SingleGroupSummaries. |