diff options
Diffstat (limited to 'mathcomp/fingroup')
| -rw-r--r-- | mathcomp/fingroup/action.v | 26 | ||||
| -rw-r--r-- | mathcomp/fingroup/fingroup.v | 4 | ||||
| -rw-r--r-- | mathcomp/fingroup/gproduct.v | 12 |
3 files changed, 21 insertions, 21 deletions
diff --git a/mathcomp/fingroup/action.v b/mathcomp/fingroup/action.v index 1bde1f7..ecfa6ea 100644 --- a/mathcomp/fingroup/action.v +++ b/mathcomp/fingroup/action.v @@ -380,14 +380,14 @@ apply/subsetP=> a cSa; rewrite !inE (astab_dom cSa). by apply/subsetP=> x Sx; rewrite inE (astab_act cSa). Qed. -Lemma astabsC S : 'N(~: S | to) = 'N(S | to). +Lemma astabsC S : 'N(~: S | to) = 'N(S | to). Proof. apply/setP=> a; apply/idP/idP=> nSa; rewrite !inE (astabs_dom nSa). by rewrite -setCS -preimsetC; apply/subsetP=> x; rewrite inE astabs_act. by rewrite preimsetC setCS; apply/subsetP=> x; rewrite inE astabs_act. Qed. -Lemma astabsI S T : 'N(S | to) :&: 'N(T | to) \subset 'N(S :&: T | to). +Lemma astabsI S T : 'N(S | to) :&: 'N(T | to) \subset 'N(S :&: T | to). Proof. apply/subsetP=> a; rewrite !inE -!andbA preimsetI => /and4P[-> nSa _ nTa] /=. by rewrite setISS. @@ -425,7 +425,7 @@ Proof. move=> sAD; apply/subsetP/subsetP=> [sAC x xS | sSF a aA]. by apply/afixP=> a aA; apply: astab_act (sAC _ aA) xS. rewrite !inE (subsetP sAD _ aA); apply/subsetP=> x xS. -by move/afixP/(_ _ aA): (sSF _ xS); rewrite inE => ->. +by move/afixP/(_ _ aA): (sSF _ xS); rewrite inE => ->. Qed. Section ActsSetop. @@ -436,12 +436,12 @@ Hypotheses (AactS : [acts A, on S | to]) (AactT : [acts A, on T | to]). Lemma astabU : 'C(S :|: T | to) = 'C(S | to) :&: 'C(T | to). Proof. by apply/setP=> a; rewrite !inE subUset; case: (a \in D). Qed. -Lemma astabsU : 'N(S | to) :&: 'N(T | to) \subset 'N(S :|: T | to). +Lemma astabsU : 'N(S | to) :&: 'N(T | to) \subset 'N(S :|: T | to). Proof. by rewrite -(astabsC S) -(astabsC T) -(astabsC (S :|: T)) setCU astabsI. Qed. -Lemma astabsD : 'N(S | to) :&: 'N(T | to) \subset 'N(S :\: T| to). +Lemma astabsD : 'N(S | to) :&: 'N(T | to) \subset 'N(S :\: T| to). Proof. by rewrite setDE -(astabsC T) astabsI. Qed. Lemma actsI : [acts A, on S :&: T | to]. @@ -680,13 +680,13 @@ Proof. by move=> Da; rewrite afix_gen_in ?sub1set. Qed. Lemma afixYin A B : A \subset D -> B \subset D -> 'Fix_to(A <*> B) = 'Fix_to(A) :&: 'Fix_to(B). -Proof. by move=> sAD sBD; rewrite afix_gen_in ?afixU // subUset sAD. Qed. +Proof. by move=> sAD sBD; rewrite afix_gen_in ?afixU // subUset sAD. Qed. Lemma afixMin G H : G \subset D -> H \subset D -> 'Fix_to(G * H) = 'Fix_to(G) :&: 'Fix_to(H). Proof. by move=> sGD sHD; rewrite -afix_gen_in ?mul_subG // genM_join afixYin. -Qed. +Qed. Lemma sub_astab1_in A x : A \subset D -> (A \subset 'C[x | to]) = (x \in 'Fix_to(A)). @@ -952,7 +952,7 @@ Proof. exact: sameP eqP (orbit_eqP G x y). Qed. Lemma orbit_inv A x y : (y \in orbit to A^-1 x) = (x \in orbit to A y). Proof. by rewrite orbit_inv_in ?subsetT. Qed. -Lemma orbit_lcoset A a x : orbit to (a *: A) x = orbit to A (to x a). +Lemma orbit_lcoset A a x : orbit to (a *: A) x = orbit to A (to x a). Proof. by rewrite orbit_lcoset_in ?subsetT ?inE. Qed. Lemma orbit_rcoset A a x y : @@ -1910,7 +1910,7 @@ Lemma gacentIim : 'C_(R | to)(A) = 'C_(|to)(A). Proof. by rewrite setIA setIid. Qed. Lemma gacentS : A \subset B -> 'C_(|to)(B) \subset 'C_(|to)(A). -Proof. by move=> sAB; rewrite !(setIS, afixS). Qed. +Proof. by move=> sAB; rewrite !(setIS, afixS). Qed. Lemma gacentU : 'C_(|to)(A :|: B) = 'C_(|to)(A) :&: 'C_(|to)(B). Proof. by rewrite -setIIr -afixU -setIUr. Qed. @@ -2001,8 +2001,8 @@ by move=> sGD sHB; rewrite -gacent_gen ?mul_subG // genM_join gacentY. Qed. Lemma astab1 : 'C(1 | to) = D. -Proof. -by apply/setP=> x; rewrite ?(inE, sub1set) andb_idr //; move/gact1=> ->. +Proof. +by apply/setP=> x; rewrite ?(inE, sub1set) andb_idr //; move/gact1=> ->. Qed. Lemma astab_range : 'C(R | to) = 'C(setT | to). @@ -2599,10 +2599,10 @@ Lemma actsQ A B H : A \subset 'N(H) -> A \subset 'N(B) -> [acts A, on B / H | 'Q]. Proof. by move=> nHA nBA; rewrite acts_quotient // subsetI dom_qactJ nHA astabsJ. -Qed. +Qed. Lemma astabsQ G H : H <| G -> 'N(G / H | 'Q) = 'N(H) :&: 'N(G). -Proof. by move=> nsHG; rewrite astabs_quotient // dom_qactJ astabsJ. Qed. +Proof. by move=> nsHG; rewrite astabs_quotient // dom_qactJ astabsJ. Qed. Lemma astabQ H Abar : 'C(Abar |'Q) = coset H @*^-1 'C(Abar). Proof. diff --git a/mathcomp/fingroup/fingroup.v b/mathcomp/fingroup/fingroup.v index 9d7bcc8..dd57af4 100644 --- a/mathcomp/fingroup/fingroup.v +++ b/mathcomp/fingroup/fingroup.v @@ -1163,7 +1163,7 @@ move=> Ax; apply/setP=> y. by apply/imsetP/set1P=> [[a Aa]|] ->; last exists x; rewrite ?conj1g. Qed. -Lemma classVg x A : x^-1 ^: A = (x ^: A)^-1. +Lemma classVg x A : x^-1 ^: A = (x ^: A)^-1. Proof. apply/setP=> xy; rewrite inE; apply/imsetP/imsetP=> [] [y Ay def_xy]. by rewrite def_xy conjVg invgK; exists y. @@ -2661,7 +2661,7 @@ Lemma norms_class_support : A \subset 'N(class_support B C). Proof. apply/subsetP=> x Ax; rewrite inE sub_conjg class_supportEr. apply/bigcupsP=> y Cy; rewrite -sub_conjg -conjsgM conjgC conjsgM. -by rewrite (normsP nBA) // bigcup_sup ?memJ_norm ?(subsetP nCA). +by rewrite (normsP nBA) // bigcup_sup ?memJ_norm ?(subsetP nCA). Qed. End norm_trans. diff --git a/mathcomp/fingroup/gproduct.v b/mathcomp/fingroup/gproduct.v index 94304c4..cd129f2 100644 --- a/mathcomp/fingroup/gproduct.v +++ b/mathcomp/fingroup/gproduct.v @@ -524,7 +524,7 @@ Lemma bigcprodWY I (r : seq I) P F G : \big[cprod/1]_(i <- r | P i) F i = G -> << \bigcup_(i <- r | P i) F i >> = G. Proof. elim/big_rec2: _ G => [|i A B _ IH G]; first by rewrite gen0. -case /cprodP => [[K H -> defB] <- cKH]. +case/cprodP => [[K H -> defB] <- cKH]. by rewrite -[<<_>>]joing_idr (IH H) ?cent_joinEr -?defB. Qed. @@ -1034,7 +1034,7 @@ Proof. by move=> x y. Qed. Canonical fst_morphism := @Morphism _ _ setT _ (in2W fst_morphM). -Canonical snd_morphism := @Morphism _ _ setT _ (in2W snd_morphM). +Canonical snd_morphism := @Morphism _ _ setT _ (in2W snd_morphM). Lemma injm_pair1g : 'injm pair1g. Proof. by apply/subsetP=> x /morphpreP[_ /set1P[->]]; apply: set11. Qed. @@ -1052,7 +1052,7 @@ Lemma morphim_fstX (H1: {set gT1}) (H2 : {group gT2}) : [morphism of fun x => x.1] @* setX H1 H2 = H1. Proof. apply/eqP; rewrite eqEsubset morphimE setTI /=. -apply/andP; split; apply/subsetP=> x. +apply/andP; split; apply/subsetP=> x. by case/imsetP=> x0; rewrite inE; move/andP=> [Hx1 _] ->. move=> Hx1; apply/imsetP; exists (x, 1); last by trivial. by rewrite in_setX Hx1 /=. @@ -1062,9 +1062,9 @@ Lemma morphim_sndX (H1: {group gT1}) (H2 : {set gT2}) : [morphism of fun x => x.2] @* setX H1 H2 = H2. Proof. apply/eqP; rewrite eqEsubset morphimE setTI /=. -apply/andP; split; apply/subsetP=> x. +apply/andP; split; apply/subsetP=> x. by case/imsetP=> x0; rewrite inE; move/andP=> [_ Hx2] ->. -move=>Hx2; apply/imsetP; exists (1, x); last by []. +move=> Hx2; apply/imsetP; exists (1, x); last by []. by rewrite in_setX Hx2 andbT. Qed. @@ -1084,7 +1084,7 @@ Lemma setX_dprod (H1 : {group gT1}) (H2 : {group gT2}) : Proof. rewrite dprodE ?setX_prod //. apply/centsP=> [[x u]]; rewrite !inE /= => /andP[/eqP-> _] [v y]. - by rewrite !inE /= => /andP[_ /eqP->]; congr (_, _); rewrite ?mul1g ?mulg1. + by rewrite !inE /= => /andP[_ /eqP->]; congr (_, _); rewrite ?mul1g ?mulg1. apply/trivgP; apply/subsetP=> [[x y]]; rewrite !inE /= -!andbA. by case/and4P=> _ /eqP-> /eqP->; rewrite eqxx. Qed. |