diff options
Diffstat (limited to 'mathcomp/solvable')
| -rw-r--r-- | mathcomp/solvable/abelian.v | 19 | ||||
| -rw-r--r-- | mathcomp/solvable/alt.v | 11 | ||||
| -rw-r--r-- | mathcomp/solvable/cyclic.v | 4 | ||||
| -rw-r--r-- | mathcomp/solvable/frobenius.v | 2 | ||||
| -rw-r--r-- | mathcomp/solvable/sylow.v | 2 |
5 files changed, 18 insertions, 20 deletions
diff --git a/mathcomp/solvable/abelian.v b/mathcomp/solvable/abelian.v index bfdafae..5f93277 100644 --- a/mathcomp/solvable/abelian.v +++ b/mathcomp/solvable/abelian.v @@ -182,8 +182,8 @@ Qed. Lemma Mho_p_elt (p : nat) x : x \in A -> p.-elt x -> x ^+ (p ^ n) \in Mho. Proof. -move=> Ax p_x; case: (eqVneq x 1) => [-> | ntx]; first by rewrite groupX. -by apply: mem_gen; apply/imsetP; exists x; rewrite ?inE ?Ax (pdiv_p_elt p_x). +move=> Ax p_x; have [-> | ntx] := eqVneq x 1; first by rewrite groupX. +by apply/mem_gen/imsetP; exists x; rewrite ?inE ?Ax (pdiv_p_elt p_x). Qed. End Functors. @@ -572,7 +572,7 @@ Lemma TIp1ElemP p A X Y : Proof. move=> EpX EpY; have p_pr := pnElem_prime EpX. have [oX oY] := (card_p1Elem EpX, card_p1Elem EpY). -have [<- |] := altP eqP. +have [<-|] := eqVneq. by right=> X1; rewrite -oX -(setIid X) X1 cards1 in p_pr. by rewrite eqEcard oX oY leqnn andbT; left; rewrite prime_TIg ?oX. Qed. @@ -668,7 +668,7 @@ Proof. apply/setP=> E; rewrite inE in_setI; apply: andb_id2l => /pElemP[sEG abelE]. apply/idP/nElemP=> [|[q]]; first by exists p; rewrite !inE sEG abelE. rewrite !inE -2!andbA => /and4P[_ /pgroupP qE _]. -case: (eqVneq E 1%G) => [-> | ]; first by rewrite cards1 !logn1. +have [->|] := eqVneq E 1%G; first by rewrite cards1 !logn1. case/(pgroup_pdiv (abelem_pgroup abelE)) => p_pr pE _. by rewrite (eqnP (qE p p_pr pE)). Qed. @@ -1166,7 +1166,7 @@ Qed. Lemma OhmE p G : p.-group G -> 'Ohm_n(G) = <<'Ldiv_(p ^ n)(G)>>. Proof. move=> pG; congr <<_>>; apply/setP=> x; rewrite !inE; apply: andb_id2l => Gx. -case: (eqVneq x 1) => [-> | ntx]; first by rewrite !expg1n. +have [-> | ntx] := eqVneq x 1; first by rewrite !expg1n. by rewrite (pdiv_p_elt (mem_p_elt pG Gx)). Qed. @@ -1468,9 +1468,8 @@ Lemma cyclic_pgroup_dprod_trivg p A B C : Proof. move=> pC cycC; case/cyclicP: cycC pC => x ->{C} pC defC. case/dprodP: defC => [] [G H -> ->{A B}] defC _ tiGH; rewrite -defC. -case: (eqVneq <[x]> 1) => [|ntC]. - move/trivgP; rewrite -defC mulG_subG => /andP[/trivgP-> _]. - by rewrite mul1g; left. +have [/trivgP | ntC] := eqVneq <[x]> 1. + by rewrite -defC mulG_subG => /andP[/trivgP-> _]; rewrite mul1g; left. have [pr_p _ _] := pgroup_pdiv pC ntC; pose K := 'Ohm_1(<[x]>). have prK : prime #|K| by rewrite (Ohm1_cyclic_pgroup_prime _ pC) ?cycle_cyclic. case: (prime_subgroupVti G prK) => [sKG |]; last first. @@ -1842,7 +1841,7 @@ Qed. Lemma rank_cycle (x : gT) : 'r(<[x]>) = (x != 1). Proof. -have [->|ntx] := altP (x =P 1); first by rewrite cycle1 rank1. +have [->|ntx] := eqVneq x 1; first by rewrite cycle1 rank1. apply/eqP; rewrite eqn_leq rank_gt0 cycle_eq1 ntx andbT. by rewrite -grank_abelian ?cycle_abelian //= -(cards1 x) grank_min. Qed. @@ -1948,7 +1947,7 @@ Qed. Lemma abelian_type_abelem p G : p.-abelem G -> abelian_type G = nseq 'r(G) p. Proof. move=> abelG; rewrite (abelian_type_homocyclic (abelem_homocyclic abelG)). -case: (eqVneq G 1%G) => [-> | ntG]; first by rewrite rank1. +have [-> | ntG] := eqVneq G 1%G; first by rewrite rank1. congr nseq; apply/eqP; rewrite eqn_dvd; have [pG _ ->] := and3P abelG. have [p_pr] := pgroup_pdiv pG ntG; case/Cauchy=> // x Gx <- _. exact: dvdn_exponent. diff --git a/mathcomp/solvable/alt.v b/mathcomp/solvable/alt.v index cb86051..e67a0f9 100644 --- a/mathcomp/solvable/alt.v +++ b/mathcomp/solvable/alt.v @@ -258,9 +258,9 @@ case Hcard1: (#|H| == 1%N); move/eqP: Hcard1 => Hcard1. by left; apply: card1_trivg; rewrite Hcard1. right; case Hcard60: (#|H| == 60%N); move/eqP: Hcard60 => Hcard60. by apply/eqP; rewrite eqEcard Hcard60 F1 andbT; case/andP: Hnorm. -have Hcard20: #|H| = 20; last clear Hcard1 Hcard60. +have {Hcard1 Hcard60} Hcard20: #|H| = 20. have Hdiv: 20 %| #|H| by apply: FF => // HH; case Hcard1; rewrite HH cards1. - case H20: (#|H| == 20); first by apply/eqP. + case H20: (#|H| == 20); first exact/eqP. case: Hcard60; case/andP: Hnorm; move/cardSg; rewrite F1 => Hdiv1 _. by case/dvdnP: Hdiv H20 Hdiv1 => n ->; move: n; do 4!case=> //. have prime_5: prime 5 by []. @@ -272,7 +272,7 @@ have nSyl5: #|'Syl_5(H)| = 1%N. case: (Sylow_exists 5 H) => S; case/pHallP=> sSH oS. have{oS} oS: #|S| = 5 by rewrite oS p_part Hcard20. suff: 20 %| #|S| by rewrite oS. -apply FF => [|S1]; last by rewrite S1 cards1 in oS. +apply: FF => [|S1]; last by rewrite S1 cards1 in oS. apply: char_normal_trans Hnorm; apply: lone_subgroup_char => // Q sQH isoQS. rewrite subEproper; apply/norP=> [[nQS _]]; move: nSyl5. rewrite (cardsD1 S) (cardsD1 Q) 4!{1}inE nQS !pHallE sQH sSH Hcard20 p_part. @@ -362,8 +362,7 @@ Proof. have rgd_x p: rgd p x = x by rewrite permE /= insubF //= eqxx. have rfd_rgd p: rfd (rgd p) = p. apply/permP => [[z Hz]]; apply/val_eqP; rewrite !permE. - rewrite /= [rgd _ _]permE /= insubF eq_refl // permE /=. - by rewrite (@insubT _ (xpredC1 x) _ _ Hz). + by rewrite /= [rgd _ _]permE /= insubF eqxx // permE /= insubT. have sSd: 'C_('Alt_T)[x | 'P] \subset 'dom rfd. by apply/subsetP=> p; rewrite !inE /=; case/andP. apply/isogP; exists [morphism of restrm sSd rfd] => /=; last first. @@ -449,7 +448,7 @@ have Hreg g z: g \in H -> g z = z -> g = 1. by rewrite memJ_norm ?(subsetP nH). clear K F8 F12 F13 Ksub F14. have Hcard: 5 < #|H|. - apply: (leq_trans oT); apply dvdn_leq; first by apply: cardG_gt0. + apply: (leq_trans oT); apply: dvdn_leq; first exact: cardG_gt0. by rewrite -cardsT (atrans_dvd F5). case Eh: (pred0b [predD1 H & 1]). by move: Hcard; rewrite /pred0b in Eh; rewrite (cardD1 1) group1 (eqP Eh). diff --git a/mathcomp/solvable/cyclic.v b/mathcomp/solvable/cyclic.v index e6d3afb..d82009b 100644 --- a/mathcomp/solvable/cyclic.v +++ b/mathcomp/solvable/cyclic.v @@ -587,7 +587,7 @@ Variable u : {unit 'Z_#[a]}. Lemma injm_cyclem : 'injm (cyclem (val u) a). Proof. apply/subsetP=> x /setIdP[ax]; rewrite !inE -order_dvdn. -case: (eqVneq a 1) => [a1 | nta]; first by rewrite a1 cycle1 inE in ax. +have [a1 | nta] := eqVneq a 1; first by rewrite a1 cycle1 inE in ax. rewrite -order_eq1 -dvdn1; move/eqnP: (valP u) => /= <-. by rewrite dvdn_gcd {2}Zp_cast ?order_gt1 // order_dvdG. Qed. @@ -616,7 +616,7 @@ Canonical Zp_unit_morphism := Morphism Zp_unitmM. Lemma injm_Zp_unitm : 'injm Zp_unitm. Proof. -case: (eqVneq a 1) => [a1 | nta]. +have [a1 | nta] := eqVneq a 1. by rewrite subIset //= card_le1_trivg ?subxx // card_units_Zp a1 order1. apply/subsetP=> /= u /morphpreP[_ /set1P/= um1]. have{um1}: Zp_unitm u a == Zp_unitm 1 a by rewrite um1 morph1. diff --git a/mathcomp/solvable/frobenius.v b/mathcomp/solvable/frobenius.v index 71b8b34..c1c1d27 100644 --- a/mathcomp/solvable/frobenius.v +++ b/mathcomp/solvable/frobenius.v @@ -598,7 +598,7 @@ have partG: partition (gval K |: (H^# :^: K)) G. apply: Frobenius_partition; apply/andP; rewrite defG; split=> //. by apply/Frobenius_actionP; apply: HasFrobeniusAction FrobG. have{FrobG} [ffulG transG regG ntH [u Su defH]]:= FrobG. -apply/setP=> x; rewrite !inE; have [-> | ntx] := altP eqP; first exact: group1. +apply/setP=> x; rewrite !inE; have [-> | ntx] := eqVneq; first exact: group1. rewrite /= -(cover_partition partG) /cover. have neKHy y: gval K <> H^# :^ y. by move/setP/(_ 1); rewrite group1 conjD1g setD11. 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. |