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/extraspecial.v | |
| parent | 835467324db450c8fb8971e477cc4d82fa3e861b (diff) | |
running semi-automated linting on the whole library
Diffstat (limited to 'mathcomp/solvable/extraspecial.v')
| -rw-r--r-- | mathcomp/solvable/extraspecial.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mathcomp/solvable/extraspecial.v b/mathcomp/solvable/extraspecial.v index 9d158cc..2c7f6c3 100644 --- a/mathcomp/solvable/extraspecial.v +++ b/mathcomp/solvable/extraspecial.v @@ -127,7 +127,7 @@ Qed. Lemma Grp_pX1p2 : p^{1+2} \isog Grp (x : y : (x ^+ p, y ^+ p, [~ x, y, x], [~ x, y, y])). Proof. -rewrite [@gtype _]unlock ; apply: intro_isoGrp => [|rT H]. +rewrite [@gtype _]unlock; apply: intro_isoGrp => [|rT H]. apply/existsP; pose x := sdpair1 actp (0, 1)%R; pose y := sdpair2 actp 1%R. exists (x, y); rewrite /= !xpair_eqE; set z := [~ x, y]; set G := _ <*> _. have def_z: z = sdpair1 actp (1, 0)%R. @@ -463,7 +463,7 @@ have ox: #[x] = p. have defCy: 'C_G(Y) = Z * <[x]>. apply/eqP; rewrite eq_sym eqEcard mulG_subG setIS ?centS //=. rewrite cycle_subG inE Gx cYx oCY TI_cardMg ?oZ -?orderE ?ox //=. - by rewrite setIC prime_TIg -?orderE ?ox ?cycle_subG. + by rewrite setIC prime_TIg -?orderE ?ox ?cycle_subG. have abelYt: p.-abelem (Y / Z). by rewrite (abelemS (quotientS _ sYG)) //= -/Z -defPhiG Phi_quotient_abelem. have Yxt: coset Z x \in Y / Z by rewrite mem_quotient. |