diff options
Diffstat (limited to 'mathcomp/fingroup')
| -rw-r--r-- | mathcomp/fingroup/action.v | 32 | ||||
| -rw-r--r-- | mathcomp/fingroup/automorphism.v | 4 | ||||
| -rw-r--r-- | mathcomp/fingroup/fingroup.v | 76 | ||||
| -rw-r--r-- | mathcomp/fingroup/gproduct.v | 14 | ||||
| -rw-r--r-- | mathcomp/fingroup/morphism.v | 35 | ||||
| -rw-r--r-- | mathcomp/fingroup/perm.v | 4 | ||||
| -rw-r--r-- | mathcomp/fingroup/quotient.v | 5 |
7 files changed, 78 insertions, 92 deletions
diff --git a/mathcomp/fingroup/action.v b/mathcomp/fingroup/action.v index 5c5dcdc..ffea847 100644 --- a/mathcomp/fingroup/action.v +++ b/mathcomp/fingroup/action.v @@ -488,10 +488,9 @@ Arguments act_inj {aT D rT} to _ [x1 x2]. Notation "to ^*" := (set_action to) : action_scope. -Arguments orbitP [aT D rT to A x y]. -Arguments afixP [aT D rT to A x]. -Arguments afix1P [aT D rT to a x]. -Prenex Implicits orbitP afixP afix1P. +Arguments orbitP {aT D rT to A x y}. +Arguments afixP {aT D rT to A x}. +Arguments afix1P {aT D rT to a x}. Arguments reindex_astabs [aT D rT] to [vT idx op S] a [F]. Arguments reindex_acts [aT D rT] to [vT idx op S A a F]. @@ -876,10 +875,9 @@ Qed. End PartialAction. Arguments orbit_transversal _ _%g _ _%act _%g _%g. -Arguments orbit_in_eqP [aT D rT to G x y]. -Arguments orbit1P [aT D rT to G x]. +Arguments orbit_in_eqP {aT D rT to G x y}. +Arguments orbit1P {aT D rT to G x}. Arguments contra_orbit [aT D rT] to G [x y]. -Prenex Implicits orbit_in_eqP orbit1P. Notation "''C' ( S | to )" := (astab_group to S) : Group_scope. Notation "''C_' A ( S | to )" := (setI_group A 'C(S | to)) : Group_scope. @@ -1005,7 +1003,7 @@ Proof. apply: (iffP idP) => [nSA x|nSA]; first exact: acts_act. by apply/subsetP=> a Aa; rewrite !inE; apply/subsetP=> x; rewrite inE nSA. Qed. -Arguments actsP [A S]. +Arguments actsP {A S}. Lemma setact_orbit A x b : to^* (orbit to A x) b = orbit to (A :^ b) (to x b). Proof. @@ -1134,14 +1132,13 @@ Qed. End TotalActions. -Arguments astabP [aT rT to S a]. -Arguments orbit_eqP [aT rT to G x y]. -Arguments astab1P [aT rT to x a]. -Arguments astabsP [aT rT to S a]. -Arguments atransP [aT rT to G S]. -Arguments actsP [aT rT to A S]. -Arguments faithfulP [aT rT to A S]. -Prenex Implicits astabP orbit_eqP astab1P astabsP atransP actsP faithfulP. +Arguments astabP {aT rT to S a}. +Arguments orbit_eqP {aT rT to G x y}. +Arguments astab1P {aT rT to x a}. +Arguments astabsP {aT rT to S a}. +Arguments atransP {aT rT to G S}. +Arguments actsP {aT rT to A S}. +Arguments faithfulP {aT rT to A S}. Section Restrict. @@ -1634,8 +1631,7 @@ Proof. by apply/permP=> x; rewrite permE. Qed. End PermAction. -Arguments perm_act1P [rT a]. -Prenex Implicits perm_act1P. +Arguments perm_act1P {rT a}. Notation "'P" := (perm_action _) (at level 8) : action_scope. diff --git a/mathcomp/fingroup/automorphism.v b/mathcomp/fingroup/automorphism.v index b1c9d94..320331c 100644 --- a/mathcomp/fingroup/automorphism.v +++ b/mathcomp/fingroup/automorphism.v @@ -198,8 +198,8 @@ Qed. End MakeAut. -Arguments morphim_fixP [gT G f]. -Prenex Implicits aut morphim_fixP. +Arguments morphim_fixP {gT G f}. +Prenex Implicits aut. Section AutIsom. diff --git a/mathcomp/fingroup/fingroup.v b/mathcomp/fingroup/fingroup.v index 959eea1..1165a33 100644 --- a/mathcomp/fingroup/fingroup.v +++ b/mathcomp/fingroup/fingroup.v @@ -493,8 +493,8 @@ Qed. End PreGroupIdentities. Hint Resolve commute1. -Arguments invg_inj [T]. -Prenex Implicits commute invgK invg_inj. +Arguments invg_inj {T}. +Prenex Implicits commute invgK. Section GroupIdentities. @@ -644,9 +644,8 @@ Definition gnorm := (gsimp, (mulgK, mulgKV, (mulgA, invMg))). Arguments mulgI [T]. Arguments mulIg [T]. Arguments conjg_inj [T]. -Arguments commgP [T x y]. -Arguments conjg_fixP [T x y]. -Prenex Implicits conjg_fixP commgP. +Arguments commgP {T x y}. +Arguments conjg_fixP {T x y}. Section Repr. (* Plucking a set representative. *) @@ -945,9 +944,9 @@ Proof. by apply/setP=> y; rewrite !inE inv_eq //; apply: invgK. Qed. End BaseSetMulProp. -Arguments set1gP [gT x]. -Arguments mulsgP [gT A B x]. -Arguments prodsgP [gT I P A x]. +Arguments set1gP {gT x}. +Arguments mulsgP {gT A B x}. +Arguments prodsgP {gT I P A x}. Section GroupSetMulProp. (* Constructs that need a finGroupType *) @@ -1303,13 +1302,12 @@ Definition order x := #|cycle x|. End GroupSetMulProp. -Arguments lcosetP [gT A x y]. -Arguments lcosetsP [gT A B C]. -Arguments rcosetP [gT A x y]. -Arguments rcosetsP [gT A B C]. -Arguments group_setP [gT A]. +Arguments lcosetP {gT A x y}. +Arguments lcosetsP {gT A B C}. +Arguments rcosetP {gT A x y}. +Arguments rcosetsP {gT A B C}. +Arguments group_setP {gT A}. Prenex Implicits group_set mulsgP set1gP. -Prenex Implicits lcosetP lcosetsP rcosetP rcosetsP group_setP. Arguments commutator _ _%g _%g. Arguments joing _ _%g _%g. @@ -1857,16 +1855,15 @@ Notation "[ 'subg' G ]" := [set: subg_of G]%G : Group_scope. Prenex Implicits subg sgval subg_of. Bind Scope group_scope with subg_of. -Arguments trivgP [gT G]. -Arguments trivGP [gT G]. -Arguments lcoset_eqP [gT G x y]. -Arguments rcoset_eqP [gT G x y]. +Arguments trivgP {gT G}. +Arguments trivGP {gT G}. +Arguments lcoset_eqP {gT G x y}. +Arguments rcoset_eqP {gT G x y}. Arguments mulGidPl [gT G H]. Arguments mulGidPr [gT G H]. -Arguments comm_group_setP [gT G H]. -Arguments class_eqP [gT G x y]. -Arguments repr_classesP [gT G xG]. -Prenex Implicits trivgP trivGP lcoset_eqP rcoset_eqP comm_group_setP class_eqP. +Arguments comm_group_setP {gT G H}. +Arguments class_eqP {gT G x y}. +Arguments repr_classesP {gT G xG}. Section GroupInter. @@ -2395,11 +2392,11 @@ Qed. End GeneratedGroup. -Arguments gen_prodgP [gT A x]. -Arguments joing_idPl [gT G A]. -Arguments joing_idPr [gT A G]. -Arguments mulGsubP [gT K H G]. -Arguments joing_subP [gT A B G]. +Arguments gen_prodgP {gT A x}. +Arguments joing_idPl {gT G A}. +Arguments joing_idPr {gT A G}. +Arguments mulGsubP {gT K H G}. +Arguments joing_subP {gT A B G}. Section Cycles. @@ -2523,7 +2520,7 @@ Proof. suffices ->: (x \in 'N(A)) = (A :^ x == A) by apply: eqP. by rewrite eqEcard cardJg leqnn andbT inE. Qed. -Arguments normP [x A]. +Arguments normP {x A}. Lemma group_set_normaliser A : group_set 'N(A). Proof. @@ -2538,7 +2535,7 @@ Proof. apply: (iffP subsetP) => nBA x Ax; last by rewrite inE nBA //. by apply/normP; apply: nBA. Qed. -Arguments normsP [A B]. +Arguments normsP {A B}. Lemma memJ_norm x y A : x \in 'N(A) -> (y ^ x \in A) = (y \in A). Proof. by move=> Nx; rewrite -{1}(normP Nx) memJ_conjg. Qed. @@ -2986,15 +2983,13 @@ End SubAbelian. End Normaliser. -Arguments normP [gT x A]. -Arguments centP [gT A x]. -Arguments normsP [gT A B]. -Arguments cent1P [gT x y]. -Arguments normalP [gT A B]. -Arguments centsP [gT A B]. -Arguments commG1P [gT A B]. - -Prenex Implicits normP normsP cent1P normalP centP centsP commG1P. +Arguments normP {gT x A}. +Arguments centP {gT A x}. +Arguments normsP {gT A B}. +Arguments cent1P {gT x y}. +Arguments normalP {gT A B}. +Arguments centsP {gT A B}. +Arguments commG1P {gT A B}. Arguments normaliser_group _ _%g. Arguments centraliser_group _ _%g. @@ -3090,6 +3085,5 @@ Notation "[ 'min' A 'of' G | gP & gQ ]" := [min A of G | gP && gQ] : group_scope. Notation "[ 'min' G | gP & gQ ]" := [min G | gP && gQ] : group_scope. -Arguments mingroupP [gT gP G]. -Arguments maxgroupP [gT gP G]. -Prenex Implicits mingroupP maxgroupP. +Arguments mingroupP {gT gP G}. +Arguments maxgroupP {gT gP G}. diff --git a/mathcomp/fingroup/gproduct.v b/mathcomp/fingroup/gproduct.v index 986489b..22c19d4 100644 --- a/mathcomp/fingroup/gproduct.v +++ b/mathcomp/fingroup/gproduct.v @@ -867,11 +867,11 @@ Qed. End InternalProd. -Arguments complP [gT H A B]. -Arguments splitsP [gT B A]. -Arguments sdprod_normal_complP [gT G K H]. -Arguments dprodYP [gT K H]. -Arguments bigdprodYP [gT I P F]. +Arguments complP {gT H A B}. +Arguments splitsP {gT B A}. +Arguments sdprod_normal_complP {gT G K H}. +Arguments dprodYP {gT K H}. +Arguments bigdprodYP {gT I P F}. Section MorphimInternalProd. @@ -1700,5 +1700,5 @@ Qed. End DirprodIsom. -Arguments mulgmP [gT H1 H2 G]. -Prenex Implicits mulgm mulgmP. +Arguments mulgmP {gT H1 H2 G}. +Prenex Implicits mulgm. diff --git a/mathcomp/fingroup/morphism.v b/mathcomp/fingroup/morphism.v index 3c23921..4b2d863 100644 --- a/mathcomp/fingroup/morphism.v +++ b/mathcomp/fingroup/morphism.v @@ -118,9 +118,8 @@ Notation "[ 'morphism' D 'of' f ]" := Notation "[ 'morphism' 'of' f ]" := (clone_morphism (@Morphism _ _ _ f)) (at level 0, format "[ 'morphism' 'of' f ]") : form_scope. -Arguments morphimP [aT rT D A y f]. -Arguments morphpreP [aT rT D R x f]. -Prenex Implicits morphimP morphpreP. +Arguments morphimP {aT rT D A y f}. +Arguments morphpreP {aT rT D R x f}. (* Domain, image, preimage, kernel, using phantom types to infer the domain. *) @@ -873,7 +872,7 @@ Notation "f @* G" := (morphim_group (MorPhantom f) G) : Group_scope. Notation "f @*^-1 M" := (morphpre_group (MorPhantom f) M) : Group_scope. Notation "f @: D" := (morph_dom_group f D) : Group_scope. -Arguments injmP [aT rT D f]. +Arguments injmP {aT rT D f}. Section IdentityMorphism. @@ -908,8 +907,7 @@ Proof. exact: morphim_idm. Qed. End IdentityMorphism. -Arguments idm _ _%g _%g. -Prenex Implicits idm. +Arguments idm {_} _%g _%g. Section RestrictedMorphism. @@ -967,10 +965,9 @@ Proof. by move <-; exists f. Qed. End RestrictedMorphism. -Arguments restrm _ _ _%g _%g _ _%g. -Prenex Implicits restrm. -Arguments restrmP [aT rT A D]. -Arguments domP [aT rT A D]. +Arguments restrm {_ _ _%g _%g} _ _%g. +Arguments restrmP {aT rT A D}. +Arguments domP {aT rT A D}. Section TrivMorphism. @@ -1324,17 +1321,17 @@ Proof. exact: restr_isom_to. Qed. End ReflectProp. -Arguments isom _ _ _%g _%g _. -Arguments morphic _ _ _%g _. +Arguments isom {_ _} _%g _%g _. +Arguments morphic {_ _} _%g _. Arguments misom _ _ _%g _%g _. -Arguments isog _ _ _%g _%g. +Arguments isog {_ _} _%g _%g. -Arguments morphicP [aT rT A f]. -Arguments misomP [aT rT A B f]. +Arguments morphicP {aT rT A f}. +Arguments misomP {aT rT A B f}. Arguments isom_isog [aT rT A B D]. -Arguments isomP [aT rT G H f]. -Arguments isogP [aT rT G H]. -Prenex Implicits morphic morphicP morphm isom isog isomP misomP isogP. +Arguments isomP {aT rT G H f}. +Arguments isogP {aT rT G H}. +Prenex Implicits morphm. Notation "x \isog y":= (isog x y). Section Isomorphisms. @@ -1482,7 +1479,7 @@ Arguments homg _ _ _%g _%g. Notation "G \homg H" := (homg G H) (at level 70, no associativity) : group_scope. -Arguments homgP [rT aT C D]. +Arguments homgP {rT aT C D}. (* Isomorphism between a group and its subtype. *) diff --git a/mathcomp/fingroup/perm.v b/mathcomp/fingroup/perm.v index 3edcfed..01ef08e 100644 --- a/mathcomp/fingroup/perm.v +++ b/mathcomp/fingroup/perm.v @@ -461,7 +461,7 @@ Lemma odd_tperm x y : odd_perm (tperm x y) = (x != y). Proof. by rewrite -[_ y]mulg1 odd_mul_tperm odd_perm1 addbF. Qed. Definition dpair (eT : eqType) := [pred t | t.1 != t.2 :> eT]. -Arguments dpair [eT]. +Arguments dpair {eT}. Lemma prod_tpermP s : {ts : seq (T * T) | s = \prod_(t <- ts) tperm t.1 t.2 & all dpair ts}. @@ -503,7 +503,7 @@ Proof. by rewrite !odd_permM odd_permV addbC addbK. Qed. End PermutationParity. Coercion odd_perm : perm_type >-> bool. -Arguments dpair [eT]. +Arguments dpair {eT}. Prenex Implicits pcycle dpair pcycles aperm. Section LiftPerm. diff --git a/mathcomp/fingroup/quotient.v b/mathcomp/fingroup/quotient.v index 03c55b3..322fc4e 100644 --- a/mathcomp/fingroup/quotient.v +++ b/mathcomp/fingroup/quotient.v @@ -198,10 +198,9 @@ Lemma quotientE : quotient = coset @* Q. Proof. by []. Qed. End Cosets. -Arguments coset_of _ _%g. -Arguments coset _ _%g _%g. +Arguments coset_of {_} _%g. +Arguments coset {_} _%g _%g. Arguments quotient _ _%g _%g. -Prenex Implicits coset_of coset. Bind Scope group_scope with coset_of. |