diff options
Diffstat (limited to 'mathcomp/solvable')
| -rw-r--r-- | mathcomp/solvable/abelian.v | 32 | ||||
| -rw-r--r-- | mathcomp/solvable/center.v | 2 | ||||
| -rw-r--r-- | mathcomp/solvable/commutator.v | 2 | ||||
| -rw-r--r-- | mathcomp/solvable/cyclic.v | 8 | ||||
| -rw-r--r-- | mathcomp/solvable/frobenius.v | 20 | ||||
| -rw-r--r-- | mathcomp/solvable/gseries.v | 22 | ||||
| -rw-r--r-- | mathcomp/solvable/jordanholder.v | 6 | ||||
| -rw-r--r-- | mathcomp/solvable/maximal.v | 16 | ||||
| -rw-r--r-- | mathcomp/solvable/nilpotent.v | 10 | ||||
| -rw-r--r-- | mathcomp/solvable/pgroup.v | 24 | ||||
| -rw-r--r-- | mathcomp/solvable/primitive_action.v | 10 | ||||
| -rw-r--r-- | mathcomp/solvable/sylow.v | 2 |
12 files changed, 74 insertions, 80 deletions
diff --git a/mathcomp/solvable/abelian.v b/mathcomp/solvable/abelian.v index f3ff7c3..7ca0bdb 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 Scope exponent [_ group_scope]. -Arguments Scope abelem [_ nat_scope group_scope]. -Arguments Scope is_abelem [_ group_scope]. -Arguments Scope pElem [_ nat_scope group_scope]. -Arguments Scope pnElem [_ nat_scope nat_scope group_scope]. -Arguments Scope nElem [_ nat_scope group_scope]. -Arguments Scope pmaxElem [_ nat_scope group_scope]. -Arguments Scope p_rank [_ nat_scope group_scope]. -Arguments Scope rank [_ group_scope]. -Arguments Scope gen_rank [_ group_scope]. +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. 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 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]. +Arguments Ohm _%N _ _%g. +Arguments Ohm_group _%N _ _%g. +Arguments Mho _%N _ _%g. +Arguments Mho_group _%N _ _%g. Arguments OhmPredP [n gT x]. Notation "''Ohm_' n ( G )" := (Ohm n G) @@ -2023,8 +2023,8 @@ Qed. End AbelianStructure. -Arguments Scope abelian_type [_ group_scope]. -Arguments Scope homocyclic [_ group_scope]. +Arguments abelian_type _ _%g. +Arguments homocyclic _ _%g. Prenex Implicits abelian_type homocyclic. Section IsogAbelian. diff --git a/mathcomp/solvable/center.v b/mathcomp/solvable/center.v index c461a9e..f984960 100644 --- a/mathcomp/solvable/center.v +++ b/mathcomp/solvable/center.v @@ -56,7 +56,7 @@ Canonical center_group (G : {group gT}) : {group gT} := End Defs. -Arguments Scope center [_ group_scope]. +Arguments center _ _%g. Notation "''Z' ( A )" := (center A) : group_scope. Notation "''Z' ( H )" := (center_group H) : Group_scope. diff --git a/mathcomp/solvable/commutator.v b/mathcomp/solvable/commutator.v index 6a390ce..ffb07d2 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 Scope derived_at [nat_scope _ group_scope]. +Arguments derived_at _%N _ _%g. Notation "G ^` ( n )" := (derived_at n G) : group_scope. Section DerivedBasics. diff --git a/mathcomp/solvable/cyclic.v b/mathcomp/solvable/cyclic.v index 7663163..bed8c5c 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 Scope cyclic [_ group_scope]. -Arguments Scope generator [_ group_scope group_scope]. -Arguments Scope expg_invn [_ group_scope nat_scope]. +Arguments cyclic _ _%g. +Arguments generator _ _%g _%g. +Arguments expg_invn _ _%g _%N. Arguments cyclicP [gT A]. Prenex Implicits cyclic Zpm generator expg_invn. @@ -556,7 +556,7 @@ Qed. End Metacyclic. -Arguments Scope metacyclic [_ group_scope]. +Arguments metacyclic _ _%g. Prenex Implicits metacyclic. Arguments metacyclicP [gT A]. diff --git a/mathcomp/solvable/frobenius.v b/mathcomp/solvable/frobenius.v index 3416587..eb7ceab 100644 --- a/mathcomp/solvable/frobenius.v +++ b/mathcomp/solvable/frobenius.v @@ -98,17 +98,15 @@ CoInductive has_Frobenius_action G H : Prop := End Definitions. -Arguments Scope semiregular [_ group_scope group_scope]. -Arguments Scope semiprime [_ group_scope group_scope]. -Arguments Scope normedTI [_ group_scope group_scope group_scope]. -Arguments Scope Frobenius_group_with_complement [_ group_scope group_scope]. -Arguments Scope Frobenius_group [_ group_scope]. -Arguments Scope Frobenius_group_with_kernel [_ group_scope group_scope]. -Arguments Scope Frobenius_group_with_kernel_and_complement - [_ group_scope group_scope group_scope]. -Arguments Scope Frobenius_action - [_ group_scope group_scope _ group_scope action_scope]. -Arguments Scope has_Frobenius_action [_ group_scope group_scope]. +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. 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 1dc6a35..c5b5c0c 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 Scope subnormal [_ group_scope group_scope]. -Arguments Scope invariant_factor [_ group_scope group_scope group_scope]. -Arguments Scope stable_factor [_ group_scope group_scope group_scope]. -Arguments Scope central_factor [_ group_scope group_scope group_scope]. -Arguments Scope maximal [_ group_scope group_scope]. -Arguments Scope maximal_eq [_ group_scope group_scope]. -Arguments Scope maxnormal [_ group_scope group_scope group_scope]. -Arguments Scope minnormal [_ group_scope group_scope]. -Arguments Scope simple [_ group_scope]. -Arguments Scope chief_factor [_ group_scope group_scope group_scope]. +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. Prenex Implicits subnormal maximal simple. Notation "H <|<| G" := (subnormal H G) @@ -95,7 +95,7 @@ Notation "A .-central" := (central_factor A) Notation "G .-chief" := (chief_factor G) (at level 2, format "G .-chief") : group_rel_scope. -Arguments Scope group_rel_of [_ group_rel_scope Group_scope Group_scope]. +Arguments group_rel_of _ _%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 7f60bed..91cc709 100644 --- a/mathcomp/solvable/jordanholder.v +++ b/mathcomp/solvable/jordanholder.v @@ -475,10 +475,8 @@ Qed. End StableCompositionSeries. -Arguments Scope maxainv - [_ _ Group_scope Group_scope groupAction_scope group_scope group_scope]. -Arguments Scope asimple - [_ _ Group_scope Group_scope groupAction_scope group_scope]. +Arguments maxainv _ _ _%G _%G _%gact _%g _%g. +Arguments asimple _ _ _%G _%G _%gact _%g. Section StrongJordanHolder. diff --git a/mathcomp/solvable/maximal.v b/mathcomp/solvable/maximal.v index 06cf329..c1a2eb5 100644 --- a/mathcomp/solvable/maximal.v +++ b/mathcomp/solvable/maximal.v @@ -102,14 +102,14 @@ Definition SCN_at n B := [set A in SCN B | n <= 'r(A)]. End Defs. -Arguments Scope charsimple [_ group_scope]. -Arguments Scope Frattini [_ group_scope]. -Arguments Scope Fitting [_ group_scope]. -Arguments Scope critical [_ group_scope group_scope]. -Arguments Scope special [_ group_scope]. -Arguments Scope extraspecial [_ group_scope]. -Arguments Scope SCN [_ group_scope]. -Arguments Scope SCN_at [_ nat_scope group_scope]. +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. diff --git a/mathcomp/solvable/nilpotent.v b/mathcomp/solvable/nilpotent.v index 3d9739d..387ce34 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 Scope lower_central_at [nat_scope _ group_scope]. -Arguments Scope upper_central_at [nat_scope _ group_scope]. +Arguments lower_central_at _%N _ _%g. +Arguments upper_central_at _%N _ _%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 Scope nilpotent [_ group_scope]. -Arguments Scope nil_class [_ group_scope]. -Arguments Scope solvable [_ group_scope]. +Arguments nilpotent _ _%g. +Arguments nil_class _ _%g. +Arguments solvable _ _%g. Prenex Implicits nil_class nilpotent solvable. Section NilpotentProps. diff --git a/mathcomp/solvable/pgroup.v b/mathcomp/solvable/pgroup.v index d383aa7..6507160 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 Scope pgroup [_ nat_scope group_scope]. -Arguments Scope psubgroup [_ nat_scope group_scope group_scope]. -Arguments Scope p_group [_ group_scope]. -Arguments Scope p_elt [_ nat_scope]. -Arguments Scope constt [_ group_scope nat_scope]. -Arguments Scope Hall [_ group_scope group_scope]. -Arguments Scope pHall [_ nat_scope group_scope group_scope]. -Arguments Scope Syl [_ nat_scope group_scope]. -Arguments Scope Sylow [_ group_scope group_scope]. +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. Prenex Implicits p_group Hall Sylow. Notation "pi .-group" := (pgroup pi) @@ -863,8 +863,8 @@ Canonical pcore_group : {group gT} := Eval hnf in [group of pcore]. End PcoreDef. -Arguments Scope pcore [_ nat_scope group_scope]. -Arguments Scope pcore_group [_ nat_scope Group_scope]. +Arguments pcore _ _%N _%g. +Arguments pcore_group _ _%N _%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. @@ -886,7 +886,7 @@ Canonical pseries_group : {group gT} := group pseries_group_set. End PseriesDefs. -Arguments Scope pseries [_ seq_scope group_scope]. +Arguments pseries _ _%SEQ _%g. Local Notation ConsPred p := (@Cons nat_pred p%N) (only parsing). Notation "''O_{' p1 , .. , pn } ( A )" := (pseries (ConsPred p1 .. (ConsPred pn [::]) ..) A) diff --git a/mathcomp/solvable/primitive_action.v b/mathcomp/solvable/primitive_action.v index c0ab34b..58a5f20 100644 --- a/mathcomp/solvable/primitive_action.v +++ b/mathcomp/solvable/primitive_action.v @@ -43,9 +43,8 @@ Definition primitive := End PrimitiveDef. -Arguments Scope imprimitivity_system - [_ _ group_scope group_scope action_scope group_scope]. -Arguments Scope primitive [_ _ group_scope group_scope action_scope]. +Arguments imprimitivity_system _ _ _%g _%g _%act _%g. +Arguments primitive _ _ _%g _%g _%act. Notation "[ 'primitive' A , 'on' S | to ]" := (primitive A S to) (at level 0, format "[ 'primitive' A , 'on' S | to ]") : form_scope. @@ -184,9 +183,8 @@ Qed. End NTransitive. -Arguments Scope dtuple_on [_ nat_scope group_scope]. -Arguments Scope ntransitive - [_ _ nat_scope group_scope group_scope action_scope]. +Arguments dtuple_on _ _%N _%g. +Arguments ntransitive _ _ _%N _%g _%g _%act. Arguments n_act [gT sT] _ [n]. Notation "n .-dtuple ( S )" := (dtuple_on n S) diff --git a/mathcomp/solvable/sylow.v b/mathcomp/solvable/sylow.v index 8925b7d..dd45afa 100644 --- a/mathcomp/solvable/sylow.v +++ b/mathcomp/solvable/sylow.v @@ -535,7 +535,7 @@ Qed. End Zgroups. -Arguments Scope Zgroup [_ group_scope]. +Arguments Zgroup _ _%g. Prenex Implicits Zgroup. Section NilPGroups. |