diff options
Diffstat (limited to 'mathcomp/solvable/abelian.v')
| -rw-r--r-- | mathcomp/solvable/abelian.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/mathcomp/solvable/abelian.v b/mathcomp/solvable/abelian.v index a51cbf2..dd14013 100644 --- a/mathcomp/solvable/abelian.v +++ b/mathcomp/solvable/abelian.v @@ -836,9 +836,9 @@ Qed. Lemma rank_gt0 G : ('r(G) > 0) = (G :!=: 1). Proof. -case: (eqsVneq G 1) => [-> |]; first by rewrite rank1 eqxx. -case: (trivgVpdiv G) => [-> | [p p_pr]]; first by case/eqP. -case/Cauchy=> // x Gx oxp ->; apply: leq_trans (p_rank_le_rank p G). +case: (eqsVneq G 1) => [-> |]; first by rewrite rank1. +case: (trivgVpdiv G) => [-> | [p p_pr]]; first by rewrite eqxx. +case/Cauchy=> // x Gx oxp _; apply: leq_trans (p_rank_le_rank p G). have EpGx: <[x]>%G \in 'E_p(G). by rewrite inE cycle_subG Gx abelemE // cycle_abelian -oxp exponent_dvdn. by apply: leq_trans (logn_le_p_rank EpGx); rewrite -orderE oxp logn_prime ?eqxx. |