diff options
Diffstat (limited to 'mathcomp/fingroup/perm.v')
| -rw-r--r-- | mathcomp/fingroup/perm.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/mathcomp/fingroup/perm.v b/mathcomp/fingroup/perm.v index 6d9abdc..bbf4363 100644 --- a/mathcomp/fingroup/perm.v +++ b/mathcomp/fingroup/perm.v @@ -128,7 +128,7 @@ Proof. by move=> x; rewrite -pvalE [@perm]unlock ffunE. Qed. Lemma perm_inj s : injective s. Proof. by rewrite -!pvalE; apply: (injectiveP _ (valP s)). Qed. -Implicit Arguments perm_inj []. +Arguments perm_inj : clear implicits. Hint Resolve perm_inj. Lemma perm_onto s : codom s =i predT. @@ -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]. -Implicit 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. -Implicit Arguments dpair [eT]. +Arguments dpair [eT]. Prenex Implicits pcycle dpair pcycles aperm. Section LiftPerm. |