diff options
| author | Anton Trunov | 2019-05-29 15:37:31 +0300 |
|---|---|---|
| committer | Anton Trunov | 2019-05-29 15:37:31 +0300 |
| commit | e9c284b97b76e214f417ccc33907853bc0b8aa8e (patch) | |
| tree | b7a8df4adad80129e1f1ffab4308dba17816744d /mathcomp/solvable/abelian.v | |
| parent | 42db44ce8df9f24d90c321d57e81e2d5bf83bd48 (diff) | |
incorporate new suggestions by @CohenCyril
Diffstat (limited to 'mathcomp/solvable/abelian.v')
| -rw-r--r-- | mathcomp/solvable/abelian.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/solvable/abelian.v b/mathcomp/solvable/abelian.v index dd14013..2e025a2 100644 --- a/mathcomp/solvable/abelian.v +++ b/mathcomp/solvable/abelian.v @@ -837,7 +837,7 @@ Qed. Lemma rank_gt0 G : ('r(G) > 0) = (G :!=: 1). Proof. case: (eqsVneq G 1) => [-> |]; first by rewrite rank1. -case: (trivgVpdiv G) => [-> | [p p_pr]]; first by rewrite eqxx. +case: (trivgVpdiv G) => [/eqP->// | [p p_pr]]. 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. |