diff options
| author | Kazuhiko Sakaguchi | 2019-11-29 01:19:33 +0900 |
|---|---|---|
| committer | Kazuhiko Sakaguchi | 2019-12-28 17:45:40 +0900 |
| commit | a06d61a8e226eeabc52f1a22e469dca1e6077065 (patch) | |
| tree | 7a78b4f2f84f360127eecc1883630891d58a8a92 /mathcomp/solvable/sylow.v | |
| parent | 52f106adee9009924765adc1a94de9dc4f23f56d (diff) | |
Refactoring and linting especially polydiv
- Replace `altP eqP` and `altP (_ =P _)` with `eqVneq`:
The improved `eqVneq` lemma (#351) is redesigned as a comparison predicate and
introduces a hypothesis in the form of `x != y` in the second case. Thus,
`case: (altP eqP)`, `case: (altP (x =P _))` and `case: (altP (x =P y))` idioms
can be replaced with `case: eqVneq`, `case: (eqVneq x)` and
`case: (eqVneq x y)` respectively. This replacement slightly simplifies and
reduces proof scripts.
- use `have [] :=` rather than `case` if it is better.
- `by apply:` -> `exact:`.
- `apply/lem1; apply/lem2` or `apply: lem1; apply: lem2` -> `apply/lem1/lem2`.
- `move/lem1; move/lem2` -> `move/lem1/lem2`.
- Remove `GRing.` prefix if applicable.
- `negbTE` -> `negPf`, `eq_refl` -> `eqxx` and `sym_equal` -> `esym`.
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 f3ecae2..aed6351 100644 --- a/mathcomp/solvable/sylow.v +++ b/mathcomp/solvable/sylow.v @@ -255,7 +255,7 @@ Qed. Lemma p2group_abelian P : p.-group P -> logn p #|P| <= 2 -> abelian P. Proof. move=> pP lePp2; pose Z := 'Z(P); have sZP: Z \subset P := center_sub P. -case: (eqVneq Z 1); first by move/(trivg_center_pgroup pP)->; apply: abelian1. +have [/(trivg_center_pgroup pP) ->|] := eqVneq Z 1; first exact: abelian1. case/(pgroup_pdiv (pgroupS sZP pP)) => p_pr _ [k oZ]. apply: cyclic_center_factor_abelian. have [->|] := eqVneq (P / Z) 1; first exact: cyclic1. |