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.solvable.commutator.html | 165 ++++++++++++-------------
1 file changed, 82 insertions(+), 83 deletions(-)
(limited to 'docs/htmldoc/mathcomp.solvable.commutator.html')
diff --git a/docs/htmldoc/mathcomp.solvable.commutator.html b/docs/htmldoc/mathcomp.solvable.commutator.html
index 9da2584..b159af9 100644
--- a/docs/htmldoc/mathcomp.solvable.commutator.html
+++ b/docs/htmldoc/mathcomp.solvable.commutator.html
@@ -21,7 +21,6 @@
@@ -48,8 +47,8 @@
Import GroupScope.
-Definition derived_at_rec n (gT : finGroupType) (A : {set gT}) :=
- iter n (fun B ⇒ [~: B, B]) A.
+Definition derived_at_rec n (gT : finGroupType) (A : {set gT}) :=
+ iter n (fun B ⇒ [~: B, B]) A.
@@ -59,26 +58,26 @@
"cooking" destroys it.
-
Definition derived_at :=
nosimpl derived_at_rec.
+
Definition derived_at :=
nosimpl derived_at_rec.
-
Notation "G ^` ( n )" := (
derived_at n G) :
group_scope.
+
Notation "G ^` ( n )" := (
derived_at n G) :
group_scope.
Section DerivedBasics.
Variables gT :
finGroupType.
-
Implicit Type A :
{set gT}.
-
Implicit Types G :
{group gT}.
+
Implicit Type A :
{set gT}.
+
Implicit Types G :
{group gT}.
-
Lemma derg0 A :
A^`(0
) = A.
-
Lemma derg1 A :
A^`(1
) = [~: A, A].
-
Lemma dergSn n A :
A^`(n.+1) = [~: A^`(n), A^`(n)].
+
Lemma derg0 A :
A^`(0
) = A.
+
Lemma derg1 A :
A^`(1
) = [~: A, A].
+
Lemma dergSn n A :
A^`(n.+1) = [~: A^`(n), A^`(n)].
-
Lemma der_group_set G n :
group_set G^`(n).
+
Lemma der_group_set G n :
group_set G^`(n).
Canonical derived_at_group G n :=
Group (
der_group_set G n).
@@ -87,7 +86,7 @@
End DerivedBasics.
-
Notation "G ^` ( n )" := (
derived_at_group G n) :
Group_scope.
+
Notation "G ^` ( n )" := (
derived_at_group G n) :
Group_scope.
Section Basic_commutator_properties.
@@ -97,26 +96,26 @@
Implicit Types x y z :
gT.
-
Lemma conjg_mulR x y :
x ^ y = x × [~ x, y].
+
Lemma conjg_mulR x y :
x ^ y = x × [~ x, y].
-
Lemma conjg_Rmul x y :
x ^ y = [~ y, x^-1] × x.
+
Lemma conjg_Rmul x y :
x ^ y = [~ y, x^-1] × x.
-
Lemma commMgJ x y z :
[~ x × y, z] = [~ x, z] ^ y × [~ y, z].
+
Lemma commMgJ x y z :
[~ x × y, z] = [~ x, z] ^ y × [~ y, z].
-
Lemma commgMJ x y z :
[~ x, y × z] = [~ x, z] × [~ x, y] ^ z.
+
Lemma commgMJ x y z :
[~ x, y × z] = [~ x, z] × [~ x, y] ^ z.
-
Lemma commMgR x y z :
[~ x × y, z] = [~ x, z] × [~ x, z, y] × [~ y, z].
+
Lemma commMgR x y z :
[~ x × y, z] = [~ x, z] × [~ x, z, y] × [~ y, z].
-
Lemma commgMR x y z :
[~ x, y × z] = [~ x, z] × [~ x, y] × [~ x, y, z].
+
Lemma commgMR x y z :
[~ x, y × z] = [~ x, z] × [~ x, y] × [~ x, y, z].
Lemma Hall_Witt_identity x y z :
-
[~ x, y^-1, z] ^ y × [~ y, z^-1, x] ^ z × [~ z, x^-1, y] ^ x = 1.
+
[~ x, y^-1, z] ^ y × [~ y, z^-1, x] ^ z × [~ z, x^-1, y] ^ x = 1.
-Variables (i : nat) (x y : gT).
-Hypothesis cxz : commute x [~ x, y].
+Variables (i : nat) (x y : gT).
+Hypothesis cxz : commute x [~ x, y].
-Lemma commVg : [~ x^-1, y] = [~ x, y]^-1.
+Lemma commVg : [~ x^-1, y] = [~ x, y]^-1.
-Lemma commXg : [~ x ^+ i, y] = [~ x, y] ^+ i.
+Lemma commXg : [~ x ^+ i, y] = [~ x, y] ^+ i.
End LeftComm.
@@ -146,15 +145,15 @@
Section RightComm.
-Variables (i : nat) (x y : gT).
-Hypothesis cyz : commute y [~ x, y].
+Variables (i : nat) (x y : gT).
+Hypothesis cyz : commute y [~ x, y].
Let cyz' := commuteV cyz.
-Lemma commgV : [~ x, y^-1] = [~ x, y]^-1.
+Lemma commgV : [~ x, y^-1] = [~ x, y]^-1.
-Lemma commgX : [~ x, y ^+ i] = [~ x, y] ^+ i.
+Lemma commgX : [~ x, y ^+ i] = [~ x, y] ^+ i.
End RightComm.
@@ -163,14 +162,14 @@
Section LeftRightComm.
-Variables (i j : nat) (x y : gT).
-Hypotheses (cxz : commute x [~ x, y]) (cyz : commute y [~ x, y]).
+Variables (i j : nat) (x y : gT).
+Hypotheses (cxz : commute x [~ x, y]) (cyz : commute y [~ x, y]).
-Lemma commXXg : [~ x ^+ i, y ^+ j] = [~ x, y] ^+ (i × j).
+Lemma commXXg : [~ x ^+ i, y ^+ j] = [~ x, y] ^+ (i × j).
-Lemma expMg_Rmul : (y × x) ^+ i = y ^+ i × x ^+ i × [~ x, y] ^+ 'C(i, 2).
+Lemma expMg_Rmul : (y × x) ^+ i = y ^+ i × x ^+ i × [~ x, y] ^+ 'C(i, 2).
End LeftRightComm.
@@ -189,98 +188,98 @@
Variable gT : finGroupType.
-Implicit Type (rT : finGroupType) (A B C : {set gT}) (D G H K : {group gT}).
+Implicit Type (rT : finGroupType) (A B C : {set gT}) (D G H K : {group gT}).
-Lemma commG1 A : [~: A, 1] = 1.
+Lemma commG1 A : [~: A, 1] = 1.
-Lemma comm1G A : [~: 1, A] = 1.
+Lemma comm1G A : [~: 1, A] = 1.
-Lemma commg_sub A B : [~: A, B] \subset A <*> B.
+Lemma commg_sub A B : [~: A, B] \subset A <*> B.
-Lemma commg_norml G A : G \subset 'N([~: G, A]).
+Lemma commg_norml G A : G \subset 'N([~: G, A]).
-Lemma commg_normr G A : G \subset 'N([~: A, G]).
+Lemma commg_normr G A : G \subset 'N([~: A, G]).
-Lemma commg_norm G H : G <*> H \subset 'N([~: G, H]).
+Lemma commg_norm G H : G <*> H \subset 'N([~: G, H]).
-Lemma commg_normal G H : [~: G, H] <| G <*> H.
+Lemma commg_normal G H : [~: G, H] <| G <*> H.
-Lemma normsRl A G B : A \subset G → A \subset 'N([~: G, B]).
+Lemma normsRl A G B : A \subset G → A \subset 'N([~: G, B]).
-Lemma normsRr A G B : A \subset G → A \subset 'N([~: B, G]).
+Lemma normsRr A G B : A \subset G → A \subset 'N([~: B, G]).
-Lemma commg_subr G H : ([~: G, H] \subset H) = (G \subset 'N(H)).
+Lemma commg_subr G H : ([~: G, H] \subset H) = (G \subset 'N(H)).
-Lemma commg_subl G H : ([~: G, H] \subset G) = (H \subset 'N(G)).
+Lemma commg_subl G H : ([~: G, H] \subset G) = (H \subset 'N(G)).
Lemma commg_subI A B G H :
- A \subset 'N_G(H) → B \subset 'N_H(G) → [~: A, B] \subset G :&: H.
+ A \subset 'N_G(H) → B \subset 'N_H(G) → [~: A, B] \subset G :&: H.
Lemma quotient_cents2 A B K :
- A \subset 'N(K) → B \subset 'N(K) →
- (A / K \subset 'C(B / K)) = ([~: A, B] \subset K).
+ A \subset 'N(K) → B \subset 'N(K) →
+ (A / K \subset 'C(B / K)) = ([~: A, B] \subset K).
Lemma quotient_cents2r A B K :
- [~: A, B] \subset K → (A / K) \subset 'C(B / K).
+ [~: A, B] \subset K → (A / K) \subset 'C(B / K).
-Lemma sub_der1_norm G H : G^`(1) \subset H → H \subset G → G \subset 'N(H).
+Lemma sub_der1_norm G H : G^`(1) \subset H → H \subset G → G \subset 'N(H).
-Lemma sub_der1_normal G H : G^`(1) \subset H → H \subset G → H <| G.
+Lemma sub_der1_normal G H : G^`(1) \subset H → H \subset G → H <| G.
-Lemma sub_der1_abelian G H : G^`(1) \subset H → abelian (G / H).
+Lemma sub_der1_abelian G H : G^`(1) \subset H → abelian (G / H).
-Lemma der1_min G H : G \subset 'N(H) → abelian (G / H) → G^`(1) \subset H.
+Lemma der1_min G H : G \subset 'N(H) → abelian (G / H) → G^`(1) \subset H.
-Lemma der_abelian n G : abelian (G^`(n) / G^`(n.+1)).
+Lemma der_abelian n G : abelian (G^`(n) / G^`(n.+1)).
-Lemma commg_normSl G H K : G \subset 'N(H) → [~: G, H] \subset 'N([~: K, H]).
+Lemma commg_normSl G H K : G \subset 'N(H) → [~: G, H] \subset 'N([~: K, H]).
-Lemma commg_normSr G H K : G \subset 'N(H) → [~: H, G] \subset 'N([~: H, K]).
+Lemma commg_normSr G H K : G \subset 'N(H) → [~: H, G] \subset 'N([~: H, K]).
-Lemma commMGr G H K : [~: G, K] × [~: H, K] \subset [~: G × H , K].
+Lemma commMGr G H K : [~: G, K] × [~: H, K] \subset [~: G × H , K].
Lemma commMG G H K :
- H \subset 'N([~: G, K]) → [~: G × H , K] = [~: G, K] × [~: H, K].
+ H \subset 'N([~: G, K]) → [~: G × H , K] = [~: G, K] × [~: H, K].
Lemma comm3G1P A B C :
- reflect {in A & B & C, ∀ h k l, [~ h, k, l] = 1} ([~: A, B, C] :==: 1).
+ reflect {in A & B & C, ∀ h k l, [~ h, k, l] = 1} ([~: A, B, C] :==: 1).
Lemma three_subgroup G H K :
- [~: G, H, K] :=: 1 → [~: H, K, G] :=: 1→ [~: K, G, H] :=: 1.
+ [~: G, H, K] :=: 1 → [~: H, K, G] :=: 1→ [~: K, G, H] :=: 1.
Lemma der1_joing_cycles (x y : gT) :
- let XY := <[x]> <*> <[y]> in let xy := [~ x, y] in
- xy \in 'C(XY) → XY^`(1) = <[xy]>.
+ let XY := <[x]> <*> <[y]> in let xy := [~ x, y] in
+ xy \in 'C(XY) → XY^`(1) = <[xy]>.
-Lemma commgAC G x y z : x \in G → y \in G → z \in G →
- commute y z → abelian [~: [set x], G] → [~ x, y, z] = [~ x, z, y].
+Lemma commgAC G x y z : x \in G → y \in G → z \in G →
+ commute y z → abelian [~: [set x], G] → [~ x, y, z] = [~ x, z, y].
@@ -290,45 +289,45 @@
--
cgit v1.2.3