diff options
Diffstat (limited to 'mathcomp/solvable/sylow.v')
| -rw-r--r-- | mathcomp/solvable/sylow.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/solvable/sylow.v b/mathcomp/solvable/sylow.v index aed6351..fcbe7e8 100644 --- a/mathcomp/solvable/sylow.v +++ b/mathcomp/solvable/sylow.v @@ -267,7 +267,7 @@ Qed. Lemma card_p2group_abelian P : prime p -> #|P| = (p ^ 2)%N -> abelian P. Proof. -move=> primep oP; have pP: p.-group P by rewrite /pgroup oP pnat_exp pnat_id. +move=> primep oP; have pP: p.-group P by rewrite /pgroup oP pnatX pnat_id. by rewrite (p2group_abelian pP) // oP pfactorK. Qed. |