diff options
Diffstat (limited to 'mathcomp/solvable')
| -rw-r--r-- | mathcomp/solvable/abelian.v | 16 | ||||
| -rw-r--r-- | mathcomp/solvable/burnside_app.v | 42 | ||||
| -rw-r--r-- | mathcomp/solvable/extraspecial.v | 2 | ||||
| -rw-r--r-- | mathcomp/solvable/extremal.v | 2 | ||||
| -rw-r--r-- | mathcomp/solvable/jordanholder.v | 20 | ||||
| -rw-r--r-- | mathcomp/solvable/maximal.v | 2 |
6 files changed, 42 insertions, 42 deletions
diff --git a/mathcomp/solvable/abelian.v b/mathcomp/solvable/abelian.v index ad12189..2e025a2 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) => [/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. by apply: leq_trans (logn_le_p_rank EpGx); rewrite -orderE oxp logn_prime ?eqxx. @@ -1713,11 +1713,11 @@ rewrite orderXdiv ?pfactor_dvdn ?leq_subr // -(dvdn_pmul2r m_gt0). by rewrite -expnS -subSn // subSS divnK pfactor_dvdn ?leq_subr. Qed. -Lemma perm_eq_abelian_type p b G : +Lemma abelian_type_pgroup p b G : p.-group G -> \big[dprod/1]_(x <- b) <[x]> = G -> 1 \notin b -> - perm_eq (map order b) (abelian_type G). + perm_eq (abelian_type G) (map order b). Proof. -move: b => b1 pG defG1 ntb1. +rewrite perm_sym; move: b => b1 pG defG1 ntb1. have cGG: abelian G. elim: (b1) {pG}G defG1 => [_ <-|x b IHb G]; first by rewrite big_nil abelian1. rewrite big_cons; case/dprodP=> [[_ H _ defH]] <-; rewrite defH => cxH _. @@ -1992,8 +1992,8 @@ suffices def_atG: abelian_type K ++ abelian_type H =i abelian_type G. by rewrite size_abelian_type // -abelian_type_homocyclic. have [bK defK atK] := abelian_structure cKK. have [bH defH atH] := abelian_structure cHH. -apply: perm_eq_mem; rewrite -atK -atH -map_cat. -apply: (perm_eq_abelian_type pG); first by rewrite big_cat defK defH. +apply/perm_mem; rewrite perm_sym -atK -atH -map_cat. +apply: (abelian_type_pgroup pG); first by rewrite big_cat defK defH. have: all [pred m | m > 1] (map order (bK ++ bH)). by rewrite map_cat all_cat atK atH !abelian_type_gt1. by rewrite all_map (eq_all (@order_gt1 _)) all_predC has_pred1. diff --git a/mathcomp/solvable/burnside_app.v b/mathcomp/solvable/burnside_app.v index b5d34a5..18c6509 100644 --- a/mathcomp/solvable/burnside_app.v +++ b/mathcomp/solvable/burnside_app.v @@ -371,7 +371,7 @@ Lemma F_r3 : 'Fix_to[r3] = Proof. apply/setP=> x; rewrite (sameP afix1P eqP) !inE eqperm_map /=. rewrite /act_f r3_inv !ffunE !permE /=. -by do 3![rewrite eq_sym; case E: {+}(_ == _); rewrite // {E}(eqP E)]. +by do 3![case: eqVneq=> // <-]. Qed. Lemma card_n2 : forall x y z t : square, uniq [:: x; y; z; t] -> @@ -950,7 +950,7 @@ Proof. apply sym_equal. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g r05_inv !ffunE !permE /=. rewrite !eqxx /= !andbT /col1/col2/col3/col4/col5/col0. -by do 3![rewrite eq_sym; case E: {+}(_ == _); rewrite ?andbF // {E}(eqP E) ]. +by do 3![case: eqVneq; rewrite ?andbF // => <-]. Qed. Lemma F_r50 : 'Fix_to_g[r50]= @@ -959,7 +959,7 @@ Lemma F_r50 : 'Fix_to_g[r50]= Proof. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g r50_inv !ffunE !permE /=. apply sym_equal; rewrite !eqxx /= !andbT /col1/col2/col3/col4. -by do 3![rewrite eq_sym; case E: {+}(_ == _); rewrite ?andbF // {E}(eqP E) ]. +by do 3![case: eqVneq; rewrite ?andbF // => <-]. Qed. Lemma F_r23 : 'Fix_to_g[r23] = @@ -969,7 +969,7 @@ Proof. have r23_inv: r23^-1 = r32 by inv_tac. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g r23_inv !ffunE !permE /=. apply sym_equal; rewrite !eqxx /= !andbT /col1/col0/col5/col4. -by do 3![rewrite eq_sym; case E: {+}(_ == _); rewrite ?andbF // {E}(eqP E)]. +by do 3![case: eqVneq; rewrite ?andbF // => <-]. Qed. Lemma F_r32 : 'Fix_to_g[r32] = @@ -979,7 +979,7 @@ Proof. have r32_inv: r32^-1 = r23 by inv_tac. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g r32_inv !ffunE !permE /=. apply sym_equal; rewrite !eqxx /= !andbT /col1/col0/col5/col4. -by do 3![rewrite eq_sym; case E: {+}(_ == _); rewrite ?andbF // {E}(eqP E)]. +by do 3![case: eqVneq; rewrite ?andbF // => <-]. Qed. Lemma F_r14 : 'Fix_to_g[r14] = @@ -987,7 +987,7 @@ Lemma F_r14 : 'Fix_to_g[r14] = Proof. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g r14_inv !ffunE !permE /=. apply sym_equal; rewrite !eqxx /= !andbT /col2/col0/col5/col3. -by do 3![rewrite eq_sym; case E: {+}(_ == _); rewrite ?andbF // {E}(eqP E)]. +by do 3![case: eqVneq; rewrite ?andbF // => <-]. Qed. Lemma F_r41 : 'Fix_to_g[r41] = @@ -995,7 +995,7 @@ Lemma F_r41 : 'Fix_to_g[r41] = Proof. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g r41_inv !ffunE !permE /=. apply sym_equal; rewrite !eqxx /= !andbT /col2/col0/col5/col3. -by do 3![rewrite eq_sym; case E: {+}(_ == _); rewrite ?andbF // {E}(eqP E)]. +by do 3![case: eqVneq; rewrite ?andbF // => <-]. Qed. Lemma F_r024 : 'Fix_to_g[r024] = @@ -1005,7 +1005,7 @@ Proof. have r024_inv: r024^-1 = r042 by inv_tac. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g r024_inv !ffunE !permE /=. apply sym_equal; rewrite ?eqxx /= !andbT /col0/col1/col2/col3/col4/col5. -by do 4![rewrite eq_sym; case E: {+}(_ == _); rewrite ?andbF // ?{E}(eqP E)]. +by do 4![case: eqVneq=> E; rewrite ?andbF // ?{}E]. Qed. Lemma F_r042 : 'Fix_to_g[r042] = @@ -1015,7 +1015,7 @@ Proof. have r042_inv: r042^-1 = r024 by inv_tac. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g r042_inv !ffunE !permE /=. apply sym_equal; rewrite ?eqxx /= !andbT /col0/col1/col2/col3/col4/col5. -by do 4![rewrite eq_sym; case E: {+}(_ == _); rewrite ?andbF // ?{E}(eqP E)]. +by do 4![case: eqVneq=> E; rewrite ?andbF // ?{}E]. Qed. Lemma F_r012 : 'Fix_to_g[r012] = @@ -1025,7 +1025,7 @@ Proof. have r012_inv: r012^-1 = r021 by inv_tac. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g r012_inv !ffunE !permE /=. apply sym_equal; rewrite ?eqxx /= !andbT /col0/col1/col2/col3/col4/col5. -by do 4![rewrite eq_sym; case E: {+}(_ == _); rewrite ?andbF // ?{E}(eqP E)]. +by do 4![case: eqVneq=> E; rewrite ?andbF // ?{}E]. Qed. Lemma F_r021 : 'Fix_to_g[r021] = @@ -1035,7 +1035,7 @@ Proof. have r021_inv: r021^-1 = r012 by inv_tac. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g r021_inv !ffunE !permE /=. apply sym_equal; rewrite ?eqxx /= !andbT /col0/col1/col2/col3/col4/col5. -do 4![rewrite eq_sym; case E: {+}(_ == _); rewrite ?andbF // ?{E}(eqP E)]. +do 4![case: eqVneq=> E; rewrite ?andbF // ?{}E]. Qed. Lemma F_r031 : 'Fix_to_g[r031] = @@ -1045,7 +1045,7 @@ Proof. have r031_inv: r031^-1 = r013 by inv_tac. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g r031_inv !ffunE !permE /=. apply sym_equal; rewrite ?eqxx /= !andbT /col0/col1/col2/col3/col4/col5. -by do 4![rewrite eq_sym; case E: {+}(_ == _); rewrite ?andbF // ?{E}(eqP E)]. +by do 4![case: eqVneq=> E; rewrite ?andbF // ?{}E]. Qed. Lemma F_r013 : 'Fix_to_g[r013] = @@ -1055,7 +1055,7 @@ Proof. have r013_inv: r013^-1 = r031 by inv_tac. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g r013_inv !ffunE !permE /=. apply sym_equal; rewrite ?eqxx /= !andbT /col0/col1/col2/col3/col4/col5. -by do 4![rewrite eq_sym; case E: {+}(_ == _); rewrite ?andbF // ?{E}(eqP E)]. +by do 4![case: eqVneq=> E; rewrite ?andbF // ?{}E]. Qed. Lemma F_r043 : 'Fix_to_g[r043] = @@ -1065,7 +1065,7 @@ Proof. have r043_inv: r043^-1 = r034 by inv_tac. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g r043_inv !ffunE !permE /=. apply sym_equal; rewrite ?eqxx /= !andbT /col0/col1/col2/col3/col4/col5. -by do 4![rewrite eq_sym; case E: {+}(_ == _); rewrite ?andbF // ?{E}(eqP E)]. +by do 4![case: eqVneq=> E; rewrite ?andbF // ?{}E]. Qed. Lemma F_r034 : 'Fix_to_g[r034] = @@ -1075,7 +1075,7 @@ Proof. have r034_inv: r034^-1 = r043 by inv_tac. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g r034_inv !ffunE !permE /=. apply sym_equal; rewrite ?eqxx /= !andbT /col0/col1/col2/col3/col4/col5. -by do 4![rewrite eq_sym; case E: {+}(_ == _); rewrite ?andbF // ?{E}(eqP E)]. +by do 4![case: eqVneq=> E; rewrite ?andbF // ?{}E]. Qed. Lemma F_s1 : 'Fix_to_g[s1] = @@ -1084,7 +1084,7 @@ Proof. have s1_inv: s1^-1 = s1 by inv_tac. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g s1_inv !ffunE !permE /=. apply sym_equal; rewrite ?eqxx /= !andbT /col0/col1/col2/col3/col4/col5. -by do 3![rewrite eq_sym; case E: {+}(_ == _); rewrite ?andbF // ?{E}(eqP E)]. +by do 3![case: eqVneq=> E; rewrite ?andbF // ?{}E]. Qed. Lemma F_s2 : 'Fix_to_g[s2] = @@ -1093,7 +1093,7 @@ Proof. have s2_inv: s2^-1 = s2 by inv_tac. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g s2_inv !ffunE !permE /=. apply sym_equal; rewrite ?eqxx /= !andbT /col0/col1/col2/col3/col4/col5. -by do 3![rewrite eq_sym; case E: {+}(_ == _); rewrite ?andbF // ?{E}(eqP E)]. +by do 3![case: eqVneq=> E; rewrite ?andbF // ?{}E]. Qed. Lemma F_s3 : 'Fix_to_g[s3] = @@ -1102,7 +1102,7 @@ Proof. have s3_inv: s3^-1 = s3 by inv_tac. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g s3_inv !ffunE !permE /=. apply sym_equal; rewrite ?eqxx /= !andbT /col0/col1/col2/col3/col4/col5. -by do 3![rewrite eq_sym; case E: {+}(_ == _); rewrite ?andbF // ?{E}(eqP E)]. +by do 3![case: eqVneq=> E; rewrite ?andbF // ?{}E]. Qed. Lemma F_s4 : 'Fix_to_g[s4] = @@ -1111,7 +1111,7 @@ Proof. have s4_inv: s4^-1 = s4 by inv_tac. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g s4_inv !ffunE !permE /=. apply sym_equal; rewrite ?eqxx /= !andbT /col0/col1/col2/col3/col4/col5. -by do 3![rewrite eq_sym; case E: {+}(_ == _); rewrite ?andbF // ?{E}(eqP E)]. +by do 3![case: eqVneq=> E; rewrite ?andbF // ?{}E]. Qed. Lemma F_s5 : 'Fix_to_g[s5] = @@ -1120,7 +1120,7 @@ Proof. have s5_inv: s5^-1 = s5 by inv_tac. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g s5_inv !ffunE !permE /=. apply sym_equal; rewrite ?eqxx /= !andbT /col0/col1/col2/col3/col4/col5. -by do 3![rewrite eq_sym; case E: {+}(_ == _); rewrite ?andbF // ?{E}(eqP E)]. +by do 3![case: eqVneq=> E; rewrite ?andbF // ?{}E]. Qed. Lemma F_s6 : 'Fix_to_g[s6] = @@ -1129,7 +1129,7 @@ Proof. have s6_inv: s6^-1 = s6 by inv_tac. apply/setP => x; rewrite infE !inE eqperm_map2 /= /act_g s6_inv !ffunE !permE /=. apply sym_equal; rewrite ?eqxx /= !andbT /col0/col1/col2/col3/col4/col5. -by do 3![rewrite eq_sym; case E: {+}(_ == _); rewrite ?andbF // ?{E}(eqP E)]. +by do 3![case: eqVneq=> E; rewrite ?andbF // ?{}E]. Qed. Lemma uniq4_uniq6 : forall x y z t : cube, diff --git a/mathcomp/solvable/extraspecial.v b/mathcomp/solvable/extraspecial.v index aa3ebed..0aacd7c 100644 --- a/mathcomp/solvable/extraspecial.v +++ b/mathcomp/solvable/extraspecial.v @@ -340,7 +340,7 @@ have ntY: Y != 1 by apply: subG1_contra ntZ. have p_odd: odd p by rewrite -oZ (oddSg sZG). have expY: exponent Y %| p by rewrite exponent_Ohm1_class2 // nil_class2 defG'. rewrite (prime_nt_dvdP p_pr _ expY) -?dvdn1 -?trivg_exponent //. -have [-> | neYG] := eqVneq Y G; first by rewrite indexgg dvd1n eqxx; split. +have [-> | neYG] := eqVneq Y G; first by rewrite indexgg dvd1n; split. have sG1Z: 'Mho^1(G) \subset Z by rewrite -defPhiG (Phi_joing pG) joing_subr. have Z_Gp: {in G, forall x, x ^+ p \in Z}. by move=> x Gx; rewrite /= (subsetP sG1Z) ?(Mho_p_elt 1) ?(mem_p_elt pG). diff --git a/mathcomp/solvable/extremal.v b/mathcomp/solvable/extremal.v index 65c186a..d236575 100644 --- a/mathcomp/solvable/extremal.v +++ b/mathcomp/solvable/extremal.v @@ -2322,7 +2322,7 @@ have{defZN2} strZN2: \big[dprod/1]_(z <- [:: xpn3; y]) <[z]> = 'Z('Ohm_2(N)). by rewrite unlock /= dprodg1. rewrite -size_abelian_type ?center_abelian //. have pZN2: p.-group 'Z('Ohm_2(N)) by rewrite (pgroupS _ pN) // subIset ?Ohm_sub. -rewrite -(perm_eq_size (perm_eq_abelian_type pZN2 strZN2 _)) //= !inE. +rewrite (perm_size (abelian_type_pgroup pZN2 strZN2 _)) //= !inE. rewrite !(eq_sym 1) -!order_eq1 oy orderE oX2. by rewrite (eqn_exp2l 2 0) // (eqn_exp2l 1 0). Qed. diff --git a/mathcomp/solvable/jordanholder.v b/mathcomp/solvable/jordanholder.v index 1a32bce..d191e20 100644 --- a/mathcomp/solvable/jordanholder.v +++ b/mathcomp/solvable/jordanholder.v @@ -179,9 +179,9 @@ elim: {G}#|G| {-2}G (leqnn #|G|) => [|n Hi] G cG in s1 s2 * => cs1 cs2. have [G1 | ntG] := boolP (G :==: 1). have -> : s1 = [::] by apply/eqP; rewrite -(trivg_comps cs1). have -> : s2 = [::] by apply/eqP; rewrite -(trivg_comps cs2). - by rewrite /= perm_eq_refl. + by rewrite /= perm_refl. have [sG | nsG] := boolP (simple G). - by rewrite (simple_compsP cs1 sG) (simple_compsP cs2 sG) perm_eq_refl. + by rewrite (simple_compsP cs1 sG) (simple_compsP cs2 sG) perm_refl. case es1: s1 cs1 => [|N1 st1] cs1. by move: (trivg_comps cs1); rewrite eqxx; move/negP:ntG. case es2: s2 cs2 => [|N2 st2] cs2 {s1 es1}. @@ -228,9 +228,9 @@ have i3 : perm_eq fG1 fG2. rewrite (@perm_catCA _ [::_] [::_]) /mksrepr. rewrite (@section_repr_isog _ (mkSec _ _) (mkSec _ _) iso1). rewrite -(@section_repr_isog _ (mkSec _ _) (mkSec _ _) iso2). - exact: perm_eq_refl. -apply: (perm_eq_trans i1); apply: (perm_eq_trans i3); rewrite perm_eq_sym. -by apply: perm_eq_trans i2; apply: perm_eq_refl. + exact: perm_refl. +apply: (perm_trans i1); apply: (perm_trans i3); rewrite perm_sym. +by apply: perm_trans i2; apply: perm_refl. Qed. End CompositionSeries. @@ -593,11 +593,11 @@ elim: {G} #|G| {-2}G (leqnn #|G|) => [|n Hi] G cG in s1 s2 * => hsD cs1 cs2. case/orP: (orbN (G :==: 1)) => [tG | ntG]. have -> : s1 = [::] by apply/eqP; rewrite -(trivg_acomps cs1). have -> : s2 = [::] by apply/eqP; rewrite -(trivg_acomps cs2). - by rewrite /= perm_eq_refl. + by rewrite /= perm_refl. case/orP: (orbN (asimple to G))=> [sG | nsG]. have -> : s1 = [:: 1%G ] by apply/(asimple_acompsP cs1). have -> : s2 = [:: 1%G ] by apply/(asimple_acompsP cs2). - by rewrite /= perm_eq_refl. + by rewrite /= perm_refl. case es1: s1 cs1 => [|N1 st1] cs1. by move: (trivg_comps cs1); rewrite eqxx; move/negP:ntG. case es2: s2 cs2 => [|N2 st2] cs2 {s1 es1}. @@ -667,9 +667,9 @@ have i3 : perm_eq fG1 fG2. rewrite (@perm_catCA _ [::_] [::_]) /mksrepr. rewrite (@section_repr_isog _ (mkSec _ _) (mkSec _ _) iso1). rewrite -(@section_repr_isog _ (mkSec _ _) (mkSec _ _) iso2). - exact: perm_eq_refl. -apply: (perm_eq_trans i1); apply: (perm_eq_trans i3); rewrite perm_eq_sym. -by apply: perm_eq_trans i2; apply: perm_eq_refl. + exact: perm_refl. +apply: (perm_trans i1); apply: (perm_trans i3); rewrite perm_sym. +by apply: perm_trans i2; apply: perm_refl. Qed. End StrongJordanHolder. diff --git a/mathcomp/solvable/maximal.v b/mathcomp/solvable/maximal.v index f3d79fc..0dfb4d1 100644 --- a/mathcomp/solvable/maximal.v +++ b/mathcomp/solvable/maximal.v @@ -1642,4 +1642,4 @@ Qed. End SCN. -Arguments SCN_P {gT G A}.
\ No newline at end of file +Arguments SCN_P {gT G A}. |