diff options
Diffstat (limited to 'mathcomp/solvable')
| -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 95bc562..3a5caeb 100644 --- a/mathcomp/solvable/abelian.v +++ b/mathcomp/solvable/abelian.v @@ -264,7 +264,7 @@ Qed. Lemma exponent_witness G : nilpotent G -> {x | x \in G & exponent G = #[x]}. Proof. -move=> nilG; have [//=| /= x Gx max_x] := @arg_maxP _ 1 (mem G) order. +move=> nilG; have [//=| /= x Gx max_x] := @arg_maxnP _ 1 (mem G) order. exists x => //; apply/eqP; rewrite eqn_dvd dvdn_exponent // andbT. apply/dvdn_biglcmP=> y Gy; apply/dvdn_partP=> //= p. rewrite mem_primes => /andP[p_pr _]; have p_gt1: p > 1 := prime_gt1 p_pr. @@ -726,12 +726,12 @@ Qed. Lemma grank_min B : 'm(<<B>>) <= #|B|. Proof. -by rewrite /gen_rank; case: arg_minP => [|_ _ -> //]; rewrite genGid. +by rewrite /gen_rank; case: arg_minnP => [|_ _ -> //]; rewrite genGid. Qed. Lemma grank_witness G : {B | <<B>> = G & #|B| = 'm(G)}. Proof. -rewrite /gen_rank; case: arg_minP => [|B defG _]; first by rewrite genGid. +rewrite /gen_rank; case: arg_minnP => [|B defG _]; first by rewrite genGid. by exists B; first apply/eqP. Qed. |