diff options
Diffstat (limited to 'mathcomp/solvable')
| -rw-r--r-- | mathcomp/solvable/abelian.v | 32 | ||||
| -rw-r--r-- | mathcomp/solvable/burnside_app.v | 2 | ||||
| -rw-r--r-- | mathcomp/solvable/center.v | 4 | ||||
| -rw-r--r-- | mathcomp/solvable/commutator.v | 4 | ||||
| -rw-r--r-- | mathcomp/solvable/cyclic.v | 8 | ||||
| -rw-r--r-- | mathcomp/solvable/frobenius.v | 18 | ||||
| -rw-r--r-- | mathcomp/solvable/gseries.v | 22 | ||||
| -rw-r--r-- | mathcomp/solvable/jordanholder.v | 4 | ||||
| -rw-r--r-- | mathcomp/solvable/maximal.v | 20 | ||||
| -rw-r--r-- | mathcomp/solvable/nilpotent.v | 16 | ||||
| -rw-r--r-- | mathcomp/solvable/pgroup.v | 36 | ||||
| -rw-r--r-- | mathcomp/solvable/primitive_action.v | 12 | ||||
| -rw-r--r-- | mathcomp/solvable/sylow.v | 2 |
13 files changed, 88 insertions, 92 deletions
diff --git a/mathcomp/solvable/abelian.v b/mathcomp/solvable/abelian.v index 5f1a013..746898f 100644 --- a/mathcomp/solvable/abelian.v +++ b/mathcomp/solvable/abelian.v @@ -111,16 +111,16 @@ Definition gen_rank A := #|[arg min_(B < A | <<B>> == A) #|B|]|. End AbelianDefs. -Arguments exponent _ _%g. -Arguments abelem _ _%N _%g. -Arguments is_abelem _ _%g. -Arguments pElem _ _%N _%g. -Arguments pnElem _ _%N _%N _%g. -Arguments nElem _ _%N _%g. -Arguments pmaxElem _ _%N _%g. -Arguments p_rank _ _%N _%g. -Arguments rank _ _%g. -Arguments gen_rank _ _%g. +Arguments exponent {gT} A%g. +Arguments abelem {gT} p%N A%g. +Arguments is_abelem {gT} A%g. +Arguments pElem {gT} p%N A%g. +Arguments pnElem {gT} p%N n%N A%g. +Arguments nElem {gT} n%N A%g. +Arguments pmaxElem {gT} p%N A%g. +Arguments p_rank {gT} p%N A%g. +Arguments rank {gT} A%g. +Arguments gen_rank {gT} A%g. Notation "''Ldiv_' n ()" := (Ldiv _ n) (at level 8, n at level 2, format "''Ldiv_' n ()") : group_scope. @@ -192,10 +192,10 @@ Qed. End Functors. -Arguments Ohm _%N _ _%g. -Arguments Ohm_group _%N _ _%g. -Arguments Mho _%N _ _%g. -Arguments Mho_group _%N _ _%g. +Arguments Ohm n%N {gT} A%g. +Arguments Ohm_group n%N {gT} A%g. +Arguments Mho n%N {gT} A%g. +Arguments Mho_group n%N {gT} A%g. Arguments OhmPredP {n gT x}. Notation "''Ohm_' n ( G )" := (Ohm n G) @@ -2023,8 +2023,8 @@ Qed. End AbelianStructure. -Arguments abelian_type {_} _%g. -Arguments homocyclic {_} _%g. +Arguments abelian_type {gT} A%g. +Arguments homocyclic {gT} A%g. Section IsogAbelian. diff --git a/mathcomp/solvable/burnside_app.v b/mathcomp/solvable/burnside_app.v index 1c804cc..10cbbaa 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. -Arguments burnside_formula [gT]. +Arguments burnside_formula {gT}. Section colouring. diff --git a/mathcomp/solvable/center.v b/mathcomp/solvable/center.v index 98434ba..88774db 100644 --- a/mathcomp/solvable/center.v +++ b/mathcomp/solvable/center.v @@ -56,11 +56,11 @@ Canonical center_group (G : {group gT}) : {group gT} := End Defs. -Arguments center _ _%g. +Arguments center {gT} A%g. Notation "''Z' ( A )" := (center A) : group_scope. Notation "''Z' ( H )" := (center_group H) : Group_scope. -Lemma morphim_center : GFunctor.pcontinuous center. +Lemma morphim_center : GFunctor.pcontinuous (@center). Proof. by move=> gT rT G D f; apply: morphim_subcent. Qed. Canonical center_igFun := [igFun by fun _ _ => subsetIl _ _ & morphim_center]. diff --git a/mathcomp/solvable/commutator.v b/mathcomp/solvable/commutator.v index dcd53ce..7895116 100644 --- a/mathcomp/solvable/commutator.v +++ b/mathcomp/solvable/commutator.v @@ -33,7 +33,7 @@ Definition derived_at_rec n (gT : finGroupType) (A : {set gT}) := (* "cooking" destroys it. *) Definition derived_at := nosimpl derived_at_rec. -Arguments derived_at _%N _ _%g. +Arguments derived_at n%N {gT} A%g. Notation "G ^` ( n )" := (derived_at n G) : group_scope. Section DerivedBasics. @@ -354,7 +354,7 @@ End Commutator_properties. Arguments derG1P {gT G}. -Lemma der_cont n : GFunctor.continuous (derived_at n). +Lemma der_cont n : GFunctor.continuous (@derived_at n). Proof. by move=> aT rT G f; rewrite morphim_der. Qed. Canonical der_igFun n := [igFun by der_sub^~ n & der_cont n]. diff --git a/mathcomp/solvable/cyclic.v b/mathcomp/solvable/cyclic.v index 046f4a2..e370a7e 100644 --- a/mathcomp/solvable/cyclic.v +++ b/mathcomp/solvable/cyclic.v @@ -289,9 +289,9 @@ Proof. by rewrite /order => /(<[a]> =P _)->. Qed. End Cyclic. -Arguments cyclic {_} _%g. -Arguments generator {_}_%g _%g. -Arguments expg_invn {_} _%g _%N. +Arguments cyclic {gT} A%g. +Arguments generator {gT} A%g a%g. +Arguments expg_invn {gT} A%g k%N. Arguments cyclicP {gT A}. Prenex Implicits cyclic Zpm. @@ -556,7 +556,7 @@ Qed. End Metacyclic. -Arguments metacyclic {_} _%g. +Arguments metacyclic {gT} A%g. Arguments metacyclicP {gT A}. (* Automorphisms of cyclic groups. *) diff --git a/mathcomp/solvable/frobenius.v b/mathcomp/solvable/frobenius.v index f7edfc9..01ba8f3 100644 --- a/mathcomp/solvable/frobenius.v +++ b/mathcomp/solvable/frobenius.v @@ -98,15 +98,15 @@ Variant has_Frobenius_action G H : Prop := End Definitions. -Arguments semiregular _ _%g _%g. -Arguments semiprime _ _%g _%g. -Arguments normedTI _ _%g _%g _%g. -Arguments Frobenius_group_with_complement _ _%g _%g. -Arguments Frobenius_group _ _%g. -Arguments Frobenius_group_with_kernel _ _%g _%g. -Arguments Frobenius_group_with_kernel_and_complement _ _%g _%g _%g. -Arguments Frobenius_action _ _%g _%g _ _%g _%act. -Arguments has_Frobenius_action _ _%g _%g. +Arguments semiregular {gT} K%g H%g. +Arguments semiprime {gT} K%g H%g. +Arguments normedTI {gT} A%g G%g L%g. +Arguments Frobenius_group_with_complement {gT} G%g H%g. +Arguments Frobenius_group {gT} G%g. +Arguments Frobenius_group_with_kernel {gT} G%g K%g. +Arguments Frobenius_group_with_kernel_and_complement {gT} G%g K%g H%g. +Arguments Frobenius_action {gT} G%g H%g {sT} S%g to%act. +Arguments has_Frobenius_action {gT} G%g H%g. Notation "[ 'Frobenius' G 'with' 'complement' H ]" := (Frobenius_group_with_complement G H) diff --git a/mathcomp/solvable/gseries.v b/mathcomp/solvable/gseries.v index a1830b9..3e99bfb 100644 --- a/mathcomp/solvable/gseries.v +++ b/mathcomp/solvable/gseries.v @@ -71,16 +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 invariant_factor _ _%g _%g _%g. -Arguments stable_factor _ _%g _%g _%g. -Arguments central_factor _ _%g _%g _%g. -Arguments maximal {_} _%g _%g. -Arguments maximal_eq _ _%g _%g. -Arguments maxnormal _ _%g _%g _%g. -Arguments minnormal _ _%g _%g. -Arguments simple {_} _%g. -Arguments chief_factor _ _%g _%g _%g. +Arguments subnormal {gT} A%g B%g. +Arguments invariant_factor {gT} A%g B%g C%g. +Arguments stable_factor {gT} A%g V%g U%g. +Arguments central_factor {gT} A%g V%g U%g. +Arguments maximal {gT} A%g B%g. +Arguments maximal_eq {gT} A%g B%g. +Arguments maxnormal {gT} A%g B%g U%g. +Arguments minnormal {gT} A%g B%g. +Arguments simple {gT} A%g. +Arguments chief_factor {gT} A%g V%g U%g. Notation "H <|<| G" := (subnormal H G) (at level 70, no associativity) : group_scope. @@ -94,7 +94,7 @@ Notation "A .-central" := (central_factor A) Notation "G .-chief" := (chief_factor G) (at level 2, format "G .-chief") : group_rel_scope. -Arguments group_rel_of _ _%group_rel_scope _%G _%G : extra scopes. +Arguments group_rel_of {gT} r%group_rel_scope _%G _%G : extra scopes. Notation "r .-series" := (path (rel_of_simpl_rel (group_rel_of r))) (at level 2, format "r .-series") : group_scope. diff --git a/mathcomp/solvable/jordanholder.v b/mathcomp/solvable/jordanholder.v index 91cc709..bda66bd 100644 --- a/mathcomp/solvable/jordanholder.v +++ b/mathcomp/solvable/jordanholder.v @@ -475,8 +475,8 @@ Qed. End StableCompositionSeries. -Arguments maxainv _ _ _%G _%G _%gact _%g _%g. -Arguments asimple _ _ _%G _%G _%gact _%g. +Arguments maxainv {aT rT D%G A%G} to%gact B%g C%g. +Arguments asimple {aT rT D%G A%G} to%gact K%g. Section StrongJordanHolder. diff --git a/mathcomp/solvable/maximal.v b/mathcomp/solvable/maximal.v index 5f7a9ed..781abbe 100644 --- a/mathcomp/solvable/maximal.v +++ b/mathcomp/solvable/maximal.v @@ -102,16 +102,14 @@ Definition SCN_at n B := [set A in SCN B | n <= 'r(A)]. End Defs. -Arguments charsimple _ _%g. -Arguments Frattini _ _%g. -Arguments Fitting _ _%g. -Arguments critical _ _%g _%g. -Arguments special _ _%g. -Arguments extraspecial _ _%g. -Arguments SCN _ _%g. -Arguments SCN_at _ _%N _%g. - -Prenex Implicits maximal simple charsimple critical special extraspecial. +Arguments charsimple {gT} A%g. +Arguments Frattini {gT} A%g. +Arguments Fitting {gT} A%g. +Arguments critical {gT} A%g B%g. +Arguments special {gT} A%g. +Arguments extraspecial {gT} A%g. +Arguments SCN {gT} B%g. +Arguments SCN_at {gT} n%N B%g. Notation "''Phi' ( A )" := (Frattini A) (at level 8, format "''Phi' ( A )") : group_scope. @@ -459,7 +457,7 @@ Section FittingFun. Implicit Types gT rT : finGroupType. -Lemma morphim_Fitting : GFunctor.pcontinuous Fitting. +Lemma morphim_Fitting : GFunctor.pcontinuous (@Fitting). Proof. move=> gT rT G D f; apply: Fitting_max. by rewrite morphim_normal ?Fitting_normal. diff --git a/mathcomp/solvable/nilpotent.v b/mathcomp/solvable/nilpotent.v index d631919..aee3113 100644 --- a/mathcomp/solvable/nilpotent.v +++ b/mathcomp/solvable/nilpotent.v @@ -52,8 +52,8 @@ Definition lower_central_at n := lower_central_at_rec n.-1. (* "cooking" destroys it. *) Definition upper_central_at := nosimpl upper_central_at_rec. -Arguments lower_central_at _%N _ _%g. -Arguments upper_central_at _%N _ _%g. +Arguments lower_central_at n%N {gT} A%g. +Arguments upper_central_at n%N {gT} A%g. Notation "''L_' n ( G )" := (lower_central_at n G) (at level 8, n at level 2, format "''L_' n ( G )") : group_scope. @@ -75,9 +75,9 @@ Definition solvable := End PropertiesDefs. -Arguments nilpotent {_} _%g. -Arguments nil_class {_} _%g. -Arguments solvable {_} _%g. +Arguments nilpotent {gT} A%g. +Arguments nil_class {gT} A%g. +Arguments solvable {gT} A%g. Section NilpotentProps. @@ -320,7 +320,7 @@ End LowerCentral. Notation "''L_' n ( G )" := (lower_central_at_group n G) : Group_scope. -Lemma lcn_cont n : GFunctor.continuous (lower_central_at n). +Lemma lcn_cont n : GFunctor.continuous (@lower_central_at n). Proof. case: n => //; elim=> // n IHn g0T h0T H phi. by rewrite !lcnSn morphimR ?lcn_sub // commSg ?IHn. @@ -338,7 +338,7 @@ Implicit Type gT : finGroupType. Lemma ucn_pmap : exists hZ : GFunctor.pmap, @upper_central_at n = hZ. Proof. elim: n => [|n' [hZ defZ]]; first by exists trivGfun_pgFun. -by exists [pgFun of center %% hZ]; rewrite /= -defZ. +by exists [pgFun of @center %% hZ]; rewrite /= -defZ. Qed. (* Now extract all the intermediate facts of the last proof. *) @@ -351,7 +351,7 @@ Canonical upper_central_at_group gT G := Group (@ucn_group_set gT G). Lemma ucn_sub gT (G : {group gT}) : 'Z_n(G) \subset G. Proof. by have [hZ ->] := ucn_pmap; apply: gFsub. Qed. -Lemma morphim_ucn : GFunctor.pcontinuous (upper_central_at n). +Lemma morphim_ucn : GFunctor.pcontinuous (@upper_central_at n). Proof. by have [hZ ->] := ucn_pmap; apply: pmorphimF. Qed. Canonical ucn_igFun := [igFun by ucn_sub & morphim_ucn]. diff --git a/mathcomp/solvable/pgroup.v b/mathcomp/solvable/pgroup.v index 6c02e7b..d62154f 100644 --- a/mathcomp/solvable/pgroup.v +++ b/mathcomp/solvable/pgroup.v @@ -83,15 +83,15 @@ Definition Sylow A B := p_group B && Hall A B. End PgroupDefs. -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 pHall _ _%N _%g _%g. -Arguments Syl _ _%N _%g. -Arguments Sylow {_} _%g _%g. +Arguments pgroup {gT} pi%N A%g. +Arguments psubgroup {gT} pi%N A%g B%g. +Arguments p_group {gT} A%g. +Arguments p_elt {gT} pi%N x. +Arguments constt {gT} x%g pi%N. +Arguments Hall {gT} A%g B%g. +Arguments pHall {gT} pi%N A%g B%g. +Arguments Syl {gT} p%N A%g. +Arguments Sylow {gT} A%g B%g. Notation "pi .-group" := (pgroup pi) (at level 2, format "pi .-group") : group_scope. @@ -861,8 +861,8 @@ Canonical pcore_group : {group gT} := Eval hnf in [group of pcore]. End PcoreDef. -Arguments pcore _ _%N _%g. -Arguments pcore_group _ _%N _%G. +Arguments pcore pi%N {gT} A%g. +Arguments pcore_group pi%N {gT} A%G. Notation "''O_' pi ( G )" := (pcore pi G) (at level 8, pi at level 2, format "''O_' pi ( G )") : group_scope. Notation "''O_' pi ( G )" := (pcore_group pi G) : Group_scope. @@ -884,7 +884,7 @@ Canonical pseries_group : {group gT} := group pseries_group_set. End PseriesDefs. -Arguments pseries _ _%SEQ _%g. +Arguments pseries pis%SEQ {gT} _%g. Local Notation ConsPred p := (@Cons nat_pred p%N) (only parsing). Notation "''O_{' p1 , .. , pn } ( A )" := (pseries (ConsPred p1 .. (ConsPred pn [::]) ..) A) @@ -977,7 +977,7 @@ Section MorphPcore. Implicit Types (pi : nat_pred) (gT rT : finGroupType). -Lemma morphim_pcore pi : GFunctor.pcontinuous (pcore pi). +Lemma morphim_pcore pi : GFunctor.pcontinuous (@pcore pi). Proof. move=> gT rT D G f; apply/bigcapsP=> M /normal_sub_max_pgroup; apply. by rewrite morphim_pgroup ?pcore_pgroup. @@ -1054,7 +1054,7 @@ Lemma pseries_rcons pi pis gT (A : {set gT}) : Proof. by rewrite /pseries rev_rcons. Qed. Lemma pseries_subfun pis : - GFunctor.closed (pseries pis) /\ GFunctor.pcontinuous (pseries pis). + GFunctor.closed (@pseries pis) /\ GFunctor.pcontinuous (@pseries pis). Proof. elim/last_ind: pis => [|pis pi [sFpi fFpi]]. by split=> [gT G | gT rT D G f]; rewrite (sub1G, morphim1). @@ -1064,13 +1064,13 @@ split=> [gT G | gT rT D G f]; rewrite !pseries_rcons ?(pcore_mod_sub F) //. exact: (morphim_pcore_mod F). Qed. -Lemma pseries_sub pis : GFunctor.closed (pseries pis). +Lemma pseries_sub pis : GFunctor.closed (@pseries pis). Proof. by case: (pseries_subfun pis). Qed. -Lemma morphim_pseries pis : GFunctor.pcontinuous (pseries pis). +Lemma morphim_pseries pis : GFunctor.pcontinuous (@pseries pis). Proof. by case: (pseries_subfun pis). Qed. -Lemma pseriesS pis : GFunctor.hereditary (pseries pis). +Lemma pseriesS pis : GFunctor.hereditary (@pseries pis). Proof. exact: (morphim_pseries pis). Qed. Canonical pseries_igFun pis := [igFun by pseries_sub pis & morphim_pseries pis]. @@ -1149,7 +1149,7 @@ apply: (quotient_inj nH2H). by apply/andP; rewrite /= -cats1 pseries_sub_catl pseries_norm2. rewrite /= quotient_pseries /= -IHpi -rcons_cat. rewrite -[G / _ / _](morphim_invm inj_f) //= {2}im_f //. -rewrite -(@injmF [igFun of pcore pi]) /= ?injm_invm ?im_f // -quotient_pseries. +rewrite -(@injmF [igFun of @pcore pi]) /= ?injm_invm ?im_f // -quotient_pseries. by rewrite -im_f ?morphim_invm ?morphimS ?normal_sub. Qed. diff --git a/mathcomp/solvable/primitive_action.v b/mathcomp/solvable/primitive_action.v index 58a5f20..fa27e75 100644 --- a/mathcomp/solvable/primitive_action.v +++ b/mathcomp/solvable/primitive_action.v @@ -43,14 +43,12 @@ Definition primitive := End PrimitiveDef. -Arguments imprimitivity_system _ _ _%g _%g _%act _%g. -Arguments primitive _ _ _%g _%g _%act. +Arguments imprimitivity_system {aT sT} A%g S%g to%act Q%g. +Arguments primitive {aT sT} A%g S%g to%act. Notation "[ 'primitive' A , 'on' S | to ]" := (primitive A S to) (at level 0, format "[ 'primitive' A , 'on' S | to ]") : form_scope. -Prenex Implicits imprimitivity_system. - Section Primitive. Variables (aT : finGroupType) (sT : finType). @@ -183,9 +181,9 @@ Qed. End NTransitive. -Arguments dtuple_on _ _%N _%g. -Arguments ntransitive _ _ _%N _%g _%g _%act. -Arguments n_act [gT sT] _ [n]. +Arguments dtuple_on {sT} n%N S%g. +Arguments ntransitive {gT sT} n%N A%g S%g to%act. +Arguments n_act {gT sT} to {n} t a. Notation "n .-dtuple ( S )" := (dtuple_on n S) (at level 8, format "n .-dtuple ( S )") : set_scope. diff --git a/mathcomp/solvable/sylow.v b/mathcomp/solvable/sylow.v index f940ec9..a428c0d 100644 --- a/mathcomp/solvable/sylow.v +++ b/mathcomp/solvable/sylow.v @@ -535,7 +535,7 @@ Qed. End Zgroups. -Arguments Zgroup {_} _%g. +Arguments Zgroup {gT} A%g. Section NilPGroups. |