diff options
| author | Cyril Cohen | 2019-04-08 14:17:42 +0200 |
|---|---|---|
| committer | GitHub | 2019-04-08 14:17:42 +0200 |
| commit | 8099c05ca650b12abd0fbaf676357e86fd175a8a (patch) | |
| tree | a5b3a73bd05ae1a81261de7b33d0cfba750e95cb /mathcomp/solvable | |
| parent | 6e0a9a6ad6d5022e1214a4f38348e3a8f82d45a2 (diff) | |
| parent | c0254eaba338a4d308b4e2f200841ff76e6b4b9a (diff) | |
Merge pull request #324 from math-comp/seq-permutations-allpairs
Seq refactoring; adding `permutations`, extending `allpairs`
Diffstat (limited to 'mathcomp/solvable')
| -rw-r--r-- | mathcomp/solvable/primitive_action.v | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/mathcomp/solvable/primitive_action.v b/mathcomp/solvable/primitive_action.v index fa27e75..73e397d 100644 --- a/mathcomp/solvable/primitive_action.v +++ b/mathcomp/solvable/primitive_action.v @@ -165,10 +165,8 @@ Definition ntransitive := [transitive A, on dtuple_on | to * n]. Lemma dtuple_onP t : reflect (injective (tnth t) /\ forall i, tnth t i \in S) (t \in dtuple_on). Proof. -rewrite inE subset_all -map_tnth_enum. -case: (uniq _) / (injectiveP (tnth t)) => f_inj; last by right; case. -rewrite -[all _ _]negbK -has_predC has_map has_predC negbK /=. -by apply: (iffP allP) => [Sf|[]//]; split=> // i; rewrite Sf ?mem_enum. +rewrite inE subset_all -forallb_tnth -[in uniq t]map_tnth_enum /=. +by apply: (iffP andP) => -[/injectiveP-f_inj /forallP]. Qed. Lemma n_act_dtuple t a : |