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/gseries.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/gseries.v')
| -rw-r--r-- | mathcomp/solvable/gseries.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/solvable/gseries.v b/mathcomp/solvable/gseries.v index a96295f..73188a6 100644 --- a/mathcomp/solvable/gseries.v +++ b/mathcomp/solvable/gseries.v @@ -132,7 +132,7 @@ have:= sKG; rewrite subEproper => /predU1P[<-|prKG]; first exact: IHm. pose L := [group of f G]. have sHK: H \subset K by case/IHm: Hsn. have sLK: L \subset K by rewrite gen_subG class_support_sub_norm. -rewrite -(subnK (proper_card (sub_proper_trans sLK prKG))) iter_add iterSr. +rewrite -(subnK (proper_card (sub_proper_trans sLK prKG))) iterD iterSr. have defH: H = setIgr L H by rewrite -sub_setIgr ?sub_gen ?sub_class_support. have: normal.-series H (map (setIgr L) s) by rewrite defH path_setIgr. case/IHm=> [|_]; first by rewrite size_map. |