diff options
| -rw-r--r-- | mathcomp/solvable/abelian.v | 34 | ||||
| -rw-r--r-- | mathcomp/solvable/burnside_app.v | 2 | ||||
| -rw-r--r-- | mathcomp/solvable/center.v | 2 | ||||
| -rw-r--r-- | mathcomp/solvable/commutator.v | 2 | ||||
| -rw-r--r-- | mathcomp/solvable/cyclic.v | 4 | ||||
| -rw-r--r-- | mathcomp/solvable/frobenius.v | 8 | ||||
| -rw-r--r-- | mathcomp/solvable/gseries.v | 2 | ||||
| -rw-r--r-- | mathcomp/solvable/maximal.v | 2 | ||||
| -rw-r--r-- | mathcomp/solvable/pgroup.v | 10 | ||||
| -rw-r--r-- | mathcomp/solvable/primitive_action.v | 2 |
10 files changed, 34 insertions, 34 deletions
diff --git a/mathcomp/solvable/abelian.v b/mathcomp/solvable/abelian.v index 2b0ab00..f3ff7c3 100644 --- a/mathcomp/solvable/abelian.v +++ b/mathcomp/solvable/abelian.v @@ -196,7 +196,7 @@ Arguments Scope Ohm [nat_scope _ group_scope]. Arguments Scope Ohm_group [nat_scope _ group_scope]. Arguments Scope Mho [nat_scope _ group_scope]. Arguments Scope Mho_group [nat_scope _ group_scope]. -Implicit Arguments OhmPredP [n gT x]. +Arguments OhmPredP [n gT x]. Notation "''Ohm_' n ( G )" := (Ohm n G) (at level 8, n at level 2, format "''Ohm_' n ( G )") : group_scope. @@ -233,7 +233,7 @@ apply: (iffP (dvdn_biglcmP _ _ _)) => eAn x Ax. by apply/eqP; rewrite -order_dvdn eAn. by rewrite order_dvdn eAn. Qed. -Implicit Arguments exponentP [A n]. +Arguments exponentP [A n]. Lemma trivg_exponent G : (G :==: 1) = (exponent G %| 1). Proof. @@ -495,7 +495,7 @@ Qed. Lemma pElemP p A E : reflect (E \subset A /\ p.-abelem E) (E \in 'E_p(A)). Proof. by rewrite inE; apply: andP. Qed. -Implicit Arguments pElemP [p A E]. +Arguments pElemP [p A E]. Lemma pElemS p A B : A \subset B -> 'E_p(A) \subset 'E_p(B). Proof. @@ -511,7 +511,7 @@ Proof. by rewrite !inE conjSg abelemJ. Qed. Lemma pnElemP p n A E : reflect [/\ E \subset A, p.-abelem E & logn p #|E| = n] (E \in 'E_p^n(A)). Proof. by rewrite !inE -andbA; apply: (iffP and3P) => [] [-> -> /eqP]. Qed. -Implicit Arguments pnElemP [p n A E]. +Arguments pnElemP [p n A E]. Lemma pnElemPcard p n A E : E \in 'E_p^n(A) -> [/\ E \subset A, p.-abelem E & #|E| = p ^ n]%N. @@ -636,7 +636,7 @@ have:= EpnE; rewrite pnElemE ?(pnElem_prime EpnE) // !inE -andbA ltnS. case/and3P=> sEG _ oE; rewrite dvdn_leq // (dvdn_trans _ (cardSg sEG)) //. by rewrite (eqP oE) dvdn_exp. Qed. -Implicit Arguments nElemP [n G E]. +Arguments nElemP [n G E]. Lemma nElem0 G : 'E^0(G) = [set 1%G]. Proof. @@ -899,18 +899,18 @@ Qed. End ExponentAbelem. -Implicit Arguments LdivP [gT A n x]. -Implicit Arguments exponentP [gT A n]. -Implicit Arguments abelemP [gT p G]. -Implicit Arguments is_abelemP [gT G]. -Implicit Arguments pElemP [gT p A E]. -Implicit Arguments pnElemP [gT p n A E]. -Implicit Arguments nElemP [gT n G E]. -Implicit Arguments nElem1P [gT G E]. -Implicit Arguments pmaxElemP [gT p A E]. -Implicit Arguments pmaxElem_LdivP [gT p G E]. -Implicit Arguments p_rank_geP [gT p n G]. -Implicit Arguments rank_geP [gT n G]. +Arguments LdivP [gT A n x]. +Arguments exponentP [gT A n]. +Arguments abelemP [gT p G]. +Arguments is_abelemP [gT G]. +Arguments pElemP [gT p A E]. +Arguments pnElemP [gT p n A E]. +Arguments nElemP [gT n G E]. +Arguments nElem1P [gT G E]. +Arguments pmaxElemP [gT p A E]. +Arguments pmaxElem_LdivP [gT p G E]. +Arguments p_rank_geP [gT p n G]. +Arguments rank_geP [gT n G]. Section MorphAbelem. diff --git a/mathcomp/solvable/burnside_app.v b/mathcomp/solvable/burnside_app.v index d9010d5..1c804cc 100644 --- a/mathcomp/solvable/burnside_app.v +++ b/mathcomp/solvable/burnside_app.v @@ -26,7 +26,7 @@ rewrite big_uniq // -(card_uniqP Us) (eq_card sG) -Frobenius_Cauchy. by apply/actsP=> ? _ ?; rewrite !inE. Qed. -Implicit Arguments burnside_formula [gT]. +Arguments burnside_formula [gT]. Section colouring. diff --git a/mathcomp/solvable/center.v b/mathcomp/solvable/center.v index 54726be..c461a9e 100644 --- a/mathcomp/solvable/center.v +++ b/mathcomp/solvable/center.v @@ -187,7 +187,7 @@ End Injm. End Center. -Implicit Arguments center_idP [gT A]. +Arguments center_idP [gT A]. Lemma isog_center (aT rT : finGroupType) (G : {group aT}) (H : {group rT}) : G \isog H -> 'Z(G) \isog 'Z(H). diff --git a/mathcomp/solvable/commutator.v b/mathcomp/solvable/commutator.v index 1f9bad0..6a390ce 100644 --- a/mathcomp/solvable/commutator.v +++ b/mathcomp/solvable/commutator.v @@ -352,7 +352,7 @@ Proof. exact: commG1P. Qed. End Commutator_properties. -Implicit Arguments derG1P [gT G]. +Arguments derG1P [gT G]. Lemma der_cont n : GFunctor.continuous (derived_at n). Proof. by move=> aT rT G f; rewrite morphim_der. Qed. diff --git a/mathcomp/solvable/cyclic.v b/mathcomp/solvable/cyclic.v index 9a1e451..7663163 100644 --- a/mathcomp/solvable/cyclic.v +++ b/mathcomp/solvable/cyclic.v @@ -292,7 +292,7 @@ End Cyclic. Arguments Scope cyclic [_ group_scope]. Arguments Scope generator [_ group_scope group_scope]. Arguments Scope expg_invn [_ group_scope nat_scope]. -Implicit Arguments cyclicP [gT A]. +Arguments cyclicP [gT A]. Prenex Implicits cyclic Zpm generator expg_invn. (* Euler's theorem *) @@ -558,7 +558,7 @@ End Metacyclic. Arguments Scope metacyclic [_ group_scope]. Prenex Implicits metacyclic. -Implicit Arguments metacyclicP [gT A]. +Arguments metacyclicP [gT A]. (* Automorphisms of cyclic groups. *) Section CyclicAutomorphism. diff --git a/mathcomp/solvable/frobenius.v b/mathcomp/solvable/frobenius.v index da65950..3416587 100644 --- a/mathcomp/solvable/frobenius.v +++ b/mathcomp/solvable/frobenius.v @@ -246,7 +246,7 @@ have Gg: g \in G by rewrite groupMl ?groupV. rewrite -conjIg (inj_eq (act_inj 'Js x)) (eq_sym A) (sameP eqP normP). by rewrite -cards_eq0 cardJg cards_eq0 setI_eq0 => /tiAG/(subsetP nAL)->. Qed. -Implicit Arguments normedTI_P [A G L]. +Arguments normedTI_P [A G L]. Lemma normedTI_memJ_P A G L : reflect [/\ A != set0, L \subset G @@ -622,9 +622,9 @@ Qed. End FrobeniusBasics. -Implicit Arguments normedTI_P [gT A G L]. -Implicit Arguments normedTI_memJ_P [gT A G L]. -Implicit Arguments Frobenius_kerP [gT G K]. +Arguments normedTI_P [gT A G L]. +Arguments normedTI_memJ_P [gT A G L]. +Arguments Frobenius_kerP [gT G K]. Lemma Frobenius_coprime_quotient (gT : finGroupType) (G K H N : {group gT}) : K ><| H = G -> N <| G -> coprime #|K| #|H| /\ H :!=: 1%g -> diff --git a/mathcomp/solvable/gseries.v b/mathcomp/solvable/gseries.v index 6dcd833..1dc6a35 100644 --- a/mathcomp/solvable/gseries.v +++ b/mathcomp/solvable/gseries.v @@ -212,7 +212,7 @@ Qed. End Subnormal. -Implicit Arguments subnormalP [gT G H]. +Arguments subnormalP [gT H G]. Prenex Implicits subnormalP. Section MorphSubNormal. diff --git a/mathcomp/solvable/maximal.v b/mathcomp/solvable/maximal.v index e5c2d4f..06cf329 100644 --- a/mathcomp/solvable/maximal.v +++ b/mathcomp/solvable/maximal.v @@ -1649,4 +1649,4 @@ Qed. End SCN. -Implicit Arguments SCN_P [gT G A].
\ No newline at end of file +Arguments SCN_P [gT G A].
\ No newline at end of file diff --git a/mathcomp/solvable/pgroup.v b/mathcomp/solvable/pgroup.v index b595530..d383aa7 100644 --- a/mathcomp/solvable/pgroup.v +++ b/mathcomp/solvable/pgroup.v @@ -170,7 +170,7 @@ Proof. exact: partn_eq1 (cardG_gt0 G). Qed. Lemma pgroupP pi G : reflect (forall p, prime p -> p %| #|G| -> p \in pi) (pi.-group G). Proof. exact: pnatP. Qed. -Implicit Arguments pgroupP [pi G]. +Arguments pgroupP [pi G]. Lemma pgroup1 pi : pi.-group [1 gT]. Proof. by rewrite /pgroup cards1. Qed. @@ -679,8 +679,8 @@ Qed. End PgroupProps. -Implicit Arguments pgroupP [gT pi G]. -Implicit Arguments constt1P [gT pi x]. +Arguments pgroupP [gT pi G]. +Arguments constt1P [gT pi x]. Prenex Implicits pgroupP constt1P. Section NormalHall. @@ -1302,8 +1302,8 @@ Qed. End EqPcore. -Implicit Arguments sdprod_Hall_pcoreP [gT pi G H]. -Implicit Arguments sdprod_Hall_p'coreP [gT pi G H]. +Arguments sdprod_Hall_pcoreP [pi gT H G]. +Arguments sdprod_Hall_p'coreP [gT pi H G]. Section Injm. diff --git a/mathcomp/solvable/primitive_action.v b/mathcomp/solvable/primitive_action.v index ae60ce0..c0ab34b 100644 --- a/mathcomp/solvable/primitive_action.v +++ b/mathcomp/solvable/primitive_action.v @@ -187,7 +187,7 @@ End NTransitive. Arguments Scope dtuple_on [_ nat_scope group_scope]. Arguments Scope ntransitive [_ _ nat_scope group_scope group_scope action_scope]. -Implicit Arguments n_act [gT sT n]. +Arguments n_act [gT sT] _ [n]. Notation "n .-dtuple ( S )" := (dtuple_on n S) (at level 8, format "n .-dtuple ( S )") : set_scope. |