diff options
Diffstat (limited to 'mathcomp/character')
| -rw-r--r-- | mathcomp/character/character.v | 26 | ||||
| -rw-r--r-- | mathcomp/character/classfun.v | 42 | ||||
| -rw-r--r-- | mathcomp/character/inertia.v | 6 | ||||
| -rw-r--r-- | mathcomp/character/integral_char.v | 2 | ||||
| -rw-r--r-- | mathcomp/character/mxabelem.v | 4 | ||||
| -rw-r--r-- | mathcomp/character/mxrepresentation.v | 30 |
6 files changed, 54 insertions, 56 deletions
diff --git a/mathcomp/character/character.v b/mathcomp/character/character.v index 6752623..a657fa5 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 pred_Nirr _ _%g. +Arguments pred_Nirr {gT} B%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 socle_of_Iirr _ _%R. +Arguments socle_of_Iirr {gT G%G} i%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 irr _ _%g. +Arguments irr {gT} B%g. Notation "''chi_' i" := (tnth (irr _) i%R) (at level 8, i at level 2, format "''chi_' i") : ring_scope. @@ -621,7 +621,7 @@ Proof. by move/Iirr1_neq0; exists (inord 1). Qed. Lemma irrRepr i : cfRepr 'Chi_i = 'chi_i. Proof. -rewrite [irr]unlock (tnth_nth 0) nth_mkseq // -[<<G>>]/(gval _) genGidG. +rewrite [@irr]unlock (tnth_nth 0) nth_mkseq // -[<<G>>]/(gval _) genGidG. by rewrite cfRes_id inord_val. Qed. @@ -816,7 +816,7 @@ Qed. End IrrClass. -Arguments cfReg _ _%g. +Arguments cfReg {gT} B%g. Prenex Implicits cfIirr. Arguments irr_inj {gT G} [x1 x2]. @@ -1334,7 +1334,7 @@ Qed. End OrthogonalityRelations. -Arguments character_table _ _%g. +Arguments character_table {gT} G%g. Section InnerProduct. @@ -1565,7 +1565,7 @@ Qed. End IrrConstt. -Arguments irr_constt _ _%g _%CF. +Arguments irr_constt {gT B%g} phi%CF. Section Kernel. @@ -1733,7 +1733,7 @@ Qed. End Restrict. -Arguments Res_Iirr _ _%g _%g _%R. +Arguments Res_Iirr {gT A%g} B%g i%R. Section MoreConstt. @@ -1870,7 +1870,7 @@ Proof. by apply/eqP; rewrite isom_Iirr_eq0. Qed. End Isom. -Arguments isom_Iirr_inj [aT rT G f R] isoGR [x1 x2]. +Arguments isom_Iirr_inj {aT rT G f R} isoGR [i1 i2] : rename. Section IsomInv. @@ -1938,7 +1938,7 @@ Qed. End Sdprod. -Arguments sdprod_Iirr_inj [gT K H G] defG [x1 x2]. +Arguments sdprod_Iirr_inj {gT K H G} defG [i1 i2] : rename. Section DProd. @@ -2089,7 +2089,7 @@ Proof. by apply/(canLR dprod_IirrK); rewrite dprod_Iirr0. Qed. End DProd. -Arguments dprod_Iirr_inj [gT G K H] KxH [x1 x2]. +Arguments dprod_Iirr_inj {gT G K H} KxH [i1 i2] : rename. Lemma dprod_IirrC (gT : finGroupType) (G K H : {group gT}) (KxH : K \x H = G) (HxK : H \x K = G) i j : @@ -2257,7 +2257,7 @@ Qed. End Aut. -Arguments aut_Iirr_inj [gT G] u [x1 x2]. +Arguments aut_Iirr_inj {gT G} u [i1 i2] : rename. Section Coset. @@ -2993,4 +2993,4 @@ Proof. by move/cfker_Ind->; rewrite ?irr_neq0 ?irr_char. Qed. End Induced. -Arguments Ind_Iirr _ _%g _%g _%R.
\ No newline at end of file +Arguments Ind_Iirr {gT A%g} B%g i%R. diff --git a/mathcomp/character/classfun.v b/mathcomp/character/classfun.v index ac3e5bc..7b2b90d 100644 --- a/mathcomp/character/classfun.v +++ b/mathcomp/character/classfun.v @@ -392,14 +392,13 @@ End Defs. Bind Scope cfun_scope with classfun. -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. +Arguments classfun {gT} B%g. +Arguments classfun_on {gT} B%g A%g. +Arguments cfun_indicator {gT} B%g. +Arguments cfAut {gT B%g} u phi%CF. +Arguments cfReal {gT B%g} phi%CF. +Arguments cfdot {gT B%g} phi%CF psi%CF. +Arguments cfdotr_head {gT B%g} k psi%CF phi%CF. Notation "''CF' ( G )" := (classfun G) : type_scope. Notation "''CF' ( G )" := (@fullv _ (cfun_vectType G)) : vspace_scope. @@ -452,12 +451,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 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. +Arguments cfker {gT D%g} phi%CF. +Arguments cfaithful {gT D%g} phi%CF. +Arguments orthogonal {gT D%g} S1%CF S2%CF. +Arguments pairwise_orthogonal {gT D%g} S%CF. +Arguments orthonormal {gT D%g} S%CF. +Arguments isometry {gT rT D%g R%g} tau%CF. Notation "{ 'in' CFD , 'isometry' tau , 'to' CFR }" := (isometry_from_to (mem CFD) tau (mem CFR)) @@ -756,7 +755,7 @@ Proof. by []. Qed. End ClassFun. -Arguments classfun_on _ _%g _%g. +Arguments classfun_on {gT} B%g A%g. Notation "''CF' ( G , A )" := (classfun_on G A) : ring_scope. Arguments cfun_onP {gT G A phi}. @@ -1394,7 +1393,7 @@ Canonical cfRes_lrmorphism := [lrmorphism of cfRes]. End Restrict. -Arguments cfRes _ _%g _%g _%CF. +Arguments cfRes {gT} A%g {B%g} phi%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. @@ -1621,7 +1620,7 @@ Proof. exact: cforder_inj_rmorph cfIsom_inj. Qed. End InvMorphism. -Arguments cfIsom_inj [aT rT G f R] isoGR [x1 x2]. +Arguments cfIsom_inj {aT rT G f R} isoGR [phi1 phi2] : rename. Section Coset. @@ -1727,9 +1726,8 @@ Proof. by move=> nsBG kerH; rewrite -cfMod_eq1 // cfQuoK. Qed. End Coset. -Arguments cfQuo _ _%G _%g _%CF. -Arguments cfMod _ _%G _%g _%CF. -Prenex Implicits cfMod. +Arguments cfQuo {gT G%G} B%g phi%CF. +Arguments cfMod {gT G%G B%g} phi%CF. Notation "phi / H" := (cfQuo H phi) : cfun_scope. Notation "phi %% H" := (@cfMod _ _ H phi) : cfun_scope. @@ -2327,7 +2325,7 @@ Qed. End Induced. -Arguments cfInd _ _%g _%g _%CF. +Arguments cfInd {gT} B%g {A%g} phi%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. @@ -2489,7 +2487,7 @@ End FieldAutomorphism. Arguments cfAutK u {gT G}. Arguments cfAutVK u {gT G}. -Arguments cfAut_inj u [gT G x1 x2]. +Arguments cfAut_inj u {gT G} [phi1 phi2] : rename. Definition conj_cfRes := cfAutRes conjC. Definition cfker_conjC := cfker_aut conjC. diff --git a/mathcomp/character/inertia.v b/mathcomp/character/inertia.v index ffa9696..80d5cc5 100644 --- a/mathcomp/character/inertia.v +++ b/mathcomp/character/inertia.v @@ -567,9 +567,9 @@ Qed. End Inertia. -Arguments inertia _ _%g _%CF. -Arguments cfclass _ _%g _%CF _%g. -Arguments conjg_Iirr_inj [gT H] y [x1 x2]. +Arguments inertia {gT B%g} phi%CF. +Arguments cfclass {gT A%g} phi%CF B%g. +Arguments conjg_Iirr_inj {gT H} y [i1 i2] : rename. Notation "''I[' phi ] " := (inertia phi) : group_scope. Notation "''I[' phi ] " := (inertia_group phi) : Group_scope. diff --git a/mathcomp/character/integral_char.v b/mathcomp/character/integral_char.v index f0553f2..3c2b0d6 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 gring_irr_mode _ _%G _%R _%g : extra scopes. +Arguments gring_irr_mode {gT G%G} i%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 b121f4c..69055d4 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 rowg_mx _ _ _%g. +Arguments rowg_mx {F n%N} L%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 abelem_dim' _ _%g. +Arguments abelem_dim' {gT} E%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 6859168..560b61d 100644 --- a/mathcomp/character/mxrepresentation.v +++ b/mathcomp/character/mxrepresentation.v @@ -814,10 +814,10 @@ End Regular. End RingRepr. -Arguments mx_representation _ _ _%g _%N. -Arguments mx_repr _ _ _%g _%N _. -Arguments group_ring _ _ _%g. -Arguments regular_repr _ _ _%g. +Arguments mx_representation R {gT} G%g n%N. +Arguments mx_repr {R gT} G%g {n%N} r. +Arguments group_ring R {gT} G%g. +Arguments regular_repr R {gT} G%g. Arguments centgmxP {R gT G n rG f}. Arguments rkerP {R gT G n rG x}. @@ -2377,8 +2377,8 @@ Arguments mxsimple_isoP {gT G n rG U V}. Arguments socleP {gT G n rG sG0 W W'}. Arguments mx_abs_irrP {gT G n rG}. -Arguments val_submod_inj {n U m}. -Arguments val_factmod_inj {n U m}. +Arguments val_submod_inj {n U m} [W1 W2] : rename. +Arguments val_factmod_inj {n U m} [W1 W2] : rename. Section Proper. @@ -4652,10 +4652,10 @@ End LinearIrr. End FieldRepr. -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 rfix_mx {F gT G%g n%N} rG H%g. +Arguments gset_mx F {gT} G%g A%g. +Arguments classg_base F {gT} G%g _%g : extra scopes. +Arguments irrType F {gT} G%g. Arguments mxmoduleP {F gT G n rG m U}. Arguments envelop_mxP {F gT G n rG A}. @@ -4671,16 +4671,16 @@ Arguments socleP {F gT G n rG sG0 W W'}. Arguments mx_abs_irrP {F gT G n rG}. Arguments socle_rsimP {F gT G n rG sG W1 W2}. -Arguments val_submod_inj {F n U m}. -Arguments val_factmod_inj {F n U m}. +Arguments val_submod_inj {F n U m} [W1 W2] : rename. +Arguments val_factmod_inj {F n U m} [W1 W2] : rename. Notation "'Cl" := (Clifford_action _) : action_scope. Bind Scope irrType_scope with socle_sort. Notation "[ 1 sG ]" := (principal_comp sG) : irrType_scope. -Arguments irr_degree _ _ _%G _ _%irr. -Arguments irr_repr _ _ _%G _ _%irr _%g : extra scopes. -Arguments irr_mode _ _ _%G _ _%irr _%g : extra scopes. +Arguments irr_degree {F gT G%G sG} i%irr. +Arguments irr_repr [F gT G%G sG] i%irr _%g : extra scopes. +Arguments irr_mode [F gT G%G sG] i%irr z%g : rename. 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. |