diff options
Diffstat (limited to 'mathcomp/character')
| -rw-r--r-- | mathcomp/character/character.v | 16 | ||||
| -rw-r--r-- | mathcomp/character/classfun.v | 38 | ||||
| -rw-r--r-- | mathcomp/character/inertia.v | 4 | ||||
| -rw-r--r-- | mathcomp/character/integral_char.v | 2 | ||||
| -rw-r--r-- | mathcomp/character/mxabelem.v | 4 | ||||
| -rw-r--r-- | mathcomp/character/mxrepresentation.v | 26 |
6 files changed, 45 insertions, 45 deletions
diff --git a/mathcomp/character/character.v b/mathcomp/character/character.v index ad0fa32..e522924 100644 --- a/mathcomp/character/character.v +++ b/mathcomp/character/character.v @@ -544,7 +544,7 @@ Notation xcfun_r A := (xcfun_r_head tt A). Notation "phi .[ A ]" := (xcfun phi A) : cfun_scope. Definition pred_Nirr gT B := #|@classes gT B|.-1. -Arguments Scope pred_Nirr [_ group_scope]. +Arguments pred_Nirr _ _%g. Notation Nirr G := (pred_Nirr G).+1. Notation Iirr G := 'I_(Nirr G). @@ -587,7 +587,7 @@ Proof. by apply: onW_bij; exists irr_of_socle. Qed. End IrrClassDef. Prenex Implicits socle_of_IirrK irr_of_socleK. -Arguments Scope socle_of_Iirr [_ ring_scope]. +Arguments socle_of_Iirr _ _%R. Notation "''Chi_' i" := (irr_repr (socle_of_Iirr i)) (at level 8, i at level 2, format "''Chi_' i"). @@ -598,7 +598,7 @@ Definition irr_def gT B : (Nirr B).-tuple 'CF(B) := [tuple of mkseq irr_of (Nirr B)]. Definition irr := locked_with irr_key irr_def. -Arguments Scope irr [_ group_scope]. +Arguments irr _ _%g. Notation "''chi_' i" := (tnth (irr _) i%R) (at level 8, i at level 2, format "''chi_' i") : ring_scope. @@ -816,7 +816,7 @@ Qed. End IrrClass. -Arguments Scope cfReg [_ group_scope]. +Arguments cfReg _ _%g. Prenex Implicits cfIirr. Arguments irr_inj {gT G} [x1 x2]. @@ -1334,7 +1334,7 @@ Qed. End OrthogonalityRelations. -Arguments Scope character_table [_ group_scope]. +Arguments character_table _ _%g. Section InnerProduct. @@ -1565,7 +1565,7 @@ Qed. End IrrConstt. -Arguments Scope irr_constt [_ group_scope cfun_scope]. +Arguments irr_constt _ _%g _%CF. Section Kernel. @@ -1733,7 +1733,7 @@ Qed. End Restrict. -Arguments Scope Res_Iirr [_ group_scope group_scope ring_scope]. +Arguments Res_Iirr _ _%g _%g _%R. Section MoreConstt. @@ -2993,4 +2993,4 @@ Proof. by move/cfker_Ind->; rewrite ?irr_neq0 ?irr_char. Qed. End Induced. -Arguments Scope Ind_Iirr [_ group_scope group_scope ring_scope].
\ No newline at end of file +Arguments Ind_Iirr _ _%g _%g _%R.
\ No newline at end of file diff --git a/mathcomp/character/classfun.v b/mathcomp/character/classfun.v index 3afaa82..7a0e538 100644 --- a/mathcomp/character/classfun.v +++ b/mathcomp/character/classfun.v @@ -392,14 +392,14 @@ End Defs. Bind Scope cfun_scope with classfun. -Arguments Scope classfun [_ group_scope]. -Arguments Scope classfun_on [_ group_scope group_scope]. -Arguments Scope cfun_indicator [_ group_scope]. -Arguments Scope cfAut [_ group_scope _ cfun_scope]. -Arguments Scope cfReal [_ group_scope cfun_scope]. -Arguments Scope cfdot [_ group_scope cfun_scope cfun_scope]. -Arguments Scope cfdotr_head [_ group_scope _ cfun_scope cfun_scope]. -Arguments Scope cfdotr_head [_ group_scope _ cfun_scope]. +Arguments classfun _ _%g. +Arguments classfun_on _ _%g _%g. +Arguments cfun_indicator _ _%g. +Arguments cfAut _ _%g _ _%CF. +Arguments cfReal _ _%g _%CF. +Arguments cfdot _ _%g _%CF _%CF. +Arguments cfdotr_head _ _%g _ _%CF _%CF. +Arguments cfdotr_head _ _%g _ _%CF. Notation "''CF' ( G )" := (classfun G) : type_scope. Notation "''CF' ( G )" := (@fullv _ (cfun_vectType G)) : vspace_scope. @@ -452,12 +452,12 @@ End Predicates. (* Outside section so the nosimpl does not get "cooked" out. *) Definition orthogonal gT D S1 S2 := nosimpl (@ortho_rec gT D S1 S2). -Arguments Scope cfker [_ group_scope cfun_scope]. -Arguments Scope cfaithful [_ group_scope cfun_scope]. -Arguments Scope orthogonal [_ group_scope cfun_scope cfun_scope]. -Arguments Scope pairwise_orthogonal [_ group_scope cfun_scope]. -Arguments Scope orthonormal [_ group_scope cfun_scope]. -Arguments Scope isometry [_ _ group_scope group_scope cfun_scope]. +Arguments cfker _ _%g _%CF. +Arguments cfaithful _ _%g _%CF. +Arguments orthogonal _ _%g _%CF _%CF. +Arguments pairwise_orthogonal _ _%g _%CF. +Arguments orthonormal _ _%g _%CF. +Arguments isometry _ _ _%g _%g _%CF. Notation "{ 'in' CFD , 'isometry' tau , 'to' CFR }" := (isometry_from_to (mem CFD) tau (mem CFR)) @@ -756,7 +756,7 @@ Proof. by []. Qed. End ClassFun. -Arguments Scope classfun_on [_ group_scope group_scope]. +Arguments classfun_on _ _%g _%g. Notation "''CF' ( G , A )" := (classfun_on G A) : ring_scope. Arguments cfun_onP [gT G A phi]. @@ -1394,7 +1394,7 @@ Canonical cfRes_lrmorphism := [lrmorphism of cfRes]. End Restrict. -Arguments Scope cfRes [_ group_scope group_scope cfun_scope]. +Arguments cfRes _ _%g _%g _%CF. Notation "''Res[' H , G ]" := (@cfRes _ H G) (only parsing) : ring_scope. Notation "''Res[' H ]" := 'Res[H, _] : ring_scope. Notation "''Res'" := 'Res[_] (only parsing) : ring_scope. @@ -1727,8 +1727,8 @@ Proof. by move=> nsBG kerH; rewrite -cfMod_eq1 // cfQuoK. Qed. End Coset. -Arguments Scope cfQuo [_ Group_scope group_scope cfun_scope]. -Arguments Scope cfMod [_ Group_scope group_scope cfun_scope]. +Arguments cfQuo _ _%G _%g _%CF. +Arguments cfMod _ _%G _%g _%CF. Prenex Implicits cfMod. Notation "phi / H" := (cfQuo H phi) : cfun_scope. Notation "phi %% H" := (@cfMod _ _ H phi) : cfun_scope. @@ -2327,7 +2327,7 @@ Qed. End Induced. -Arguments Scope cfInd [_ group_scope group_scope cfun_scope]. +Arguments cfInd _ _%g _%g _%CF. Notation "''Ind[' G , H ]" := (@cfInd _ G H) (only parsing) : ring_scope. Notation "''Ind[' G ]" := 'Ind[G, _] : ring_scope. Notation "''Ind'" := 'Ind[_] (only parsing) : ring_scope. diff --git a/mathcomp/character/inertia.v b/mathcomp/character/inertia.v index 7d4a84c..ffa9696 100644 --- a/mathcomp/character/inertia.v +++ b/mathcomp/character/inertia.v @@ -567,8 +567,8 @@ Qed. End Inertia. -Arguments Scope inertia [_ group_scope cfun_scope]. -Arguments Scope cfclass [_ group_scope cfun_scope group_scope]. +Arguments inertia _ _%g _%CF. +Arguments cfclass _ _%g _%CF _%g. Arguments conjg_Iirr_inj [gT H] y [x1 x2]. Notation "''I[' phi ] " := (inertia phi) : group_scope. diff --git a/mathcomp/character/integral_char.v b/mathcomp/character/integral_char.v index 16e3b51..f0553f2 100644 --- a/mathcomp/character/integral_char.v +++ b/mathcomp/character/integral_char.v @@ -157,7 +157,7 @@ Canonical gring_irr_mode_unlockable := [unlockable fun gring_irr_mode]. End GenericClassSums. -Arguments Scope gring_irr_mode [_ Group_scope ring_scope group_scope]. +Arguments gring_irr_mode _ _%G _%R _%g : extra scopes. Notation "''K_' i" := (gring_class_sum _ i) (at level 8, i at level 2, format "''K_' i") : ring_scope. diff --git a/mathcomp/character/mxabelem.v b/mathcomp/character/mxabelem.v index 92fdb0e..b121f4c 100644 --- a/mathcomp/character/mxabelem.v +++ b/mathcomp/character/mxabelem.v @@ -341,7 +341,7 @@ Proof. by move=> sHG; rewrite gacentE // setTI afix_repr. Qed. End FinFieldRepr. -Arguments Scope rowg_mx [_ _ group_scope]. +Arguments rowg_mx _ _ _%g. Notation "''Zm'" := (scale_action _ _ _) (at level 8) : action_scope. Notation "''Zm'" := (scale_groupAction _ _ _) : groupAction_scope. @@ -406,7 +406,7 @@ Open Scope abelem_scope. Definition abelem_dim' (gT : finGroupType) (E : {set gT}) := (logn (pdiv #|E|) #|E|).-1. -Arguments Scope abelem_dim' [_ group_scope]. +Arguments abelem_dim' _ _%g. Notation "''dim' E" := (abelem_dim' E).+1 (at level 10, E at level 8, format "''dim' E") : abelem_scope. diff --git a/mathcomp/character/mxrepresentation.v b/mathcomp/character/mxrepresentation.v index fbd4bc3..4558b3d 100644 --- a/mathcomp/character/mxrepresentation.v +++ b/mathcomp/character/mxrepresentation.v @@ -291,7 +291,7 @@ Structure mx_representation G n := MxRepresentation { repr_mx :> gT -> 'M_n; _ : mx_repr G repr_mx }. Variables (G : {group gT}) (n : nat) (rG : mx_representation G n). -Arguments Scope rG [group_scope]. +Arguments rG _%group_scope : extra scopes. Lemma repr_mx1 : rG 1 = 1%:M. Proof. by case: rG => r []. Qed. @@ -814,10 +814,10 @@ End Regular. End RingRepr. -Arguments Scope mx_representation [_ _ group_scope nat_scope]. -Arguments Scope mx_repr [_ _ group_scope nat_scope _]. -Arguments Scope group_ring [_ _ group_scope]. -Arguments Scope regular_repr [_ _ group_scope]. +Arguments mx_representation _ _ _%g _%N. +Arguments mx_repr _ _ _%g _%N _. +Arguments group_ring _ _ _%g. +Arguments regular_repr _ _ _%g. Arguments centgmxP [R gT G n rG f]. Arguments rkerP [R gT G n rG x]. @@ -891,7 +891,7 @@ Section OneRepresentation. Variable gT : finGroupType. Variables (G : {group gT}) (n : nat) (rG : mx_representation F G n). -Arguments Scope rG [group_scope]. +Arguments rG _%group_scope : extra scopes. Local Notation E_G := (enveloping_algebra_mx rG). @@ -4654,10 +4654,10 @@ End LinearIrr. End FieldRepr. -Arguments Scope rfix_mx [_ _ group_scope nat_scope _ group_scope]. -Arguments Scope gset_mx [_ _ group_scope group_scope]. -Arguments Scope classg_base [_ _ group_scope group_scope]. -Arguments Scope irrType [_ _ group_scope group_scope]. +Arguments rfix_mx _ _ _%g _%N _ _%g. +Arguments gset_mx _ _ _%g _%g. +Arguments classg_base _ _ _%g _%g : extra scopes. +Arguments irrType _ _ _%g _%g : extra scopes. Arguments mxmoduleP [F gT G n rG m U]. Arguments envelop_mxP [F gT G n rG A]. @@ -4681,9 +4681,9 @@ Notation "'Cl" := (Clifford_action _) : action_scope. Bind Scope irrType_scope with socle_sort. Notation "[ 1 sG ]" := (principal_comp sG) : irrType_scope. -Arguments Scope irr_degree [_ _ Group_scope _ irrType_scope]. -Arguments Scope irr_repr [_ _ Group_scope _ irrType_scope group_scope]. -Arguments Scope irr_mode [_ _ Group_scope _ irrType_scope group_scope]. +Arguments irr_degree _ _ _%G _ _%irr. +Arguments irr_repr _ _ _%G _ _%irr _%g : extra scopes. +Arguments irr_mode _ _ _%G _ _%irr _%g : extra scopes. Notation "''n_' i" := (irr_degree i) : group_ring_scope. Notation "''R_' i" := (Wedderburn_subring i) : group_ring_scope. Notation "''e_' i" := (Wedderburn_id i) : group_ring_scope. |