From 748d716efb2f2f75946c8386e441ce1789806a39 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 22 May 2019 13:43:08 +0200 Subject: htmldoc regenerated --- docs/htmldoc/mathcomp.fingroup.gproduct.html | 727 +++++++++++++-------------- 1 file changed, 363 insertions(+), 364 deletions(-) (limited to 'docs/htmldoc/mathcomp.fingroup.gproduct.html') diff --git a/docs/htmldoc/mathcomp.fingroup.gproduct.html b/docs/htmldoc/mathcomp.fingroup.gproduct.html index 7670d1a..7636563 100644 --- a/docs/htmldoc/mathcomp.fingroup.gproduct.html +++ b/docs/htmldoc/mathcomp.fingroup.gproduct.html @@ -21,7 +21,6 @@
(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  
 Distributed under the terms of CeCILL-B.                                  *)
-Require Import mathcomp.ssreflect.ssreflect.

@@ -86,31 +85,31 @@
Variables gT : finGroupType.
-Implicit Types A B C : {set gT}.
+Implicit Types A B C : {set gT}.

Definition partial_product A B :=
-  if A == 1 then B else if B == 1 then A else
-  if [&& group_set A, group_set B & B \subset 'N(A)] then A × B else set0.
+  if A == 1 then B else if B == 1 then A else
+  if [&& group_set A, group_set B & B \subset 'N(A)] then A × B else set0.

Definition semidirect_product A B :=
-  if A :&: B \subset 1%G then partial_product A B else set0.
+  if A :&: B \subset 1%G then partial_product A B else set0.

Definition central_product A B :=
-  if B \subset 'C(A) then partial_product A B else set0.
+  if B \subset 'C(A) then partial_product A B else set0.

Definition direct_product A B :=
-  if A :&: B \subset 1%G then central_product A B else set0.
+  if A :&: B \subset 1%G then central_product A B else set0.

Definition complements_to_in A B :=
-  [set K : {group gT} | A :&: K == 1 & A × K == B].
+  [set K : {group gT} | A :&: K == 1 & A × K == B].

-Definition splits_over B A := complements_to_in A B != set0.
+Definition splits_over B A := complements_to_in A B != set0.

@@ -119,8 +118,8 @@ Product remainder functions -- right variant only.
-Definition remgr A B x := repr (A :* x :&: B).
-Definition divgr A B x := x × (remgr A B x)^-1.
+Definition remgr A B x := repr (A :* x :&: B).
+Definition divgr A B x := x × (remgr A B x)^-1.

End Defs.
@@ -132,16 +131,16 @@ Notation dprod := (direct_product _).

-Notation "G ><| H" := (sdprod G H)%g (at level 40, left associativity).
-Notation "G \* H" := (cprod G H)%g (at level 40, left associativity).
-Notation "G \x H" := (dprod G H)%g (at level 40, left associativity).
+Notation "G ><| H" := (sdprod G H)%g (at level 40, left associativity).
+Notation "G \* H" := (cprod G H)%g (at level 40, left associativity).
+Notation "G \x H" := (dprod G H)%g (at level 40, left associativity).

-Notation "[ 'complements' 'to' A 'in' B ]" := (complements_to_in A B)
+Notation "[ 'complements' 'to' A 'in' B ]" := (complements_to_in A B)
  (at level 0, format "[ 'complements' 'to' A 'in' B ]") : group_scope.

-Notation "[ 'splits' B , 'over' A ]" := (splits_over B A)
+Notation "[ 'splits' B , 'over' A ]" := (splits_over B A)
  (at level 0, format "[ 'splits' B , 'over' A ]") : group_scope.

@@ -157,50 +156,50 @@
Variable gT : finGroupType.
-Implicit Types A B C : {set gT}.
-Implicit Types G H K L M : {group gT}.
+Implicit Types A B C : {set gT}.
+Implicit Types G H K L M : {group gT}.


-Lemma pprod1g : left_id 1 pprod.
+Lemma pprod1g : left_id 1 pprod.

-Lemma pprodg1 : right_id 1 pprod.
+Lemma pprodg1 : right_id 1 pprod.

-CoInductive are_groups A B : Prop := AreGroups K H of A = K & B = H.
+Variant are_groups A B : Prop := AreGroups K H of A = K & B = H.

-Lemma group_not0 G : set0 ≠ G.
+Lemma group_not0 G : set0 ≠ G.

-Lemma mulg0 : right_zero (@set0 gT) mulg.
+Lemma mulg0 : right_zero (@set0 gT) mulg.

-Lemma mul0g : left_zero (@set0 gT) mulg.
+Lemma mul0g : left_zero (@set0 gT) mulg.

Lemma pprodP A B G :
-  pprod A B = G → [/\ are_groups A B, A × B = G & B \subset 'N(A)].
+  pprod A B = G → [/\ are_groups A B, A × B = G & B \subset 'N(A)].

-Lemma pprodE K H : H \subset 'N(K) → pprod K H = K × H.
+Lemma pprodE K H : H \subset 'N(K) → pprod K H = K × H.

-Lemma pprodEY K H : H \subset 'N(K) → pprod K H = K <*> H.
+Lemma pprodEY K H : H \subset 'N(K) → pprod K H = K <*> H.

-Lemma pprodW A B G : pprod A B = G → A × B = G.
+Lemma pprodW A B G : pprod A B = G → A × B = G.

-Lemma pprodWC A B G : pprod A B = G → B × A = G.
+Lemma pprodWC A B G : pprod A B = G → B × A = G.

-Lemma pprodWY A B G : pprod A B = G → A <*> B = G.
+Lemma pprodWY A B G : pprod A B = G → A <*> B = G.

-Lemma pprodJ A B x : pprod A B :^ x = pprod (A :^ x) (B :^ x).
+Lemma pprodJ A B x : pprod A B :^ x = pprod (A :^ x) (B :^ x).

@@ -211,46 +210,46 @@

-Lemma remgrMl K B x y : y \in K → remgr K B (y × x) = remgr K B x.
+Lemma remgrMl K B x y : y \in K → remgr K B (y × x) = remgr K B x.

-Lemma remgrP K B x : (remgr K B x \in K :* x :&: B) = (x \in K × B).
+Lemma remgrP K B x : (remgr K B x \in K :* x :&: B) = (x \in K × B).

-Lemma remgr1 K H x : x \in K → remgr K H x = 1.
+Lemma remgr1 K H x : x \in K → remgr K H x = 1.

-Lemma divgr_eq A B x : x = divgr A B x × remgr A B x.
+Lemma divgr_eq A B x : x = divgr A B x × remgr A B x.

-Lemma divgrMl K B x y : x \in K → divgr K B (x × y) = x × divgr K B y.
+Lemma divgrMl K B x y : x \in K → divgr K B (x × y) = x × divgr K B y.

-Lemma divgr_id K H x : x \in K → divgr K H x = x.
+Lemma divgr_id K H x : x \in K → divgr K H x = x.

-Lemma mem_remgr K B x : x \in K × B → remgr K B x \in B.
+Lemma mem_remgr K B x : x \in K × B → remgr K B x \in B.

-Lemma mem_divgr K B x : x \in K × B → divgr K B x \in K.
+Lemma mem_divgr K B x : x \in K × B → divgr K B x \in K.

Section DisjointRem.

-Variables K H : {group gT}.
+Variables K H : {group gT}.

-Hypothesis tiKH : K :&: H = 1.
+Hypothesis tiKH : K :&: H = 1.

-Lemma remgr_id x : x \in H → remgr K H x = x.
+Lemma remgr_id x : x \in H → remgr K H x = x.

-Lemma remgrMid x y : x \in K → y \in H → remgr K H (x × y) = y.
+Lemma remgrMid x y : x \in K → y \in H → remgr K H (x × y) = y.

-Lemma divgrMid x y : x \in K → y \in H → divgr K H (x × y) = x.
+Lemma divgrMid x y : x \in K → y \in H → divgr K H (x × y) = x.

End DisjointRem.
@@ -265,7 +264,7 @@
Lemma subcent_TImulg K H A :
-  K :&: H = 1 → A \subset 'N(K) :&: 'N(H) → 'C_K(A) × 'C_H(A) = 'C_(K × H)(A).
+  K :&: H = 1 → A \subset 'N(K) :&: 'N(H) → 'C_K(A) × 'C_H(A) = 'C_(K × H)(A).

@@ -277,30 +276,30 @@
Lemma complP H A B :
-  reflect (A :&: H = 1 ∧ A × H = B) (H \in [complements to A in B]).
+  reflect (A :&: H = 1 ∧ A × H = B) (H \in [complements to A in B]).

Lemma splitsP B A :
-  reflect (∃ H, H \in [complements to A in B]) [splits B, over A].
+  reflect (∃ H, H \in [complements to A in B]) [splits B, over A].

Lemma complgC H K G :
-  (H \in [complements to K in G]) = (K \in [complements to H in G]).
+  (H \in [complements to K in G]) = (K \in [complements to H in G]).

Section NormalComplement.

-Variables K H G : {group gT}.
+Variables K H G : {group gT}.

-Hypothesis complH_K : H \in [complements to K in G].
+Hypothesis complH_K : H \in [complements to K in G].

-Lemma remgrM : K <| G → {in G &, {morph remgr K H : x y / x × y}}.
+Lemma remgrM : K <| G → {in G &, {morph remgr K H : x y / x × y}}.

-Lemma divgrM : H \subset 'C(K) → {in G &, {morph divgr K H : x y / x × y}}.
+Lemma divgrM : H \subset 'C(K) → {in G &, {morph divgr K H : x y / x × y}}.

End NormalComplement.
@@ -314,106 +313,106 @@

-Lemma sdprod1g : left_id 1 sdprod.
+Lemma sdprod1g : left_id 1 sdprod.

-Lemma sdprodg1 : right_id 1 sdprod.
+Lemma sdprodg1 : right_id 1 sdprod.

Lemma sdprodP A B G :
-  A ><| B = G → [/\ are_groups A B, A × B = G, B \subset 'N(A) & A :&: B = 1].
+  A ><| B = G → [/\ are_groups A B, A × B = G, B \subset 'N(A) & A :&: B = 1].

-Lemma sdprodE K H : H \subset 'N(K) → K :&: H = 1 → K ><| H = K × H.
+Lemma sdprodE K H : H \subset 'N(K) → K :&: H = 1 → K ><| H = K × H.

-Lemma sdprodEY K H : H \subset 'N(K) → K :&: H = 1 → K ><| H = K <*> H.
+Lemma sdprodEY K H : H \subset 'N(K) → K :&: H = 1 → K ><| H = K <*> H.

-Lemma sdprodWpp A B G : A ><| B = G → pprod A B = G.
+Lemma sdprodWpp A B G : A ><| B = G → pprod A B = G.

-Lemma sdprodW A B G : A ><| B = G → A × B = G.
+Lemma sdprodW A B G : A ><| B = G → A × B = G.

-Lemma sdprodWC A B G : A ><| B = G → B × A = G.
+Lemma sdprodWC A B G : A ><| B = G → B × A = G.

-Lemma sdprodWY A B G : A ><| B = G → A <*> B = G.
+Lemma sdprodWY A B G : A ><| B = G → A <*> B = G.

-Lemma sdprodJ A B x : (A ><| B) :^ x = A :^ x ><| B :^ x.
+Lemma sdprodJ A B x : (A ><| B) :^ x = A :^ x ><| B :^ x.

-Lemma sdprod_context G K H : K ><| H = G →
-  [/\ K <| G, H \subset G, K × H = G, H \subset 'N(K) & K :&: H = 1].
+Lemma sdprod_context G K H : K ><| H = G →
+  [/\ K <| G, H \subset G, K × H = G, H \subset 'N(K) & K :&: H = 1].

-Lemma sdprod_compl G K H : K ><| H = G → H \in [complements to K in G].
+Lemma sdprod_compl G K H : K ><| H = G → H \in [complements to K in G].

Lemma sdprod_normal_complP G K H :
-  K <| G → reflect (K ><| H = G) (K \in [complements to H in G]).
+  K <| G → reflect (K ><| H = G) (K \in [complements to H in G]).

-Lemma sdprod_card G A B : A ><| B = G → (#|A| × #|B|)%N = #|G|.
+Lemma sdprod_card G A B : A ><| B = G → (#|A| × #|B|)%N = #|G|.

Lemma sdprod_isom G A B :
-    A ><| B = G →
- {nAB : B \subset 'N(A) | isom B (G / A) (restrm nAB (coset A))}.
+    A ><| B = G →
+ {nAB : B \subset 'N(A) | isom B (G / A) (restrm nAB (coset A))}.

-Lemma sdprod_isog G A B : A ><| B = G → B \isog G / A.
+Lemma sdprod_isog G A B : A ><| B = G → B \isog G / A.

-Lemma sdprod_subr G A B M : A ><| B = G → M \subset B → A ><| M = A <*> M.
+Lemma sdprod_subr G A B M : A ><| B = G → M \subset B → A ><| M = A <*> M.

-Lemma index_sdprod G A B : A ><| B = G → #|B| = #|G : A|.
+Lemma index_sdprod G A B : A ><| B = G → #|B| = #|G : A|.

Lemma index_sdprodr G A B M :
-  A ><| B = G → M \subset B → #|B : M| = #|G : A <*> M|.
+  A ><| B = G → M \subset B → #|B : M| = #|G : A <*> M|.

Lemma quotient_sdprodr_isom G A B M :
-    A ><| B = G → M <| B →
-  {f : {morphism B / M >-> coset_of (A <*> M)} |
-    isom (B / M) (G / (A <*> M)) f
-  & ∀ L, L \subset B → f @* (L / M) = A <*> L / (A <*> M)}.
+    A ><| B = G → M <| B →
+  {f : {morphism B / M >-> coset_of (A <*> M)} |
+    isom (B / M) (G / (A <*> M)) f
+  & ∀ L, L \subset B → f @* (L / M) = A <*> L / (A <*> M)}.

Lemma quotient_sdprodr_isog G A B M :
-  A ><| B = G → M <| B → B / M \isog G / (A <*> M).
+  A ><| B = G → M <| B → B / M \isog G / (A <*> M).

Lemma sdprod_modl A B G H :
-  A ><| B = G → A \subset H → A ><| (B :&: H) = G :&: H.
+  A ><| B = G → A \subset H → A ><| (B :&: H) = G :&: H.

Lemma sdprod_modr A B G H :
-  A ><| B = G → B \subset H → (H :&: A) ><| B = H :&: G.
+  A ><| B = G → B \subset H → (H :&: A) ><| B = H :&: G.

Lemma subcent_sdprod B C G A :
-  B ><| C = G → A \subset 'N(B) :&: 'N(C) → 'C_B(A) ><| 'C_C(A) = 'C_G(A).
+  B ><| C = G → A \subset 'N(B) :&: 'N(C) → 'C_B(A) ><| 'C_C(A) = 'C_G(A).

Lemma sdprod_recl n G K H K1 :
-    #|G| ≤ n → K ><| H = G → K1 \proper K → H \subset 'N(K1) →
-  ∃ G1 : {group gT}, [/\ #|G1| < n, G1 \subset G & K1 ><| H = G1].
+    #|G| ≤ n → K ><| H = G → K1 \proper K → H \subset 'N(K1) →
+  ∃ G1 : {group gT}, [/\ #|G1| < n, G1 \subset G & K1 ><| H = G1].

Lemma sdprod_recr n G K H H1 :
-    #|G| ≤ n → K ><| H = G → H1 \proper H →
-  ∃ G1 : {group gT}, [/\ #|G1| < n, G1 \subset G & K ><| H1 = G1].
+    #|G| ≤ n → K ><| H = G → H1 \proper H →
+  ∃ G1 : {group gT}, [/\ #|G1| < n, G1 \subset G & K ><| H1 = G1].

-Lemma mem_sdprod G A B x : A ><| B = G → x \in G →
-  ∃ y, ∃ z,
-    [/\ y \in A, z \in B, x = y × z &
-        {in A & B, ∀ u t, x = u × t → u = y ∧ t = z}].
+Lemma mem_sdprod G A B x : A ><| B = G → x \in G →
+  ∃ y, ∃ z,
+    [/\ y \in A, z \in B, x = y × z &
+        {in A & B, ∀ u t, x = u × t → u = y ∧ t = z}].

@@ -424,69 +423,69 @@

-Lemma cprod1g : left_id 1 cprod.
+Lemma cprod1g : left_id 1 cprod.

-Lemma cprodg1 : right_id 1 cprod.
+Lemma cprodg1 : right_id 1 cprod.

Lemma cprodP A B G :
-  A \* B = G → [/\ are_groups A B, A × B = G & B \subset 'C(A)].
+  A \* B = G → [/\ are_groups A B, A × B = G & B \subset 'C(A)].

-Lemma cprodE G H : H \subset 'C(G) → G \* H = G × H.
+Lemma cprodE G H : H \subset 'C(G) → G \* H = G × H.

-Lemma cprodEY G H : H \subset 'C(G) → G \* H = G <*> H.
+Lemma cprodEY G H : H \subset 'C(G) → G \* H = G <*> H.

-Lemma cprodWpp A B G : A \* B = G → pprod A B = G.
+Lemma cprodWpp A B G : A \* B = G → pprod A B = G.

-Lemma cprodW A B G : A \* B = G → A × B = G.
+Lemma cprodW A B G : A \* B = G → A × B = G.

-Lemma cprodWC A B G : A \* B = G → B × A = G.
+Lemma cprodWC A B G : A \* B = G → B × A = G.

-Lemma cprodWY A B G : A \* B = G → A <*> B = G.
+Lemma cprodWY A B G : A \* B = G → A <*> B = G.

-Lemma cprodJ A B x : (A \* B) :^ x = A :^ x \* B :^ x.
+Lemma cprodJ A B x : (A \* B) :^ x = A :^ x \* B :^ x.

-Lemma cprod_normal2 A B G : A \* B = G → A <| G ∧ B <| G.
+Lemma cprod_normal2 A B G : A \* B = G → A <| G ∧ B <| G.

Lemma bigcprodW I (r : seq I) P F G :
-  \big[cprod/1]_(i <- r | P i) F i = G → \prod_(i <- r | P i) F i = G.
+  \big[cprod/1]_(i <- r | P i) F i = G → \prod_(i <- r | P i) F i = G.

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.
+  \big[cprod/1]_(i <- r | P i) F i = G → << \bigcup_(i <- r | P i) F i >> = G.

-Lemma triv_cprod A B : (A \* B == 1) = (A == 1) && (B == 1).
+Lemma triv_cprod A B : (A \* B == 1) = (A == 1) && (B == 1).

-Lemma cprod_ntriv A B : A != 1 → B != 1 →
-  A \* B =
-    if [&& group_set A, group_set B & B \subset 'C(A)] then A × B else set0.
+Lemma cprod_ntriv A B : A != 1 → B != 1 →
+  A \* B =
+    if [&& group_set A, group_set B & B \subset 'C(A)] then A × B else set0.

-Lemma trivg0 : (@set0 gT == 1) = false.
+Lemma trivg0 : (@set0 gT == 1) = false.

-Lemma group0 : group_set (@set0 gT) = false.
+Lemma group0 : group_set (@set0 gT) = false.

-Lemma cprod0g A : set0 \* A = set0.
+Lemma cprod0g A : set0 \* A = set0.

-Lemma cprodC : commutative cprod.
+Lemma cprodC : commutative cprod.

-Lemma cprodA : associative cprod.
+Lemma cprodA : associative cprod.

Canonical cprod_law := Monoid.Law cprodA cprod1g cprodg1.
@@ -494,33 +493,33 @@
Lemma cprod_modl A B G H :
-  A \* B = G → A \subset H → A \* (B :&: H) = G :&: H.
+  A \* B = G → A \subset H → A \* (B :&: H) = G :&: H.

Lemma cprod_modr A B G H :
-  A \* B = G → B \subset H → (H :&: A) \* B = H :&: G.
+  A \* B = G → B \subset H → (H :&: A) \* B = H :&: G.

-Lemma bigcprodYP (I : finType) (P : pred I) (H : I → {group gT}) :
-  reflect (∀ i j, P i → P j → i != j → H i \subset 'C(H j))
-          (\big[cprod/1]_(i | P i) H i == (\prod_(i | P i) H i)%G).
+Lemma bigcprodYP (I : finType) (P : pred I) (H : I → {group gT}) :
+  reflect (∀ i j, P i → P j → i != j → H i \subset 'C(H j))
+          (\big[cprod/1]_(i | P i) H i == (\prod_(i | P i) H i)%G).

-Lemma bigcprodEY I r (P : pred I) (H : I → {group gT}) G :
-    abelian G → (∀ i, P i → H i \subset G) →
-  \big[cprod/1]_(i <- r | P i) H i = (\prod_(i <- r | P i) H i)%G.
+Lemma bigcprodEY I r (P : pred I) (H : I → {group gT}) G :
+    abelian G → (∀ i, P i → H i \subset G) →
+  \big[cprod/1]_(i <- r | P i) H i = (\prod_(i <- r | P i) H i)%G.

-Lemma perm_bigcprod (I : eqType) r1 r2 (A : I → {set gT}) G x :
-    \big[cprod/1]_(i <- r1) A i = G → {in r1, ∀ i, x i \in A i} →
-    perm_eq r1 r2 →
-  \prod_(i <- r1) x i = \prod_(i <- r2) x i.
+Lemma perm_bigcprod (I : eqType) r1 r2 (A : I → {set gT}) G x :
+    \big[cprod/1]_(i <- r1) A i = G → {in r1, ∀ i, x i \in A i} →
+    perm_eq r1 r2 →
+  \prod_(i <- r1) x i = \prod_(i <- r2) x i.

-Lemma reindex_bigcprod (I J : finType) (h : J → I) P (A : I → {set gT}) G x :
-    {on SimplPred P, bijective h} → \big[cprod/1]_(i | P i) A i = G →
-    {in SimplPred P, ∀ i, x i \in A i} →
-  \prod_(i | P i) x i = \prod_(j | P (h j)) x (h j).
+Lemma reindex_bigcprod (I J : finType) (h : J → I) P (A : I → {set gT}) G x :
+    {on SimplPred P, bijective h} → \big[cprod/1]_(i | P i) A i = G →
+    {in SimplPred P, ∀ i, x i \in A i} →
+  \prod_(i | P i) x i = \prod_(j | P (h j)) x (h j).

@@ -531,63 +530,63 @@

-Lemma dprod1g : left_id 1 dprod.
+Lemma dprod1g : left_id 1 dprod.

-Lemma dprodg1 : right_id 1 dprod.
+Lemma dprodg1 : right_id 1 dprod.

Lemma dprodP A B G :
-  A \x B = G → [/\ are_groups A B, A × B = G, B \subset 'C(A) & A :&: B = 1].
+  A \x B = G → [/\ are_groups A B, A × B = G, B \subset 'C(A) & A :&: B = 1].

-Lemma dprodE G H : H \subset 'C(G) → G :&: H = 1 → G \x H = G × H.
+Lemma dprodE G H : H \subset 'C(G) → G :&: H = 1 → G \x H = G × H.

-Lemma dprodEY G H : H \subset 'C(G) → G :&: H = 1 → G \x H = G <*> H.
+Lemma dprodEY G H : H \subset 'C(G) → G :&: H = 1 → G \x H = G <*> H.

-Lemma dprodEcp A B : A :&: B = 1 → A \x B = A \* B.
+Lemma dprodEcp A B : A :&: B = 1 → A \x B = A \* B.

-Lemma dprodEsd A B : B \subset 'C(A) → A \x B = A ><| B.
+Lemma dprodEsd A B : B \subset 'C(A) → A \x B = A ><| B.

-Lemma dprodWcp A B G : A \x B = G → A \* B = G.
+Lemma dprodWcp A B G : A \x B = G → A \* B = G.

-Lemma dprodWsd A B G : A \x B = G → A ><| B = G.
+Lemma dprodWsd A B G : A \x B = G → A ><| B = G.

-Lemma dprodW A B G : A \x B = G → A × B = G.
+Lemma dprodW A B G : A \x B = G → A × B = G.

-Lemma dprodWC A B G : A \x B = G → B × A = G.
+Lemma dprodWC A B G : A \x B = G → B × A = G.

-Lemma dprodWY A B G : A \x B = G → A <*> B = G.
+Lemma dprodWY A B G : A \x B = G → A <*> B = G.

Lemma cprod_card_dprod G A B :
-  A \* B = G → #|A| × #|B| ≤ #|G| → A \x B = G.
+  A \* B = G → #|A| × #|B| ≤ #|G| → A \x B = G.

-Lemma dprodJ A B x : (A \x B) :^ x = A :^ x \x B :^ x.
+Lemma dprodJ A B x : (A \x B) :^ x = A :^ x \x B :^ x.

-Lemma dprod_normal2 A B G : A \x B = G → A <| G ∧ B <| G.
+Lemma dprod_normal2 A B G : A \x B = G → A <| G ∧ B <| G.

-Lemma dprodYP K H : reflect (K \x H = K <*> H) (H \subset 'C(K) :\: K^#).
+Lemma dprodYP K H : reflect (K \x H = K <*> H) (H \subset 'C(K) :\: K^#).

-Lemma dprodC : commutative dprod.
+Lemma dprodC : commutative dprod.

-Lemma dprodWsdC A B G : A \x B = G → B ><| A = G.
+Lemma dprodWsdC A B G : A \x B = G → B ><| A = G.

-Lemma dprodA : associative dprod.
+Lemma dprodA : associative dprod.

Canonical dprod_law := Monoid.Law dprodA dprod1g dprodg1.
@@ -595,67 +594,67 @@
Lemma bigdprodWcp I (r : seq I) P F G :
-  \big[dprod/1]_(i <- r | P i) F i = G → \big[cprod/1]_(i <- r | P i) F i = G.
+  \big[dprod/1]_(i <- r | P i) F i = G → \big[cprod/1]_(i <- r | P i) F i = G.

Lemma bigdprodW I (r : seq I) P F G :
-  \big[dprod/1]_(i <- r | P i) F i = G → \prod_(i <- r | P i) F i = G.
+  \big[dprod/1]_(i <- r | P i) F i = G → \prod_(i <- r | P i) F i = G.

Lemma bigdprodWY I (r : seq I) P F G :
-  \big[dprod/1]_(i <- r | P i) F i = G → << \bigcup_(i <- r | P i) F i >> = G.
+  \big[dprod/1]_(i <- r | P i) F i = G → << \bigcup_(i <- r | P i) F i >> = G.

-Lemma bigdprodYP (I : finType) (P : pred I) (F : I → {group gT}) :
-  reflect (∀ i, P i →
-             (\prod_(j | P j && (j != i)) F j)%G \subset 'C(F i) :\: (F i)^#)
-          (\big[dprod/1]_(i | P i) F i == (\prod_(i | P i) F i)%G).
+Lemma bigdprodYP (I : finType) (P : pred I) (F : I → {group gT}) :
+  reflect (∀ i, P i →
+             (\prod_(j | P j && (j != i)) F j)%G \subset 'C(F i) :\: (F i)^#)
+          (\big[dprod/1]_(i | P i) F i == (\prod_(i | P i) F i)%G).

Lemma dprod_modl A B G H :
-  A \x B = G → A \subset H → A \x (B :&: H) = G :&: H.
+  A \x B = G → A \subset H → A \x (B :&: H) = G :&: H.

Lemma dprod_modr A B G H :
-  A \x B = G → B \subset H → (H :&: A) \x B = H :&: G.
+  A \x B = G → B \subset H → (H :&: A) \x B = H :&: G.

Lemma subcent_dprod B C G A :
-   B \x C = G → A \subset 'N(B) :&: 'N(C) → 'C_B(A) \x 'C_C(A) = 'C_G(A).
+   B \x C = G → A \subset 'N(B) :&: 'N(C) → 'C_B(A) \x 'C_C(A) = 'C_G(A).

-Lemma dprod_card A B G : A \x B = G → (#|A| × #|B|)%N = #|G|.
+Lemma dprod_card A B G : A \x B = G → (#|A| × #|B|)%N = #|G|.

-Lemma bigdprod_card I r (P : pred I) E G :
-    \big[dprod/1]_(i <- r | P i) E i = G →
-  (\prod_(i <- r | P i) #|E i|)%N = #|G|.
+Lemma bigdprod_card I r (P : pred I) E G :
+    \big[dprod/1]_(i <- r | P i) E i = G →
+  (\prod_(i <- r | P i) #|E i|)%N = #|G|.

-Lemma bigcprod_card_dprod I r (P : pred I) (A : I → {set gT}) G :
-    \big[cprod/1]_(i <- r | P i) A i = G →
-    \prod_(i <- r | P i) #|A i| ≤ #|G| →
-  \big[dprod/1]_(i <- r | P i) A i = G.
+Lemma bigcprod_card_dprod I r (P : pred I) (A : I → {set gT}) G :
+    \big[cprod/1]_(i <- r | P i) A i = G →
+    \prod_(i <- r | P i) #|A i| ≤ #|G| →
+  \big[dprod/1]_(i <- r | P i) A i = G.

-Lemma bigcprod_coprime_dprod (I : finType) (P : pred I) (A : I → {set gT}) G :
-    \big[cprod/1]_(i | P i) A i = G →
-    (∀ i j, P i → P j → i != j → coprime #|A i| #|A j|) →
-  \big[dprod/1]_(i | P i) A i = G.
+Lemma bigcprod_coprime_dprod (I : finType) (P : pred I) (A : I → {set gT}) G :
+    \big[cprod/1]_(i | P i) A i = G →
+    (∀ i j, P i → P j → i != j → coprime #|A i| #|A j|) →
+  \big[dprod/1]_(i | P i) A i = G.

-Lemma mem_dprod G A B x : A \x B = G → x \in G →
-  ∃ y, ∃ z,
-    [/\ y \in A, z \in B, x = y × z &
-        {in A & B, ∀ u t, x = u × t → u = y ∧ t = z}].
+Lemma mem_dprod G A B x : A \x B = G → x \in G →
+  ∃ y, ∃ z,
+    [/\ y \in A, z \in B, x = y × z &
+        {in A & B, ∀ u t, x = u × t → u = y ∧ t = z}].

-Lemma mem_bigdprod (I : finType) (P : pred I) F G x :
-    \big[dprod/1]_(i | P i) F i = G → x \in G →
-  ∃ c, [/\ ∀ i, P i → c i \in F i, x = \prod_(i | P i) c i
-              & ∀ e, (∀ i, P i → e i \in F i) →
-                          x = \prod_(i | P i) e i →
-                ∀ i, P i → e i = c i].
+Lemma mem_bigdprod (I : finType) (P : pred I) F G x :
+    \big[dprod/1]_(i | P i) F i = G → x \in G →
+  ∃ c, [/\ ∀ i, P i → c i \in F i, x = \prod_(i | P i) c i
+              & ∀ e, (∀ i, P i → e i \in F i) →
+                          x = \prod_(i | P i) e i →
+                ∀ i, P i → e i = c i].

End InternalProd.
@@ -666,56 +665,56 @@ Section MorphimInternalProd.

-Variables (gT rT : finGroupType) (D : {group gT}) (f : {morphism D >-> rT}).
+Variables (gT rT : finGroupType) (D : {group gT}) (f : {morphism D >-> rT}).

Section OneProd.

-Variables G H K : {group gT}.
-Hypothesis sGD : G \subset D.
+Variables G H K : {group gT}.
+Hypothesis sGD : G \subset D.

-Lemma morphim_pprod : pprod K H = G → pprod (f @* K) (f @* H) = f @* G.
+Lemma morphim_pprod : pprod K H = G → pprod (f @* K) (f @* H) = f @* G.

Lemma morphim_coprime_sdprod :
-  K ><| H = G → coprime #|K| #|H| → f @* K ><| f @* H = f @* G.
+  K ><| H = G → coprime #|K| #|H| → f @* K ><| f @* H = f @* G.

-Lemma injm_sdprod : 'injm f → K ><| H = G → f @* K ><| f @* H = f @* G.
+Lemma injm_sdprod : 'injm f → K ><| H = G → f @* K ><| f @* H = f @* G.

-Lemma morphim_cprod : K \* H = G → f @* K \* f @* H = f @* G.
+Lemma morphim_cprod : K \* H = G → f @* K \* f @* H = f @* G.

-Lemma injm_dprod : 'injm f → K \x H = G → f @* K \x f @* H = f @* G.
+Lemma injm_dprod : 'injm f → K \x H = G → f @* K \x f @* H = f @* G.

Lemma morphim_coprime_dprod :
-  K \x H = G → coprime #|K| #|H| → f @* K \x f @* H = f @* G.
+  K \x H = G → coprime #|K| #|H| → f @* K \x f @* H = f @* G.

End OneProd.

-Implicit Type G : {group gT}.
+Implicit Type G : {group gT}.

-Lemma morphim_bigcprod I r (P : pred I) (H : I → {group gT}) G :
-    G \subset D → \big[cprod/1]_(i <- r | P i) H i = G →
-  \big[cprod/1]_(i <- r | P i) f @* H i = f @* G.
+Lemma morphim_bigcprod I r (P : pred I) (H : I → {group gT}) G :
+    G \subset D → \big[cprod/1]_(i <- r | P i) H i = G →
+  \big[cprod/1]_(i <- r | P i) f @* H i = f @* G.

-Lemma injm_bigdprod I r (P : pred I) (H : I → {group gT}) G :
-    G \subset D → 'injm f → \big[dprod/1]_(i <- r | P i) H i = G →
-  \big[dprod/1]_(i <- r | P i) f @* H i = f @* G.
+Lemma injm_bigdprod I r (P : pred I) (H : I → {group gT}) G :
+    G \subset D → 'injm f → \big[dprod/1]_(i <- r | P i) H i = G →
+  \big[dprod/1]_(i <- r | P i) f @* H i = f @* G.

-Lemma morphim_coprime_bigdprod (I : finType) P (H : I → {group gT}) G :
-    G \subset D → \big[dprod/1]_(i | P i) H i = G →
-    (∀ i j, P i → P j → i != j → coprime #|H i| #|H j|) →
-  \big[dprod/1]_(i | P i) f @* H i = f @* G.
+Lemma morphim_coprime_bigdprod (I : finType) P (H : I → {group gT}) G :
+    G \subset D → \big[dprod/1]_(i | P i) H i = G →
+    (∀ i j, P i → P j → i != j → coprime #|H i| #|H j|) →
+  \big[dprod/1]_(i | P i) f @* H i = f @* G.

End MorphimInternalProd.
@@ -724,24 +723,24 @@ Section QuotientInternalProd.

-Variables (gT : finGroupType) (G K H M : {group gT}).
+Variables (gT : finGroupType) (G K H M : {group gT}).

-Hypothesis nMG: G \subset 'N(M).
+Hypothesis nMG: G \subset 'N(M).

-Lemma quotient_pprod : pprod K H = G → pprod (K / M) (H / M) = G / M.
+Lemma quotient_pprod : pprod K H = G → pprod (K / M) (H / M) = G / M.

Lemma quotient_coprime_sdprod :
-  K ><| H = G → coprime #|K| #|H| → (K / M) ><| (H / M) = G / M.
+  K ><| H = G → coprime #|K| #|H| → (K / M) ><| (H / M) = G / M.

-Lemma quotient_cprod : K \* H = G → (K / M) \* (H / M) = G / M.
+Lemma quotient_cprod : K \* H = G → (K / M) \* (H / M) = G / M.

Lemma quotient_coprime_dprod :
-  K \x H = G → coprime #|K| #|H| → (K / M) \x (H / M) = G / M.
+  K \x H = G → coprime #|K| #|H| → (K / M) \x (H / M) = G / M.

End QuotientInternalProd.
@@ -753,96 +752,96 @@ Variables gT1 gT2 : finGroupType.

-Definition extprod_mulg (x y : gT1 × gT2) := (x.1 × y.1, x.2 × y.2).
-Definition extprod_invg (x : gT1 × gT2) := (x.1^-1, x.2^-1).
+Definition extprod_mulg (x y : gT1 × gT2) := (x.1 × y.1, x.2 × y.2).
+Definition extprod_invg (x : gT1 × gT2) := (x.1^-1, x.2^-1).

-Lemma extprod_mul1g : left_id (1, 1) extprod_mulg.
+Lemma extprod_mul1g : left_id (1, 1) extprod_mulg.

-Lemma extprod_mulVg : left_inverse (1, 1) extprod_invg extprod_mulg.
+Lemma extprod_mulVg : left_inverse (1, 1) extprod_invg extprod_mulg.

-Lemma extprod_mulgA : associative extprod_mulg.
+Lemma extprod_mulgA : associative extprod_mulg.

Definition extprod_groupMixin :=
  Eval hnf in FinGroup.Mixin extprod_mulgA extprod_mul1g extprod_mulVg.
Canonical extprod_baseFinGroupType :=
-  Eval hnf in BaseFinGroupType (gT1 × gT2) extprod_groupMixin.
+  Eval hnf in BaseFinGroupType (gT1 × gT2) extprod_groupMixin.
Canonical prod_group := FinGroupType extprod_mulVg.

-Lemma group_setX (H1 : {group gT1}) (H2 : {group gT2}) : group_set (setX H1 H2).
+Lemma group_setX (H1 : {group gT1}) (H2 : {group gT2}) : group_set (setX H1 H2).

Canonical setX_group H1 H2 := Group (group_setX H1 H2).

-Definition pairg1 x : gT1 × gT2 := (x, 1).
-Definition pair1g x : gT1 × gT2 := (1, x).
+Definition pairg1 x : gT1 × gT2 := (x, 1).
+Definition pair1g x : gT1 × gT2 := (1, x).

-Lemma pairg1_morphM : {morph pairg1 : x y / x × y}.
+Lemma pairg1_morphM : {morph pairg1 : x y / x × y}.

-Canonical pairg1_morphism := @Morphism _ _ setT _ (in2W pairg1_morphM).
+Canonical pairg1_morphism := @Morphism _ _ setT _ (in2W pairg1_morphM).

-Lemma pair1g_morphM : {morph pair1g : x y / x × y}.
+Lemma pair1g_morphM : {morph pair1g : x y / x × y}.

-Canonical pair1g_morphism := @Morphism _ _ setT _ (in2W pair1g_morphM).
+Canonical pair1g_morphism := @Morphism _ _ setT _ (in2W pair1g_morphM).

-Lemma fst_morphM : {morph (@fst gT1 gT2) : x y / x × y}.
+Lemma fst_morphM : {morph (@fst gT1 gT2) : x y / x × y}.

-Lemma snd_morphM : {morph (@snd gT1 gT2) : x y / x × y}.
+Lemma snd_morphM : {morph (@snd gT1 gT2) : x y / x × y}.

-Canonical fst_morphism := @Morphism _ _ setT _ (in2W fst_morphM).
+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.
+Lemma injm_pair1g : 'injm pair1g.

-Lemma injm_pairg1 : 'injm pairg1.
+Lemma injm_pairg1 : 'injm pairg1.

-Lemma morphim_pairg1 (H1 : {set gT1}) : pairg1 @* H1 = setX H1 1.
+Lemma morphim_pairg1 (H1 : {set gT1}) : pairg1 @* H1 = setX H1 1.

-Lemma morphim_pair1g (H2 : {set gT2}) : pair1g @* H2 = setX 1 H2.
+Lemma morphim_pair1g (H2 : {set gT2}) : pair1g @* H2 = setX 1 H2.

-Lemma morphim_fstX (H1: {set gT1}) (H2 : {group gT2}) :
-  [morphism of fun x ⇒ x.1] @* setX H1 H2 = H1.
+Lemma morphim_fstX (H1: {set gT1}) (H2 : {group gT2}) :
+  [morphism of fun x ⇒ x.1] @* setX H1 H2 = H1.

-Lemma morphim_sndX (H1: {group gT1}) (H2 : {set gT2}) :
-  [morphism of fun x ⇒ x.2] @* setX H1 H2 = H2.
+Lemma morphim_sndX (H1: {group gT1}) (H2 : {set gT2}) :
+  [morphism of fun x ⇒ x.2] @* setX H1 H2 = H2.

-Lemma setX_prod (H1 : {set gT1}) (H2 : {set gT2}) :
-  setX H1 1 × setX 1 H2 = setX H1 H2.
+Lemma setX_prod (H1 : {set gT1}) (H2 : {set gT2}) :
+  setX H1 1 × setX 1 H2 = setX H1 H2.

-Lemma setX_dprod (H1 : {group gT1}) (H2 : {group gT2}) :
-  setX H1 1 \x setX 1 H2 = setX H1 H2.
+Lemma setX_dprod (H1 : {group gT1}) (H2 : {group gT2}) :
+  setX H1 1 \x setX 1 H2 = setX H1 H2.

-Lemma isog_setX1 (H1 : {group gT1}) : isog H1 (setX H1 1).
+Lemma isog_setX1 (H1 : {group gT1}) : isog H1 (setX H1 1).

-Lemma isog_set1X (H2 : {group gT2}) : isog H2 (setX 1 H2).
+Lemma isog_set1X (H2 : {group gT2}) : isog H2 (setX 1 H2).

-Lemma setX_gen (H1 : {set gT1}) (H2 : {set gT2}) :
-  1 \in H1 → 1 \in H2 → <<setX H1 H2>> = setX <<H1>> <<H2>>.
+Lemma setX_gen (H1 : {set gT1}) (H2 : {set gT2}) :
+  1 \in H1 → 1 \in H2 → <<setX H1 H2>> = setX <<H1>> <<H2>>.

End ExternalDirProd.
@@ -851,7 +850,7 @@ Section ExternalSDirProd.

-Variables (aT rT : finGroupType) (D : {group aT}) (R : {group rT}).
+Variables (aT rT : finGroupType) (D : {group aT}) (R : {group rT}).

@@ -862,8 +861,8 @@

-Inductive sdprod_by (to : groupAction D R) : predArgType :=
-   SdPair (ax : aT × rT) of ax \in setX D R.
+Inductive sdprod_by (to : groupAction D R) : predArgType :=
+   SdPair (ax : aT × rT) of ax \in setX D R.

Coercion pair_of_sd to (u : sdprod_by to) := let: SdPair ax _ := u in ax.
@@ -876,42 +875,42 @@ Notation sdval := (@pair_of_sd to).

-Canonical sdprod_subType := Eval hnf in [subType for sdval].
-Definition sdprod_eqMixin := Eval hnf in [eqMixin of sdT by <:].
+Canonical sdprod_subType := Eval hnf in [subType for sdval].
+Definition sdprod_eqMixin := Eval hnf in [eqMixin of sdT by <:].
Canonical sdprod_eqType := Eval hnf in EqType sdT sdprod_eqMixin.
-Definition sdprod_choiceMixin := [choiceMixin of sdT by <:].
+Definition sdprod_choiceMixin := [choiceMixin of sdT by <:].
Canonical sdprod_choiceType := ChoiceType sdT sdprod_choiceMixin.
-Definition sdprod_countMixin := [countMixin of sdT by <:].
+Definition sdprod_countMixin := [countMixin of sdT by <:].
Canonical sdprod_countType := CountType sdT sdprod_countMixin.
-Canonical sdprod_subCountType := Eval hnf in [subCountType of sdT].
-Definition sdprod_finMixin := [finMixin of sdT by <:].
+Canonical sdprod_subCountType := Eval hnf in [subCountType of sdT].
+Definition sdprod_finMixin := [finMixin of sdT by <:].
Canonical sdprod_finType := FinType sdT sdprod_finMixin.
-Canonical sdprod_subFinType := Eval hnf in [subFinType of sdT].
+Canonical sdprod_subFinType := Eval hnf in [subFinType of sdT].

Definition sdprod_one := SdPair to (group1 _).

-Lemma sdprod_inv_proof (u : sdT) : (u.1^-1, to u.2^-1 u.1^-1) \in setX D R.
+Lemma sdprod_inv_proof (u : sdT) : (u.1^-1, to u.2^-1 u.1^-1) \in setX D R.

Definition sdprod_inv u := SdPair to (sdprod_inv_proof u).

Lemma sdprod_mul_proof (u v : sdT) :
-  (u.1 × v.1, to u.2 v.1 × v.2) \in setX D R.
+  (u.1 × v.1, to u.2 v.1 × v.2) \in setX D R.

Definition sdprod_mul u v := SdPair to (sdprod_mul_proof u v).

-Lemma sdprod_mul1g : left_id sdprod_one sdprod_mul.
+Lemma sdprod_mul1g : left_id sdprod_one sdprod_mul.

-Lemma sdprod_mulVg : left_inverse sdprod_one sdprod_inv sdprod_mul.
+Lemma sdprod_mulVg : left_inverse sdprod_one sdprod_inv sdprod_mul.

-Lemma sdprod_mulgA : associative sdprod_mul.
+Lemma sdprod_mulgA : associative sdprod_mul.

Canonical sdprod_groupMixin :=
@@ -925,14 +924,14 @@ Canonical sdprod_groupType := FinGroupType sdprod_mulVg.

-Definition sdpair1 x := insubd sdprod_one (1, x) : sdT.
-Definition sdpair2 a := insubd sdprod_one (a, 1) : sdT.
+Definition sdpair1 x := insubd sdprod_one (1, x) : sdT.
+Definition sdpair2 a := insubd sdprod_one (a, 1) : sdT.

-Lemma sdpair1_morphM : {in R &, {morph sdpair1 : x y / x × y}}.
+Lemma sdpair1_morphM : {in R &, {morph sdpair1 : x y / x × y}}.

-Lemma sdpair2_morphM : {in D &, {morph sdpair2 : a b / a × b}}.
+Lemma sdpair2_morphM : {in D &, {morph sdpair2 : a b / a × b}}.

Canonical sdpair1_morphism := Morphism sdpair1_morphM.
@@ -941,51 +940,51 @@ Canonical sdpair2_morphism := Morphism sdpair2_morphM.

-Lemma injm_sdpair1 : 'injm sdpair1.
+Lemma injm_sdpair1 : 'injm sdpair1.

-Lemma injm_sdpair2 : 'injm sdpair2.
+Lemma injm_sdpair2 : 'injm sdpair2.

-Lemma sdpairE (u : sdT) : u = sdpair2 u.1 × sdpair1 u.2.
+Lemma sdpairE (u : sdT) : u = sdpair2 u.1 × sdpair1 u.2.

-Lemma sdpair_act : {in R & D,
-  ∀ x a, sdpair1 (to x a) = sdpair1 x ^ sdpair2 a}.
+Lemma sdpair_act : {in R & D,
+  ∀ x a, sdpair1 (to x a) = sdpair1 x ^ sdpair2 a}.

-Lemma sdpair_setact (G : {set rT}) a : G \subset R → a \in D →
-  sdpair1 @* (to^~ a @: G) = (sdpair1 @* G) :^ sdpair2 a.
+Lemma sdpair_setact (G : {set rT}) a : G \subset R → a \in D →
+  sdpair1 @* (to^~ a @: G) = (sdpair1 @* G) :^ sdpair2 a.

-Lemma im_sdpair_norm : sdpair2 @* D \subset 'N(sdpair1 @* R).
+Lemma im_sdpair_norm : sdpair2 @* D \subset 'N(sdpair1 @* R).

-Lemma im_sdpair_TI : (sdpair1 @* R) :&: (sdpair2 @* D) = 1.
+Lemma im_sdpair_TI : (sdpair1 @* R) :&: (sdpair2 @* D) = 1.

-Lemma im_sdpair : (sdpair1 @* R) × (sdpair2 @* D) = setT.
+Lemma im_sdpair : (sdpair1 @* R) × (sdpair2 @* D) = setT.

-Lemma sdprod_sdpair : sdpair1 @* R ><| sdpair2 @* D = setT.
+Lemma sdprod_sdpair : sdpair1 @* R ><| sdpair2 @* D = setT.

-Variables (A : {set aT}) (G : {set rT}).
+Variables (A : {set aT}) (G : {set rT}).

-Lemma gacentEsd : 'C_(|to)(A) = sdpair1 @*^-1 'C(sdpair2 @* A).
+Lemma gacentEsd : 'C_(|to)(A) = sdpair1 @*^-1 'C(sdpair2 @* A).

-Hypotheses (sAD : A \subset D) (sGR : G \subset R).
+Hypotheses (sAD : A \subset D) (sGR : G \subset R).

-Lemma astabEsd : 'C(G | to) = sdpair2 @*^-1 'C(sdpair1 @* G).
+Lemma astabEsd : 'C(G | to) = sdpair2 @*^-1 'C(sdpair1 @* G).

-Lemma astabsEsd : 'N(G | to) = sdpair2 @*^-1 'N(sdpair1 @* G).
+Lemma astabsEsd : 'N(G | to) = sdpair2 @*^-1 'N(sdpair1 @* G).

-Lemma actsEsd : [acts A, on G | to] = (sdpair2 @* A \subset 'N(sdpair1 @* G)).
+Lemma actsEsd : [acts A, on G | to] = (sdpair2 @* A \subset 'N(sdpair1 @* G)).

End ExternalSDirProd.
@@ -995,21 +994,21 @@
Variables gT rT : finGroupType.
-Implicit Types A B : {set gT}.
-Implicit Types G H K : {group gT}.
-Implicit Types C D : {set rT}.
-Implicit Type L : {group rT}.
+Implicit Types A B : {set gT}.
+Implicit Types G H K : {group gT}.
+Implicit Types C D : {set rT}.
+Implicit Type L : {group rT}.

Section defs.

-Variables (A B : {set gT}) (fA fB : gT → FinGroup.sort rT).
+Variables (A B : {set gT}) (fA fB : gT → FinGroup.sort rT).

-Definition pprodm of B \subset 'N(A) & {in A & B, morph_act 'J 'J fA fB}
-                  & {in A :&: B, fA =1 fB} :=
-  fun x ⇒ fA (divgr A B x) × fB (remgr A B x).
+Definition pprodm of B \subset 'N(A) & {in A & B, morph_act 'J 'J fA fB}
+                  & {in A :&: B, fA =1 fB} :=
+  fun x ⇒ fA (divgr A B x) × fB (remgr A B x).

End defs.
@@ -1018,45 +1017,45 @@ Section Props.

-Variables H K : {group gT}.
-Variables (fH : {morphism H >-> rT}) (fK : {morphism K >-> rT}).
-Hypothesis nHK : K \subset 'N(H).
-Hypothesis actf : {in H & K, morph_act 'J 'J fH fK}.
-Hypothesis eqfHK : {in H :&: K, fH =1 fK}.
+Variables H K : {group gT}.
+Variables (fH : {morphism H >-> rT}) (fK : {morphism K >-> rT}).
+Hypothesis nHK : K \subset 'N(H).
+Hypothesis actf : {in H & K, morph_act 'J 'J fH fK}.
+Hypothesis eqfHK : {in H :&: K, fH =1 fK}.


-Lemma pprodmE x a : x \in H → a \in K → f (x × a) = fH x × fK a.
+Lemma pprodmE x a : x \in H → a \in K → f (x × a) = fH x × fK a.

-Lemma pprodmEl : {in H, f =1 fH}.
+Lemma pprodmEl : {in H, f =1 fH}.

-Lemma pprodmEr : {in K, f =1 fK}.
+Lemma pprodmEr : {in K, f =1 fK}.

-Lemma pprodmM : {in H <*> K &, {morph f: x y / x × y}}.
+Lemma pprodmM : {in H <*> K &, {morph f: x y / x × y}}.

Canonical pprodm_morphism := Morphism pprodmM.

Lemma morphim_pprodm A B :
-  A \subset H → B \subset K → f @* (A × B) = fH @* A × fK @* B.
+  A \subset H → B \subset K → f @* (A × B) = fH @* A × fK @* B.

-Lemma morphim_pprodml A : A \subset H → f @* A = fH @* A.
+Lemma morphim_pprodml A : A \subset H → f @* A = fH @* A.

-Lemma morphim_pprodmr B : B \subset K → f @* B = fK @* B.
+Lemma morphim_pprodmr B : B \subset K → f @* B = fK @* B.

-Lemma ker_pprodm : 'ker f = [set x × a^-1 | x in H, a in K & fH x == fK a].
+Lemma ker_pprodm : 'ker f = [set x × a^-1 | x in H, a in K & fH x == fK a].

Lemma injm_pprodm :
-  'injm f = [&& 'injm fH, 'injm fK & fH @* H :&: fK @* K == fH @* K].
+  'injm f = [&& 'injm fH, 'injm fK & fH @* H :&: fK @* K == fH @* K].

End Props.
@@ -1065,56 +1064,56 @@ Section Sdprodm.

-Variables H K G : {group gT}.
-Variables (fH : {morphism H >-> rT}) (fK : {morphism K >-> rT}).
-Hypothesis eqHK_G : H ><| K = G.
-Hypothesis actf : {in H & K, morph_act 'J 'J fH fK}.
+Variables H K G : {group gT}.
+Variables (fH : {morphism H >-> rT}) (fK : {morphism K >-> rT}).
+Hypothesis eqHK_G : H ><| K = G.
+Hypothesis actf : {in H & K, morph_act 'J 'J fH fK}.

-Lemma sdprodm_norm : K \subset 'N(H).
+Lemma sdprodm_norm : K \subset 'N(H).

-Lemma sdprodm_sub : G \subset H <*> K.
+Lemma sdprodm_sub : G \subset H <*> K.

-Lemma sdprodm_eqf : {in H :&: K, fH =1 fK}.
+Lemma sdprodm_eqf : {in H :&: K, fH =1 fK}.

Definition sdprodm :=
  restrm sdprodm_sub (pprodm sdprodm_norm actf sdprodm_eqf).

-Canonical sdprodm_morphism := Eval hnf in [morphism of sdprodm].
+Canonical sdprodm_morphism := Eval hnf in [morphism of sdprodm].

-Lemma sdprodmE a b : a \in H → b \in K → sdprodm (a × b) = fH a × fK b.
+Lemma sdprodmE a b : a \in H → b \in K → sdprodm (a × b) = fH a × fK b.

-Lemma sdprodmEl a : a \in H → sdprodm a = fH a.
+Lemma sdprodmEl a : a \in H → sdprodm a = fH a.

-Lemma sdprodmEr b : b \in K → sdprodm b = fK b.
+Lemma sdprodmEr b : b \in K → sdprodm b = fK b.

Lemma morphim_sdprodm A B :
-  A \subset H → B \subset K → sdprodm @* (A × B) = fH @* A × fK @* B.
+  A \subset H → B \subset K → sdprodm @* (A × B) = fH @* A × fK @* B.

-Lemma im_sdprodm : sdprodm @* G = fH @* H × fK @* K.
+Lemma im_sdprodm : sdprodm @* G = fH @* H × fK @* K.

-Lemma morphim_sdprodml A : A \subset H → sdprodm @* A = fH @* A.
+Lemma morphim_sdprodml A : A \subset H → sdprodm @* A = fH @* A.

-Lemma morphim_sdprodmr B : B \subset K → sdprodm @* B = fK @* B.
+Lemma morphim_sdprodmr B : B \subset K → sdprodm @* B = fK @* B.

Lemma ker_sdprodm :
-  'ker sdprodm = [set a × b^-1 | a in H, b in K & fH a == fK b].
+  'ker sdprodm = [set a × b^-1 | a in H, b in K & fH a == fK b].

Lemma injm_sdprodm :
-  'injm sdprodm = [&& 'injm fH, 'injm fK & fH @* H :&: fK @* K == 1].
+  'injm sdprodm = [&& 'injm fH, 'injm fK & fH @* H :&: fK @* K == 1].

End Sdprodm.
@@ -1123,55 +1122,55 @@ Section Cprodm.

-Variables H K G : {group gT}.
-Variables (fH : {morphism H >-> rT}) (fK : {morphism K >-> rT}).
-Hypothesis eqHK_G : H \* K = G.
-Hypothesis cfHK : fK @* K \subset 'C(fH @* H).
-Hypothesis eqfHK : {in H :&: K, fH =1 fK}.
+Variables H K G : {group gT}.
+Variables (fH : {morphism H >-> rT}) (fK : {morphism K >-> rT}).
+Hypothesis eqHK_G : H \* K = G.
+Hypothesis cfHK : fK @* K \subset 'C(fH @* H).
+Hypothesis eqfHK : {in H :&: K, fH =1 fK}.

-Lemma cprodm_norm : K \subset 'N(H).
+Lemma cprodm_norm : K \subset 'N(H).

-Lemma cprodm_sub : G \subset H <*> K.
+Lemma cprodm_sub : G \subset H <*> K.

-Lemma cprodm_actf : {in H & K, morph_act 'J 'J fH fK}.
+Lemma cprodm_actf : {in H & K, morph_act 'J 'J fH fK}.

Definition cprodm := restrm cprodm_sub (pprodm cprodm_norm cprodm_actf eqfHK).

-Canonical cprodm_morphism := Eval hnf in [morphism of cprodm].
+Canonical cprodm_morphism := Eval hnf in [morphism of cprodm].

-Lemma cprodmE a b : a \in H → b \in K → cprodm (a × b) = fH a × fK b.
+Lemma cprodmE a b : a \in H → b \in K → cprodm (a × b) = fH a × fK b.

-Lemma cprodmEl a : a \in H → cprodm a = fH a.
+Lemma cprodmEl a : a \in H → cprodm a = fH a.

-Lemma cprodmEr b : b \in K → cprodm b = fK b.
+Lemma cprodmEr b : b \in K → cprodm b = fK b.

Lemma morphim_cprodm A B :
-  A \subset H → B \subset K → cprodm @* (A × B) = fH @* A × fK @* B.
+  A \subset H → B \subset K → cprodm @* (A × B) = fH @* A × fK @* B.

-Lemma im_cprodm : cprodm @* G = fH @* H × fK @* K.
+Lemma im_cprodm : cprodm @* G = fH @* H × fK @* K.

-Lemma morphim_cprodml A : A \subset H → cprodm @* A = fH @* A.
+Lemma morphim_cprodml A : A \subset H → cprodm @* A = fH @* A.

-Lemma morphim_cprodmr B : B \subset K → cprodm @* B = fK @* B.
+Lemma morphim_cprodmr B : B \subset K → cprodm @* B = fK @* B.

-Lemma ker_cprodm : 'ker cprodm = [set a × b^-1 | a in H, b in K & fH a == fK b].
+Lemma ker_cprodm : 'ker cprodm = [set a × b^-1 | a in H, b in K & fH a == fK b].

Lemma injm_cprodm :
-  'injm cprodm = [&& 'injm fH, 'injm fK & fH @* H :&: fK @* K == fH @* K].
+  'injm cprodm = [&& 'injm fH, 'injm fK & fH @* H :&: fK @* K == fH @* K].

End Cprodm.
@@ -1180,58 +1179,58 @@ Section Dprodm.

-Variables G H K : {group gT}.
-Variables (fH : {morphism H >-> rT}) (fK : {morphism K >-> rT}).
-Hypothesis eqHK_G : H \x K = G.
-Hypothesis cfHK : fK @* K \subset 'C(fH @* H).
+Variables G H K : {group gT}.
+Variables (fH : {morphism H >-> rT}) (fK : {morphism K >-> rT}).
+Hypothesis eqHK_G : H \x K = G.
+Hypothesis cfHK : fK @* K \subset 'C(fH @* H).

-Lemma dprodm_cprod : H \* K = G.
+Lemma dprodm_cprod : H \* K = G.

-Lemma dprodm_eqf : {in H :&: K, fH =1 fK}.
+Lemma dprodm_eqf : {in H :&: K, fH =1 fK}.

Definition dprodm := cprodm dprodm_cprod cfHK dprodm_eqf.

-Canonical dprodm_morphism := Eval hnf in [morphism of dprodm].
+Canonical dprodm_morphism := Eval hnf in [morphism of dprodm].

-Lemma dprodmE a b : a \in H → b \in K → dprodm (a × b) = fH a × fK b.
+Lemma dprodmE a b : a \in H → b \in K → dprodm (a × b) = fH a × fK b.

-Lemma dprodmEl a : a \in H → dprodm a = fH a.
+Lemma dprodmEl a : a \in H → dprodm a = fH a.

-Lemma dprodmEr b : b \in K → dprodm b = fK b.
+Lemma dprodmEr b : b \in K → dprodm b = fK b.

Lemma morphim_dprodm A B :
-  A \subset H → B \subset K → dprodm @* (A × B) = fH @* A × fK @* B.
+  A \subset H → B \subset K → dprodm @* (A × B) = fH @* A × fK @* B.

-Lemma im_dprodm : dprodm @* G = fH @* H × fK @* K.
+Lemma im_dprodm : dprodm @* G = fH @* H × fK @* K.

-Lemma morphim_dprodml A : A \subset H → dprodm @* A = fH @* A.
+Lemma morphim_dprodml A : A \subset H → dprodm @* A = fH @* A.

-Lemma morphim_dprodmr B : B \subset K → dprodm @* B = fK @* B.
+Lemma morphim_dprodmr B : B \subset K → dprodm @* B = fK @* B.

-Lemma ker_dprodm : 'ker dprodm = [set a × b^-1 | a in H, b in K & fH a == fK b].
+Lemma ker_dprodm : 'ker dprodm = [set a × b^-1 | a in H, b in K & fH a == fK b].

Lemma injm_dprodm :
-  'injm dprodm = [&& 'injm fH, 'injm fK & fH @* H :&: fK @* K == 1].
+  'injm dprodm = [&& 'injm fH, 'injm fK & fH @* H :&: fK @* K == 1].

End Dprodm.

Lemma isog_dprod A B G C D L :
-  A \x B = G → C \x D = L → isog A C → isog B D → isog G L.
+  A \x B = G → C \x D = L → isog A C → isog B D → isog G L.

End ProdMorph.
@@ -1241,41 +1240,41 @@
Variables gT aT rT : finGroupType.
-Variables (H : {group gT}) (K : {group aT}) (to : groupAction K H).
-Variables (fH : {morphism H >-> rT}) (fK : {morphism K >-> rT}).
+Variables (H : {group gT}) (K : {group aT}) (to : groupAction K H).
+Variables (fH : {morphism H >-> rT}) (fK : {morphism K >-> rT}).

-Hypothesis actf : {in H & K, morph_act to 'J fH fK}.
+Hypothesis actf : {in H & K, morph_act to 'J fH fK}.

-Let DgH := sdpair1 to @* H.
-Let DgK := sdpair2 to @* K.
+Let DgH := sdpair1 to @* H.
+Let DgK := sdpair2 to @* K.

-Lemma xsdprodm_dom1 : DgH \subset 'dom fsH.
+Lemma xsdprodm_dom1 : DgH \subset 'dom fsH.

-Lemma xsdprodm_dom2 : DgK \subset 'dom fsK.
+Lemma xsdprodm_dom2 : DgK \subset 'dom fsK.

-Lemma im_sdprodm1 : gH @* DgH = fH @* H.
+Lemma im_sdprodm1 : gH @* DgH = fH @* H.

-Lemma im_sdprodm2 : gK @* DgK = fK @* K.
+Lemma im_sdprodm2 : gK @* DgK = fK @* K.

-Lemma xsdprodm_act : {in DgH & DgK, morph_act 'J 'J gH gK}.
+Lemma xsdprodm_act : {in DgH & DgK, morph_act 'J 'J gH gK}.

Definition xsdprodm := sdprodm (sdprod_sdpair to) xsdprodm_act.
-Canonical xsdprod_morphism := [morphism of xsdprodm].
+Canonical xsdprod_morphism := [morphism of xsdprodm].

-Lemma im_xsdprodm : xsdprodm @* setT = fH @* H × fK @* K.
+Lemma im_xsdprodm : xsdprodm @* setT = fH @* H × fK @* K.

Lemma injm_xsdprodm :
-  'injm xsdprodm = [&& 'injm fH, 'injm fK & fH @* H :&: fK @* K == 1].
+  'injm xsdprodm = [&& 'injm fH, 'injm fK & fH @* H :&: fK @* K == 1].

End ExtSdprodm.
@@ -1285,16 +1284,16 @@
Variable gT : finGroupType.
-Implicit Types G H : {group gT}.
+Implicit Types G H : {group gT}.

-Definition mulgm : gT × gT → _ := prod_curry mulg.
+Definition mulgm : gT × gT → _ := prod_curry mulg.

-Lemma imset_mulgm (A B : {set gT}) : mulgm @: setX A B = A × B.
+Lemma imset_mulgm (A B : {set gT}) : mulgm @: setX A B = A × B.

-Lemma mulgmP H1 H2 G : reflect (H1 \x H2 = G) (misom (setX H1 H2) G mulgm).
+Lemma mulgmP H1 H2 G : reflect (H1 \x H2 = G) (misom (setX H1 H2) G mulgm).

End DirprodIsom.
-- cgit v1.2.3