diff options
Diffstat (limited to 'mathcomp/solvable')
| -rw-r--r-- | mathcomp/solvable/abelian.v | 39 | ||||
| -rw-r--r-- | mathcomp/solvable/center.v | 2 | ||||
| -rw-r--r-- | mathcomp/solvable/commutator.v | 2 | ||||
| -rw-r--r-- | mathcomp/solvable/cyclic.v | 15 | ||||
| -rw-r--r-- | mathcomp/solvable/frobenius.v | 8 | ||||
| -rw-r--r-- | mathcomp/solvable/gseries.v | 10 | ||||
| -rw-r--r-- | mathcomp/solvable/maximal.v | 2 | ||||
| -rw-r--r-- | mathcomp/solvable/nilpotent.v | 7 | ||||
| -rw-r--r-- | mathcomp/solvable/pgroup.v | 18 | ||||
| -rw-r--r-- | mathcomp/solvable/sylow.v | 3 |
10 files changed, 49 insertions, 57 deletions
diff --git a/mathcomp/solvable/abelian.v b/mathcomp/solvable/abelian.v index 7ca0bdb..5f1a013 100644 --- a/mathcomp/solvable/abelian.v +++ b/mathcomp/solvable/abelian.v @@ -196,7 +196,7 @@ Arguments Ohm _%N _ _%g. Arguments Ohm_group _%N _ _%g. Arguments Mho _%N _ _%g. Arguments Mho_group _%N _ _%g. -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. -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. -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. -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. -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. -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]. +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. @@ -2023,9 +2023,8 @@ Qed. End AbelianStructure. -Arguments abelian_type _ _%g. -Arguments homocyclic _ _%g. -Prenex Implicits abelian_type homocyclic. +Arguments abelian_type {_} _%g. +Arguments homocyclic {_} _%g. Section IsogAbelian. diff --git a/mathcomp/solvable/center.v b/mathcomp/solvable/center.v index f984960..98434ba 100644 --- a/mathcomp/solvable/center.v +++ b/mathcomp/solvable/center.v @@ -187,7 +187,7 @@ End Injm. End Center. -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 ffb07d2..dcd53ce 100644 --- a/mathcomp/solvable/commutator.v +++ b/mathcomp/solvable/commutator.v @@ -352,7 +352,7 @@ Proof. exact: commG1P. Qed. End Commutator_properties. -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 bed8c5c..046f4a2 100644 --- a/mathcomp/solvable/cyclic.v +++ b/mathcomp/solvable/cyclic.v @@ -289,11 +289,11 @@ Proof. by rewrite /order => /(<[a]> =P _)->. Qed. End Cyclic. -Arguments cyclic _ _%g. -Arguments generator _ _%g _%g. -Arguments expg_invn _ _%g _%N. -Arguments cyclicP [gT A]. -Prenex Implicits cyclic Zpm generator expg_invn. +Arguments cyclic {_} _%g. +Arguments generator {_}_%g _%g. +Arguments expg_invn {_} _%g _%N. +Arguments cyclicP {gT A}. +Prenex Implicits cyclic Zpm. (* Euler's theorem *) Theorem Euler_exp_totient a n : coprime a n -> a ^ totient n = 1 %[mod n]. @@ -556,9 +556,8 @@ Qed. End Metacyclic. -Arguments metacyclic _ _%g. -Prenex Implicits metacyclic. -Arguments metacyclicP [gT A]. +Arguments metacyclic {_} _%g. +Arguments metacyclicP {gT A}. (* Automorphisms of cyclic groups. *) Section CyclicAutomorphism. diff --git a/mathcomp/solvable/frobenius.v b/mathcomp/solvable/frobenius.v index 98657b4..f7edfc9 100644 --- a/mathcomp/solvable/frobenius.v +++ b/mathcomp/solvable/frobenius.v @@ -244,7 +244,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. -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 @@ -620,9 +620,9 @@ Qed. End FrobeniusBasics. -Arguments normedTI_P [gT A G L]. -Arguments normedTI_memJ_P [gT A G L]. -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 c5b5c0c..a1830b9 100644 --- a/mathcomp/solvable/gseries.v +++ b/mathcomp/solvable/gseries.v @@ -71,17 +71,16 @@ Definition simple A := minnormal A A. Definition chief_factor A V U := maxnormal V U A && (U <| A). End GroupDefs. -Arguments subnormal _ _%g _%g. +Arguments subnormal {_} _%g _%g. Arguments invariant_factor _ _%g _%g _%g. Arguments stable_factor _ _%g _%g _%g. Arguments central_factor _ _%g _%g _%g. -Arguments maximal _ _%g _%g. +Arguments maximal {_} _%g _%g. Arguments maximal_eq _ _%g _%g. Arguments maxnormal _ _%g _%g _%g. Arguments minnormal _ _%g _%g. -Arguments simple _ _%g. +Arguments simple {_} _%g. Arguments chief_factor _ _%g _%g _%g. -Prenex Implicits subnormal maximal simple. Notation "H <|<| G" := (subnormal H G) (at level 70, no associativity) : group_scope. @@ -212,8 +211,7 @@ Qed. End Subnormal. -Arguments subnormalP [gT H G]. -Prenex Implicits subnormalP. +Arguments subnormalP {gT H G}. Section MorphSubNormal. diff --git a/mathcomp/solvable/maximal.v b/mathcomp/solvable/maximal.v index c1a2eb5..5f7a9ed 100644 --- a/mathcomp/solvable/maximal.v +++ b/mathcomp/solvable/maximal.v @@ -1649,4 +1649,4 @@ Qed. End SCN. -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/nilpotent.v b/mathcomp/solvable/nilpotent.v index 387ce34..d631919 100644 --- a/mathcomp/solvable/nilpotent.v +++ b/mathcomp/solvable/nilpotent.v @@ -75,10 +75,9 @@ Definition solvable := End PropertiesDefs. -Arguments nilpotent _ _%g. -Arguments nil_class _ _%g. -Arguments solvable _ _%g. -Prenex Implicits nil_class nilpotent solvable. +Arguments nilpotent {_} _%g. +Arguments nil_class {_} _%g. +Arguments solvable {_} _%g. Section NilpotentProps. diff --git a/mathcomp/solvable/pgroup.v b/mathcomp/solvable/pgroup.v index 6507160..6c02e7b 100644 --- a/mathcomp/solvable/pgroup.v +++ b/mathcomp/solvable/pgroup.v @@ -83,16 +83,15 @@ Definition Sylow A B := p_group B && Hall A B. End PgroupDefs. -Arguments pgroup _ _%N _%g. +Arguments pgroup {_} _%N _%g. Arguments psubgroup _ _%N _%g _%g. Arguments p_group _ _%g. Arguments p_elt _ _%N. Arguments constt _ _%g _%N. -Arguments Hall _ _%g _%g. +Arguments Hall {_} _%g _%g. Arguments pHall _ _%N _%g _%g. Arguments Syl _ _%N _%g. -Arguments Sylow _ _%g _%g. -Prenex Implicits p_group Hall Sylow. +Arguments Sylow {_} _%g _%g. Notation "pi .-group" := (pgroup pi) (at level 2, format "pi .-group") : group_scope. @@ -170,7 +169,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. -Arguments pgroupP [pi G]. +Arguments pgroupP {pi G}. Lemma pgroup1 pi : pi.-group [1 gT]. Proof. by rewrite /pgroup cards1. Qed. @@ -679,9 +678,8 @@ Qed. End PgroupProps. -Arguments pgroupP [gT pi G]. -Arguments constt1P [gT pi x]. -Prenex Implicits pgroupP constt1P. +Arguments pgroupP {gT pi G}. +Arguments constt1P {gT pi x}. Section NormalHall. @@ -1302,8 +1300,8 @@ Qed. End EqPcore. -Arguments sdprod_Hall_pcoreP [pi gT H G]. -Arguments sdprod_Hall_p'coreP [gT pi H G]. +Arguments sdprod_Hall_pcoreP {pi gT H G}. +Arguments sdprod_Hall_p'coreP {gT pi H G}. Section Injm. diff --git a/mathcomp/solvable/sylow.v b/mathcomp/solvable/sylow.v index dd45afa..f940ec9 100644 --- a/mathcomp/solvable/sylow.v +++ b/mathcomp/solvable/sylow.v @@ -535,8 +535,7 @@ Qed. End Zgroups. -Arguments Zgroup _ _%g. -Prenex Implicits Zgroup. +Arguments Zgroup {_} _%g. Section NilPGroups. |