diff options
| author | Cyril Cohen | 2017-11-23 16:33:36 +0100 |
|---|---|---|
| committer | Cyril Cohen | 2018-02-06 13:54:37 +0100 |
| commit | fafd4dac5315e1d4e071b0044a50a16360b31964 (patch) | |
| tree | 5b66c3d67e2b146e3a8013496379b96dd60dc75a /mathcomp/solvable/gseries.v | |
| parent | 835467324db450c8fb8971e477cc4d82fa3e861b (diff) | |
running semi-automated linting on the whole library
Diffstat (limited to 'mathcomp/solvable/gseries.v')
| -rw-r--r-- | mathcomp/solvable/gseries.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mathcomp/solvable/gseries.v b/mathcomp/solvable/gseries.v index 772db33..6dcd833 100644 --- a/mathcomp/solvable/gseries.v +++ b/mathcomp/solvable/gseries.v @@ -420,7 +420,7 @@ Qed. Lemma maxnormal_minnormal G L M : G \subset 'N(M) -> L \subset 'N(G) -> maxnormal M G L -> - minnormal (G / M) (L / M). + minnormal (G / M) (L / M). Proof. move=> nMG nGL /maxgroupP[/andP[/andP[sMG ltMG] nML] maxM]; apply/mingroupP. rewrite -subG1 quotient_sub1 ?ltMG ?quotient_norms //. @@ -544,7 +544,7 @@ Proof. by case/and3P=> /quotient_cents2r *; rewrite subsetI quotientS. Qed. Lemma central_central_factor H K : (K / H) \subset 'Z(G / H) -> H <| K -> H <| G -> central_factor G H K. Proof. -case/subsetIP=> sKGb cGKb /andP[sHK nHK] /andP[sHG nHG]. +case/subsetIP=> sKGb cGKb /andP[sHK nHK] /andP[sHG nHG]. by rewrite /central_factor -quotient_cents2 // cGKb sHK -(quotientSGK nHK). Qed. |