diff options
| author | Cyril Cohen | 2020-04-09 16:39:37 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2020-04-15 14:20:45 +0200 |
| commit | 6dac040b009e10bc4fa0420f7c40ae9134594c86 (patch) | |
| tree | cea15b6018d326b9fc106a37e837aa49c970af5b /mathcomp/fingroup/action.v | |
| parent | 710a449fad7132a6ac89d19159fda44e48718b1d (diff) | |
reworked new lemmas in perm and action and added missing ones
In particular: rephrased permS0 and permS1 with all_equal_to
Diffstat (limited to 'mathcomp/fingroup/action.v')
| -rw-r--r-- | mathcomp/fingroup/action.v | 19 |
1 files changed, 8 insertions, 11 deletions
diff --git a/mathcomp/fingroup/action.v b/mathcomp/fingroup/action.v index 9631d28..2d1b6e6 100644 --- a/mathcomp/fingroup/action.v +++ b/mathcomp/fingroup/action.v @@ -1682,13 +1682,11 @@ Proof. exact: im_perm_on (restr_perm_on p). Qed. Lemma restr_perm_commute s : commute (restr_perm s) s. Proof. -case: (boolP (s \in 'N(S | 'P))) => - [HC | /triv_restr_perm ->]; last exact: (commute_sym (commute1 _)). -apply/permP => x; case: (boolP (x \in S)) => Hx; rewrite !permM. -- by rewrite !restr_permE //; move: HC => /astabsP/(_ x)/= ->. -- have:= restr_perm_on s => /out_perm Hout. - rewrite (Hout _ Hx) {}Hout //. - by move: Hx; apply contra; move: HC => /astabsP/(_ x)/= ->. +have [sC|/triv_restr_perm->] := boolP (s \in 'N(S | 'P)); last first. + exact: (commute_sym (commute1 _)). +apply/permP => x; have /= xsS := astabsP sC x; rewrite !permM. +have [xS|xNS] := boolP (x \in S); first by rewrite ?(restr_permE) ?xsS. +by rewrite !(out_perm (restr_perm_on _)) ?xsS. Qed. End RestrictPerm. @@ -1699,10 +1697,9 @@ Variables (T : finType) (S : {set T}). Lemma SymE : Sym S = 'C(~: S | 'P). Proof. -apply/setP => s; rewrite inE; apply/idP/astabP => [Hperm x | Hstab]. -- by rewrite inE /= apermE => /out_perm; apply. -- apply/subsetP => x; rewrite unfold_in; apply contraR => H. - by move/(_ x): Hstab; rewrite inE /= apermE => ->. +apply/setP => s; rewrite inE; apply/idP/astabP => [sS x|/= S_id]. + by rewrite inE /= apermE => /out_perm->. +by apply/subsetP => x; move=> /(contra_neqN (S_id _)); rewrite inE negbK. Qed. End Symmetry. |