diff options
| author | Cyril Cohen | 2020-10-30 18:50:56 +0100 |
|---|---|---|
| committer | GitHub | 2020-10-30 18:50:56 +0100 |
| commit | 1ec04efdcd1b00a6ae651551699c8b815a2a063f (patch) | |
| tree | 62f0dc367dc9ab3fa4210ee5e003b03a34eda25f /mathcomp/solvable/maximal.v | |
| parent | fe8759d1faec24cbe9d838f777682e260680d370 (diff) | |
| parent | bd02346e4038871f4d4021dd84df384fc8cf9aa4 (diff) | |
Merge pull request #607 from pi8027/distr-suffixes
Switch from long suffixes to short suffixes
Diffstat (limited to 'mathcomp/solvable/maximal.v')
| -rw-r--r-- | mathcomp/solvable/maximal.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/mathcomp/solvable/maximal.v b/mathcomp/solvable/maximal.v index 3786cff..af0001c 100644 --- a/mathcomp/solvable/maximal.v +++ b/mathcomp/solvable/maximal.v @@ -834,7 +834,7 @@ Lemma card_p3group_extraspecial E : prime p -> #|E| = (p ^ 3)%N -> #|'Z(E)| = p -> extraspecial E. Proof. move=> p_pr oEp3 oZp; have p_gt0 := prime_gt0 p_pr. -have pE: p.-group E by rewrite /pgroup oEp3 pnat_exp pnat_id. +have pE: p.-group E by rewrite /pgroup oEp3 pnatX pnat_id. have pEq: p.-group (E / 'Z(E))%g by rewrite quotient_pgroup. have /andP[sZE nZE] := center_normal E. have oEq: #|E / 'Z(E)|%g = (p ^ 2)%N. @@ -1248,7 +1248,7 @@ have [p2 | odd_p] := even_prime p_pr. suffices <-: restr_perm 'Z(E) @* Aut E = Aut 'Z(E) by apply: Aut_in_isog. apply/eqP; rewrite eqEcard restr_perm_Aut ?center_sub //=. by rewrite card_Aut_cyclic ?prime_cyclic ?oZE // {1}p2 cardG_gt0. -have pE: p.-group E by rewrite /pgroup oE pnat_exp pnat_id. +have pE: p.-group E by rewrite /pgroup oE pnatX pnat_id. have nZE: E \subset 'N('Z(E)) by rewrite normal_norm ?center_normal. have esE: extraspecial E := card_p3group_extraspecial p_pr oE oZE. have [[defPhiE defE'] prZ] := esE. @@ -1303,7 +1303,7 @@ pose f := Morphism fM; have fK: f @* K = K. apply/setP=> u; rewrite morphimEdom. apply/imsetP/idP=> [[v Kv ->] | Ku]; first exact: groupX. exists (u ^+ expg_invn K (val k)); first exact: groupX. - rewrite /f /= expgAC expgK // oK coprime_expl // -unitZpE //. + rewrite /f /= expgAC expgK // oK coprimeXl // -unitZpE //. by case: (k) => /=; rewrite orderE -defZ oZE => j; rewrite natr_Zp. have fMact: {in K & <[x]>, morph_act 'J 'J f (idm <[x]>)}. by move=> u v _ _; rewrite /= conjXg. |