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.abelian.html | 629 ++++++++++++++--------------
1 file changed, 314 insertions(+), 315 deletions(-)
(limited to 'docs/htmldoc/mathcomp.solvable.abelian.html')
diff --git a/docs/htmldoc/mathcomp.solvable.abelian.html b/docs/htmldoc/mathcomp.solvable.abelian.html
index 038d7d9..5efbaa9 100644
--- a/docs/htmldoc/mathcomp.solvable.abelian.html
+++ b/docs/htmldoc/mathcomp.solvable.abelian.html
@@ -21,7 +21,6 @@
@@ -107,40 +106,40 @@
Variable gT : finGroupType.
-Implicit Types (x : gT) (A B : {set gT}) (pi : nat_pred) (p n : nat).
+Implicit Types (x : gT) (A B : {set gT}) (pi : nat_pred) (p n : nat).
-Definition Ldiv n := [set x : gT | x ^+ n == 1].
+Definition Ldiv n := [set x : gT | x ^+ n == 1].
-Definition exponent A := \big[lcmn/1%N]_(x in A) #[x].
+Definition exponent A := \big[lcmn/1%N]_(x in A) #[x].
-Definition abelem p A := [&& p.-group A, abelian A & exponent A %| p].
+Definition abelem p A := [&& p.-group A, abelian A & exponent A %| p].
-Definition is_abelem A := abelem (pdiv #|A|) A.
+Definition is_abelem A := abelem (pdiv #|A|) A.
-Definition pElem p A := [set E : {group gT} | E \subset A & abelem p E].
+Definition pElem p A := [set E : {group gT} | E \subset A & abelem p E].
-Definition pnElem p n A := [set E in pElem p A | logn p #|E| == n].
+Definition pnElem p n A := [set E in pElem p A | logn p #|E| == n].
-Definition nElem n A := \bigcup_(0 ≤ p < #|A|.+1) pnElem p n A.
+Definition nElem n A := \bigcup_(0 ≤ p < #|A|.+1) pnElem p n A.
-Definition pmaxElem p A := [set E | [max E | E \in pElem p A]].
+Definition pmaxElem p A := [set E | [max E | E \in pElem p A]].
-Definition p_rank p A := \max_(E in pElem p A) logn p #|E|.
+Definition p_rank p A := \max_(E in pElem p A) logn p #|E|.
-Definition rank A := \max_(0 ≤ p < #|A|.+1) p_rank p A.
+Definition rank A := \max_(0 ≤ p < #|A|.+1) p_rank p A.
-Definition gen_rank A := #|[arg min_(B < A | <<B>> == A) #|B|]|.
+Definition gen_rank A := #|[arg min_(B < A | <<B>> == A) #|B|]|.
@@ -157,45 +156,45 @@
-Notation "''Ldiv_' n " := (Ldiv _ n)
+Notation "''Ldiv_' n " := (Ldiv _ n)
(at level 8, n at level 2, format "''Ldiv_' n ") : group_scope.
-Notation "''Ldiv_' n ( G )" := (G :&: 'Ldiv_n)
+Notation "''Ldiv_' n ( G )" := (G :&: 'Ldiv_n)
(at level 8, n at level 2, format "''Ldiv_' n ( G )") : group_scope.
-Notation "p .-abelem" := (abelem p)
+Notation "p .-abelem" := (abelem p)
(at level 2, format "p .-abelem") : group_scope.
-Notation "''E_' p ( G )" := (pElem p G)
+Notation "''E_' p ( G )" := (pElem p G)
(at level 8, p at level 2, format "''E_' p ( G )") : group_scope.
-Notation "''E_' p ^ n ( G )" := (pnElem p n G)
+Notation "''E_' p ^ n ( G )" := (pnElem p n G)
(at level 8, p, n at level 2, format "''E_' p ^ n ( G )") : group_scope.
-Notation "''E' ^ n ( G )" := (nElem n G)
+Notation "''E' ^ n ( G )" := (nElem n G)
(at level 8, n at level 2, format "''E' ^ n ( G )") : group_scope.
-Notation "''E*_' p ( G )" := (pmaxElem p G)
+Notation "''E*_' p ( G )" := (pmaxElem p G)
(at level 8, p at level 2, format "''E*_' p ( G )") : group_scope.
-Notation "''m' ( A )" := (gen_rank A)
+Notation "''m' ( A )" := (gen_rank A)
(at level 8, format "''m' ( A )") : group_scope.
-Notation "''r' ( A )" := (rank A)
+Notation "''r' ( A )" := (rank A)
(at level 8, format "''r' ( A )") : group_scope.
-Notation "''r_' p ( A )" := (p_rank p A)
+Notation "''r_' p ( A )" := (p_rank p A)
(at level 8, p at level 2, format "''r_' p ( A )") : group_scope.
@@ -210,27 +209,27 @@
-
Variables (
n :
nat) (
gT :
finGroupType) (
A :
{set gT}).
+
Variables (
n :
nat) (
gT :
finGroupType) (
A :
{set gT}).
-
Definition Ohm :=
<<[set x in A | x ^+ (pdiv #[x] ^ n) == 1
]>>.
+
Definition Ohm :=
<<[set x in A | x ^+ (pdiv #[x] ^ n) == 1
]>>.
-
Definition Mho :=
<<[set x ^+ (pdiv #[x] ^ n) | x in A & (pdiv #[x]).-elt x]>>.
+
Definition Mho :=
<<[set x ^+ (pdiv #[x] ^ n) | x in A & (pdiv #[x]).-elt x]>>.
-
Canonical Ohm_group :
{group gT} :=
Eval hnf in [group of Ohm].
-
Canonical Mho_group :
{group gT} :=
Eval hnf in [group of Mho].
+
Canonical Ohm_group :
{group gT} :=
Eval hnf in [group of Ohm].
+
Canonical Mho_group :
{group gT} :=
Eval hnf in [group of Mho].
-
Lemma pdiv_p_elt (
p :
nat) (
x :
gT) :
p.-elt x → x != 1
→ pdiv #[x] = p.
+
Lemma pdiv_p_elt (
p :
nat) (
x :
gT) :
p.-elt x → x != 1
→ pdiv #[x] = p.
Lemma OhmPredP (
x :
gT) :
-
reflect (
exists2 p, prime p & x ^+ (p ^ n) = 1) (
x ^+ (pdiv #[x] ^ n) == 1).
+
reflect (
exists2 p, prime p & x ^+ (p ^ n) = 1) (
x ^+ (pdiv #[x] ^ n) == 1).
-
Lemma Mho_p_elt (
p :
nat)
x :
x \in A → p.-elt x → x ^+ (p ^ n) \in Mho.
+
Lemma Mho_p_elt (
p :
nat)
x :
x \in A → p.-elt x → x ^+ (p ^ n) \in Mho.
End Functors.
@@ -238,349 +237,349 @@
-
Notation "''Ohm_' n ( G )" := (
Ohm n G)
+
Notation "''Ohm_' n ( G )" := (
Ohm n G)
(
at level 8,
n at level 2,
format "''Ohm_' n ( G )") :
group_scope.
-
Notation "''Ohm_' n ( G )" := (
Ohm_group n G) :
Group_scope.
+
Notation "''Ohm_' n ( G )" := (
Ohm_group n G) :
Group_scope.
-
Notation "''Mho^' n ( G )" := (
Mho n G)
+
Notation "''Mho^' n ( G )" := (
Mho n G)
(
at level 8,
n at level 2,
format "''Mho^' n ( G )") :
group_scope.
-
Notation "''Mho^' n ( G )" := (
Mho_group n G) :
Group_scope.
+
Notation "''Mho^' n ( G )" := (
Mho_group n G) :
Group_scope.
Section ExponentAbelem.
Variable gT :
finGroupType.
-
Implicit Types (
p n :
nat) (
pi :
nat_pred) (
x :
gT) (
A B C :
{set gT}).
-
Implicit Types E G H K P X Y :
{group gT}.
+
Implicit Types (
p n :
nat) (
pi :
nat_pred) (
x :
gT) (
A B C :
{set gT}).
+
Implicit Types E G H K P X Y :
{group gT}.
-
Lemma LdivP A n x :
reflect (
x \in A ∧ x ^+ n = 1) (
x \in 'Ldiv_n(A)).
+
Lemma LdivP A n x :
reflect (
x \in A ∧ x ^+ n = 1) (
x \in 'Ldiv_n(A)).
-
Lemma dvdn_exponent x A :
x \in A → #[x] %| exponent A.
+
Lemma dvdn_exponent x A :
x \in A → #[x] %| exponent A.
-
Lemma expg_exponent x A :
x \in A → x ^+ exponent A = 1.
+
Lemma expg_exponent x A :
x \in A → x ^+ exponent A = 1.
-
Lemma exponentS A B :
A \subset B → exponent A %| exponent B.
+
Lemma exponentS A B :
A \subset B → exponent A %| exponent B.
Lemma exponentP A n :
-
reflect (
∀ x,
x \in A → x ^+ n = 1) (
exponent A %| n).
+
reflect (
∀ x,
x \in A → x ^+ n = 1) (
exponent A %| n).
-
Lemma trivg_exponent G :
(G :==: 1
) = (exponent G %| 1
).
+
Lemma trivg_exponent G :
(G :==: 1
) = (exponent G %| 1
).
-
Lemma exponent1 :
exponent [1 gT] = 1%
N.
+
Lemma exponent1 :
exponent [1 gT] = 1%
N.
-
Lemma exponent_dvdn G :
exponent G %| #|G|.
+
Lemma exponent_dvdn G :
exponent G %| #|G|.
-
Lemma exponent_gt0 G : 0
< exponent G.
-
Hint Resolve exponent_gt0.
+
Lemma exponent_gt0 G : 0
< exponent G.
+
Hint Resolve exponent_gt0 :
core.
-
Lemma pnat_exponent pi G :
pi.-nat (
exponent G)
= pi.-group G.
+
Lemma pnat_exponent pi G :
pi.-nat (
exponent G)
= pi.-group G.
-
Lemma exponentJ A x :
exponent (
A :^ x)
= exponent A.
+
Lemma exponentJ A x :
exponent (
A :^ x)
= exponent A.
-
Lemma exponent_witness G :
nilpotent G → {x | x \in G & exponent G = #[x]}.
+
Lemma exponent_witness G :
nilpotent G → {x | x \in G & exponent G = #[x]}.
-
Lemma exponent_cycle x :
exponent <[x]> = #[x].
+
Lemma exponent_cycle x :
exponent <[x]> = #[x].
-
Lemma exponent_cyclic X :
cyclic X → exponent X = #|X|.
+
Lemma exponent_cyclic X :
cyclic X → exponent X = #|X|.
-
Lemma primes_exponent G :
primes (
exponent G)
= primes (
#|G|).
+
Lemma primes_exponent G :
primes (
exponent G)
= primes (
#|G|).
-
Lemma pi_of_exponent G :
\pi(exponent G) = \pi(G).
+
Lemma pi_of_exponent G :
\pi(exponent G) = \pi(G).
Lemma partn_exponentS pi H G :
-
H \subset G → #|G|`_pi %| #|H| → (exponent H)`_pi = (exponent G)`_pi.
+
H \subset G → #|G|`_pi %| #|H| → (exponent H)`_pi = (exponent G)`_pi.
-
Lemma exponent_Hall pi G H :
pi.-Hall(G) H → exponent H = (exponent G)`_pi.
+
Lemma exponent_Hall pi G H :
pi.-Hall(G) H → exponent H = (exponent G)`_pi.
-
Lemma exponent_Zgroup G :
Zgroup G → exponent G = #|G|.
+
Lemma exponent_Zgroup G :
Zgroup G → exponent G = #|G|.
Lemma cprod_exponent A B G :
-
A \* B = G → lcmn (
exponent A) (
exponent B)
= (exponent G).
+
A \* B = G → lcmn (
exponent A) (
exponent B)
= (exponent G).
Lemma dprod_exponent A B G :
-
A \x B = G → lcmn (
exponent A) (
exponent B)
= (exponent G).
+
A \x B = G → lcmn (
exponent A) (
exponent B)
= (exponent G).
-
Lemma sub_LdivT A n :
(A \subset 'Ldiv_n) = (exponent A %| n).
+
Lemma sub_LdivT A n :
(A \subset 'Ldiv_n) = (exponent A %| n).
-
Lemma LdivT_J n x :
'Ldiv_n :^ x = 'Ldiv_n.
+
Lemma LdivT_J n x :
'Ldiv_n :^ x = 'Ldiv_n.
-
Lemma LdivJ n A x :
'Ldiv_n(A :^ x) = 'Ldiv_n(A) :^ x.
+
Lemma LdivJ n A x :
'Ldiv_n(A :^ x) = 'Ldiv_n(A) :^ x.
-
Lemma sub_Ldiv A n :
(A \subset 'Ldiv_n(A)) = (exponent A %| n).
+
Lemma sub_Ldiv A n :
(A \subset 'Ldiv_n(A)) = (exponent A %| n).
-
Lemma group_Ldiv G n :
abelian G → group_set 'Ldiv_n(G).
+
Lemma group_Ldiv G n :
abelian G → group_set 'Ldiv_n(G).
-
Lemma abelian_exponent_gen A :
abelian A → exponent <<A>> = exponent A.
+
Lemma abelian_exponent_gen A :
abelian A → exponent <<A>> = exponent A.
-
Lemma abelem_pgroup p A :
p.-abelem A → p.-group A.
+
Lemma abelem_pgroup p A :
p.-abelem A → p.-group A.
-
Lemma abelem_abelian p A :
p.-abelem A → abelian A.
+
Lemma abelem_abelian p A :
p.-abelem A → abelian A.
-
Lemma abelem1 p :
p.-abelem [1 gT].
+
Lemma abelem1 p :
p.-abelem [1 gT].
-
Lemma abelemE p G :
prime p → p.-abelem G = abelian G && (exponent G %| p).
+
Lemma abelemE p G :
prime p → p.-abelem G = abelian G && (exponent G %| p).
Lemma abelemP p G :
-
prime p →
-
reflect (
abelian G ∧ ∀ x,
x \in G → x ^+ p = 1) (
p.-abelem G).
+
prime p →
+
reflect (
abelian G ∧ ∀ x,
x \in G → x ^+ p = 1) (
p.-abelem G).
-
Lemma abelem_order_p p G x :
p.-abelem G → x \in G → x != 1
→ #[x] = p.
+
Lemma abelem_order_p p G x :
p.-abelem G → x \in G → x != 1
→ #[x] = p.
-
Lemma cyclic_abelem_prime p X :
p.-abelem X → cyclic X → X :!=: 1
→ #|X| = p.
+
Lemma cyclic_abelem_prime p X :
p.-abelem X → cyclic X → X :!=: 1
→ #|X| = p.
-
Lemma cycle_abelem p x :
p.-elt x || prime p → p.-abelem <[x]> = (#[x] %| p).
+
Lemma cycle_abelem p x :
p.-elt x || prime p → p.-abelem <[x]> = (#[x] %| p).
-
Lemma exponent2_abelem G :
exponent G %| 2
→ 2
.-abelem G.
+
Lemma exponent2_abelem G :
exponent G %| 2
→ 2
.-abelem G.
-
Lemma prime_abelem p G :
prime p → #|G| = p → p.-abelem G.
+
Lemma prime_abelem p G :
prime p → #|G| = p → p.-abelem G.
-
Lemma abelem_cyclic p G :
p.-abelem G → cyclic G = (logn p #|G| ≤ 1
).
+
Lemma abelem_cyclic p G :
p.-abelem G → cyclic G = (logn p #|G| ≤ 1
).
-
Lemma abelemS p H G :
H \subset G → p.-abelem G → p.-abelem H.
+
Lemma abelemS p H G :
H \subset G → p.-abelem G → p.-abelem H.
-
Lemma abelemJ p G x :
p.-abelem (
G :^ x)
= p.-abelem G.
+
Lemma abelemJ p G x :
p.-abelem (
G :^ x)
= p.-abelem G.
Lemma cprod_abelem p A B G :
-
A \* B = G → p.-abelem G = p.-abelem A && p.-abelem B.
+
A \* B = G → p.-abelem G = p.-abelem A && p.-abelem B.
Lemma dprod_abelem p A B G :
-
A \x B = G → p.-abelem G = p.-abelem A && p.-abelem B.
+
A \x B = G → p.-abelem G = p.-abelem A && p.-abelem B.
-
Lemma is_abelem_pgroup p G :
p.-group G → is_abelem G = p.-abelem G.
+
Lemma is_abelem_pgroup p G :
p.-group G → is_abelem G = p.-abelem G.
-
Lemma is_abelemP G :
reflect (
exists2 p, prime p & p.-abelem G) (
is_abelem G).
+
Lemma is_abelemP G :
reflect (
exists2 p, prime p & p.-abelem G) (
is_abelem G).
-
Lemma pElemP p A E :
reflect (
E \subset A ∧ p.-abelem E) (
E \in 'E_p(A)).
+
Lemma pElemP p A E :
reflect (
E \subset A ∧ p.-abelem E) (
E \in 'E_p(A)).
-
Lemma pElemS p A B :
A \subset B → 'E_p(A) \subset 'E_p(B).
+
Lemma pElemS p A B :
A \subset B → 'E_p(A) \subset 'E_p(B).
-
Lemma pElemI p A B :
'E_p(A :&: B) = 'E_p(A) :&: subgroups B.
+
Lemma pElemI p A B :
'E_p(A :&: B) = 'E_p(A) :&: subgroups B.
-
Lemma pElemJ x p A E :
((
E :^ x)%
G \in 'E_p(A :^ x)) = (E \in 'E_p(A)).
+
Lemma pElemJ x p A E :
((
E :^ x)%
G \in 'E_p(A :^ x)) = (E \in 'E_p(A)).
Lemma pnElemP p n A E :
-
reflect [/\ E \subset A, p.-abelem E & logn p #|E| = n] (
E \in 'E_p^n(A)).
+
reflect [/\ E \subset A, p.-abelem E & logn p #|E| = n] (
E \in 'E_p^n(A)).
Lemma pnElemPcard p n A E :
-
E \in 'E_p^n(A) → [/\ E \subset A, p.-abelem E & #|E| = p ^ n]%
N.
+
E \in 'E_p^n(A) → [/\ E \subset A, p.-abelem E & #|E| = p ^ n]%
N.
-
Lemma card_pnElem p n A E :
E \in 'E_p^n(A) → #|E| = (
p ^ n)%
N.
+
Lemma card_pnElem p n A E :
E \in 'E_p^n(A) → #|E| = (
p ^ n)%
N.
-
Lemma pnElem0 p G :
'E_p^0
(G) = [set 1%
G].
+
Lemma pnElem0 p G :
'E_p^0
(G) = [set 1%
G].
-
Lemma pnElem_prime p n A E :
E \in 'E_p^n.+1(A) → prime p.
+
Lemma pnElem_prime p n A E :
E \in 'E_p^n.+1(A) → prime p.
Lemma pnElemE p n A :
-
prime p → 'E_p^n(A) = [set E in 'E_p(A) | #|E| == (
p ^ n)%
N].
+
prime p → 'E_p^n(A) = [set E in 'E_p(A) | #|E| == (
p ^ n)%
N].
-
Lemma pnElemS p n A B :
A \subset B → 'E_p^n(A) \subset 'E_p^n(B).
+
Lemma pnElemS p n A B :
A \subset B → 'E_p^n(A) \subset 'E_p^n(B).
-
Lemma pnElemI p n A B :
'E_p^n(A :&: B) = 'E_p^n(A) :&: subgroups B.
+
Lemma pnElemI p n A B :
'E_p^n(A :&: B) = 'E_p^n(A) :&: subgroups B.
-
Lemma pnElemJ x p n A E :
((
E :^ x)%
G \in 'E_p^n(A :^ x)) = (E \in 'E_p^n(A)).
+
Lemma pnElemJ x p n A E :
((
E :^ x)%
G \in 'E_p^n(A :^ x)) = (E \in 'E_p^n(A)).
Lemma abelem_pnElem p n G :
-
p.-abelem G → n ≤ logn p #|G| → ∃ E, E \in 'E_p^n(G).
+
p.-abelem G → n ≤ logn p #|G| → ∃ E, E \in 'E_p^n(G).
-
Lemma card_p1Elem p A X :
X \in 'E_p^1
(A) → #|X| = p.
+
Lemma card_p1Elem p A X :
X \in 'E_p^1
(A) → #|X| = p.
-
Lemma p1ElemE p A :
prime p → 'E_p^1
(A) = [set X in subgroups A | #|X| == p].
+
Lemma p1ElemE p A :
prime p → 'E_p^1
(A) = [set X in subgroups A | #|X| == p].
Lemma TIp1ElemP p A X Y :
-
X \in 'E_p^1
(A) → Y \in 'E_p^1
(A) → reflect (
X :&: Y = 1) (
X :!=: Y).
+
X \in 'E_p^1
(A) → Y \in 'E_p^1
(A) → reflect (
X :&: Y = 1) (
X :!=: Y).
Lemma card_p1Elem_pnElem p n A E :
-
E \in 'E_p^n(A) → #|'E_p^1
(E)| = (
\sum_(i < n) p ^ i)%
N.
+
E \in 'E_p^n(A) → #|'E_p^1
(E)| = (
\sum_(i < n) p ^ i)%
N.
-
Lemma card_p1Elem_p2Elem p A E :
E \in 'E_p^2
(A) → #|'E_p^1
(E)| = p.+1.
+
Lemma card_p1Elem_p2Elem p A E :
E \in 'E_p^2
(A) → #|'E_p^1
(E)| = p.+1.
Lemma p2Elem_dprodP p A E X Y :
-
E \in 'E_p^2
(A) → X \in 'E_p^1
(E) → Y \in 'E_p^1
(E) →
-
reflect (
X \x Y = E) (
X :!=: Y).
+
E \in 'E_p^2
(A) → X \in 'E_p^1
(E) → Y \in 'E_p^1
(E) →
+
reflect (
X \x Y = E) (
X :!=: Y).
-
Lemma nElemP n G E :
reflect (
∃ p, E \in 'E_p^n(G)) (
E \in 'E^n(G)).
+
Lemma nElemP n G E :
reflect (
∃ p, E \in 'E_p^n(G)) (
E \in 'E^n(G)).
-
Lemma nElem0 G :
'E^0
(G) = [set 1%
G].
+
Lemma nElem0 G :
'E^0
(G) = [set 1%
G].
Lemma nElem1P G E :
-
reflect (
E \subset G ∧ exists2 p, prime p & #|E| = p) (
E \in 'E^1
(G)).
+
reflect (
E \subset G ∧ exists2 p, prime p & #|E| = p) (
E \in 'E^1
(G)).
-
Lemma nElemS n G H :
G \subset H → 'E^n(G) \subset 'E^n(H).
+
Lemma nElemS n G H :
G \subset H → 'E^n(G) \subset 'E^n(H).
-
Lemma nElemI n G H :
'E^n(G :&: H) = 'E^n(G) :&: subgroups H.
+
Lemma nElemI n G H :
'E^n(G :&: H) = 'E^n(G) :&: subgroups H.
-
Lemma def_pnElem p n G :
'E_p^n(G) = 'E_p(G) :&: 'E^n(G).
+
Lemma def_pnElem p n G :
'E_p^n(G) = 'E_p(G) :&: 'E^n(G).
Lemma pmaxElemP p A E :
-
reflect (
E \in 'E_p(A) ∧ ∀ H,
H \in 'E_p(A) → E \subset H → H :=: E)
- (
E \in 'E×_p(A)).
+
reflect (
E \in 'E_p(A) ∧ ∀ H,
H \in 'E_p(A) → E \subset H → H :=: E)
+ (
E \in 'E×_p(A)).
Lemma pmaxElem_exists p A D :
-
D \in 'E_p(A) → {E | E \in 'E×_p(A) & D \subset E}.
+
D \in 'E_p(A) → {E | E \in 'E×_p(A) & D \subset E}.
Lemma pmaxElem_LdivP p G E :
-
prime p → reflect (
'Ldiv_p('C_G(E)) = E) (
E \in 'E×_p(G)).
+
prime p → reflect (
'Ldiv_p('C_G(E)) = E) (
E \in 'E×_p(G)).
Lemma pmaxElemS p A B :
-
A \subset B → 'E×_p(B) :&: subgroups A \subset 'E×_p(A).
+
A \subset B → 'E×_p(B) :&: subgroups A \subset 'E×_p(A).
-
Lemma pmaxElemJ p A E x :
((
E :^ x)%
G \in 'E×_p(A :^ x)) = (E \in 'E×_p(A)).
+
Lemma pmaxElemJ p A E x :
((
E :^ x)%
G \in 'E×_p(A :^ x)) = (E \in 'E×_p(A)).
-
Lemma grank_min B :
'm(<<B>>) ≤ #|B|.
+
Lemma grank_min B :
'm(<<B>>) ≤ #|B|.
-
Lemma grank_witness G :
{B | <<B>> = G & #|B| = 'm(G)}.
+
Lemma grank_witness G :
{B | <<B>> = G & #|B| = 'm(G)}.
-
Lemma p_rank_witness p G :
{E | E \in 'E_p^('r_p(G))(G)}.
+
Lemma p_rank_witness p G :
{E | E \in 'E_p^('r_p(G))(G)}.
-
Lemma p_rank_geP p n G :
reflect (
∃ E, E \in 'E_p^n(G)) (
n ≤ 'r_p(G)).
+
Lemma p_rank_geP p n G :
reflect (
∃ E, E \in 'E_p^n(G)) (
n ≤ 'r_p(G)).
-
Lemma p_rank_gt0 p H :
('r_p(H) > 0
) = (p \in \pi(H)).
+
Lemma p_rank_gt0 p H :
('r_p(H) > 0
) = (p \in \pi(H)).
-
Lemma p_rank1 p :
'r_p([1 gT]) = 0.
+
Lemma p_rank1 p :
'r_p([1 gT]) = 0.
-
Lemma logn_le_p_rank p A E :
E \in 'E_p(A) → logn p #|E| ≤ 'r_p(A).
+
Lemma logn_le_p_rank p A E :
E \in 'E_p(A) → logn p #|E| ≤ 'r_p(A).
-
Lemma p_rank_le_logn p G :
'r_p(G) ≤ logn p #|G|.
+
Lemma p_rank_le_logn p G :
'r_p(G) ≤ logn p #|G|.
-
Lemma p_rank_abelem p G :
p.-abelem G → 'r_p(G) = logn p #|G|.
+
Lemma p_rank_abelem p G :
p.-abelem G → 'r_p(G) = logn p #|G|.
-
Lemma p_rankS p A B :
A \subset B → 'r_p(A) ≤ 'r_p(B).
+
Lemma p_rankS p A B :
A \subset B → 'r_p(A) ≤ 'r_p(B).
-
Lemma p_rankElem_max p A :
'E_p^('r_p(A))(A) \subset 'E×_p(A).
+
Lemma p_rankElem_max p A :
'E_p^('r_p(A))(A) \subset 'E×_p(A).
-
Lemma p_rankJ p A x :
'r_p(A :^ x) = 'r_p(A).
+
Lemma p_rankJ p A x :
'r_p(A :^ x) = 'r_p(A).
-
Lemma p_rank_Sylow p G H :
p.-Sylow(G) H → 'r_p(H) = 'r_p(G).
+
Lemma p_rank_Sylow p G H :
p.-Sylow(G) H → 'r_p(H) = 'r_p(G).
-
Lemma p_rank_Hall pi p G H :
pi.-Hall(G) H → p \in pi → 'r_p(H) = 'r_p(G).
+
Lemma p_rank_Hall pi p G H :
pi.-Hall(G) H → p \in pi → 'r_p(H) = 'r_p(G).
Lemma p_rank_pmaxElem_exists p r G :
-
'r_p(G) ≥ r → exists2 E, E \in 'E×_p(G) & 'r_p(E) ≥ r.
+
'r_p(G) ≥ r → exists2 E, E \in 'E×_p(G) & 'r_p(E) ≥ r.
-
Lemma rank1 :
'r([1 gT]) = 0.
+
Lemma rank1 :
'r([1 gT]) = 0.
-
Lemma p_rank_le_rank p G :
'r_p(G) ≤ 'r(G).
+
Lemma p_rank_le_rank p G :
'r_p(G) ≤ 'r(G).
-
Lemma rank_gt0 G :
('r(G) > 0
) = (G :!=: 1
).
+
Lemma rank_gt0 G :
('r(G) > 0
) = (G :!=: 1
).
-
Lemma rank_witness G :
{p | prime p & 'r(G) = 'r_p(G)}.
+
Lemma rank_witness G :
{p | prime p & 'r(G) = 'r_p(G)}.
-
Lemma rank_pgroup p G :
p.-group G → 'r(G) = 'r_p(G).
+
Lemma rank_pgroup p G :
p.-group G → 'r(G) = 'r_p(G).
-
Lemma rank_Sylow p G P :
p.-Sylow(G) P → 'r(P) = 'r_p(G).
+
Lemma rank_Sylow p G P :
p.-Sylow(G) P → 'r(P) = 'r_p(G).
-
Lemma rank_abelem p G :
p.-abelem G → 'r(G) = logn p #|G|.
+
Lemma rank_abelem p G :
p.-abelem G → 'r(G) = logn p #|G|.
-
Lemma nt_pnElem p n E A :
E \in 'E_p^n(A) → n > 0
→ E :!=: 1.
+
Lemma nt_pnElem p n E A :
E \in 'E_p^n(A) → n > 0
→ E :!=: 1.
-
Lemma rankJ A x :
'r(A :^ x) = 'r(A).
+
Lemma rankJ A x :
'r(A :^ x) = 'r(A).
-
Lemma rankS A B :
A \subset B → 'r(A) ≤ 'r(B).
+
Lemma rankS A B :
A \subset B → 'r(A) ≤ 'r(B).
-
Lemma rank_geP n G :
reflect (
∃ E, E \in 'E^n(G)) (
n ≤ 'r(G)).
+
Lemma rank_geP n G :
reflect (
∃ E, E \in 'E^n(G)) (
n ≤ 'r(G)).
End ExponentAbelem.
@@ -591,30 +590,30 @@
Section MorphAbelem.
-
Variables (
aT rT :
finGroupType) (
D :
{group aT}) (
f :
{morphism D >-> rT}).
-
Implicit Types (
G H E :
{group aT}) (
A B :
{set aT}).
+
Variables (
aT rT :
finGroupType) (
D :
{group aT}) (
f :
{morphism D >-> rT}).
+
Implicit Types (
G H E :
{group aT}) (
A B :
{set aT}).
-
Lemma exponent_morphim G :
exponent (
f @* G)
%| exponent G.
+
Lemma exponent_morphim G :
exponent (
f @* G)
%| exponent G.
-
Lemma morphim_LdivT n :
f @* 'Ldiv_n \subset 'Ldiv_n.
+
Lemma morphim_LdivT n :
f @* 'Ldiv_n \subset 'Ldiv_n.
-
Lemma morphim_Ldiv n A :
f @* 'Ldiv_n(A) \subset 'Ldiv_n(f @* A).
+
Lemma morphim_Ldiv n A :
f @* 'Ldiv_n(A) \subset 'Ldiv_n(f @* A).
-
Lemma morphim_abelem p G :
p.-abelem G → p.-abelem (
f @* G).
+
Lemma morphim_abelem p G :
p.-abelem G → p.-abelem (
f @* G).
-
Lemma morphim_pElem p G E :
E \in 'E_p(G) → (
f @* E)%
G \in 'E_p(f @* G).
+
Lemma morphim_pElem p G E :
E \in 'E_p(G) → (
f @* E)%
G \in 'E_p(f @* G).
Lemma morphim_pnElem p n G E :
-
E \in 'E_p^n(G) → {m | m ≤ n & (
f @* E)%
G \in 'E_p^m(f @* G)}.
+
E \in 'E_p^n(G) → {m | m ≤ n & (
f @* E)%
G \in 'E_p^m(f @* G)}.
-
Lemma morphim_grank G :
G \subset D → 'm(f @* G) ≤ 'm(G).
+
Lemma morphim_grank G :
G \subset D → 'm(f @* G) ≤ 'm(G).
@@ -632,43 +631,43 @@
Section InjmAbelem.
-Variables (aT rT : finGroupType) (D G : {group aT}) (f : {morphism D >-> rT}).
-Hypotheses (injf : 'injm f) (sGD : G \subset D).
-Let defG : invm injf @* (f @* G) = G := morphim_invm injf sGD.
+Variables (aT rT : finGroupType) (D G : {group aT}) (f : {morphism D >-> rT}).
+Hypotheses (injf : 'injm f) (sGD : G \subset D).
+Let defG : invm injf @* (f @* G) = G := morphim_invm injf sGD.
-Lemma exponent_injm : exponent (f @* G) = exponent G.
+Lemma exponent_injm : exponent (f @* G) = exponent G.
-Lemma injm_Ldiv n A : f @* 'Ldiv_n(A) = 'Ldiv_n(f @* A).
+Lemma injm_Ldiv n A : f @* 'Ldiv_n(A) = 'Ldiv_n(f @* A).
-Lemma injm_abelem p : p.-abelem (f @* G) = p.-abelem G.
+Lemma injm_abelem p : p.-abelem (f @* G) = p.-abelem G.
-Lemma injm_pElem p (E : {group aT}) :
- E \subset D → ((f @* E)%G \in 'E_p(f @* G)) = (E \in 'E_p(G)).
+Lemma injm_pElem p (E : {group aT}) :
+ E \subset D → ((f @* E)%G \in 'E_p(f @* G)) = (E \in 'E_p(G)).
-Lemma injm_pnElem p n (E : {group aT}) :
- E \subset D → ((f @* E)%G \in 'E_p^n(f @* G)) = (E \in 'E_p^n(G)).
+Lemma injm_pnElem p n (E : {group aT}) :
+ E \subset D → ((f @* E)%G \in 'E_p^n(f @* G)) = (E \in 'E_p^n(G)).
-Lemma injm_nElem n (E : {group aT}) :
- E \subset D → ((f @* E)%G \in 'E^n(f @* G)) = (E \in 'E^n(G)).
+Lemma injm_nElem n (E : {group aT}) :
+ E \subset D → ((f @* E)%G \in 'E^n(f @* G)) = (E \in 'E^n(G)).
-Lemma injm_pmaxElem p (E : {group aT}) :
- E \subset D → ((f @* E)%G \in 'E×_p(f @* G)) = (E \in 'E×_p(G)).
+Lemma injm_pmaxElem p (E : {group aT}) :
+ E \subset D → ((f @* E)%G \in 'E×_p(f @* G)) = (E \in 'E×_p(G)).
-Lemma injm_grank : 'm(f @* G) = 'm(G).
+Lemma injm_grank : 'm(f @* G) = 'm(G).
-Lemma injm_p_rank p : 'r_p(f @* G) = 'r_p(G).
+Lemma injm_p_rank p : 'r_p(f @* G) = 'r_p(G).
-Lemma injm_rank : 'r(f @* G) = 'r(G).
+Lemma injm_rank : 'r(f @* G) = 'r(G).
End InjmAbelem.
@@ -677,23 +676,23 @@
Section IsogAbelem.
-Variables (aT rT : finGroupType) (G : {group aT}) (H : {group rT}).
-Hypothesis isoGH : G \isog H.
+Variables (aT rT : finGroupType) (G : {group aT}) (H : {group rT}).
+Hypothesis isoGH : G \isog H.
-Lemma exponent_isog : exponent G = exponent H.
+Lemma exponent_isog : exponent G = exponent H.
-Lemma isog_abelem p : p.-abelem G = p.-abelem H.
+Lemma isog_abelem p : p.-abelem G = p.-abelem H.
-Lemma isog_grank : 'm(G) = 'm(H).
+Lemma isog_grank : 'm(G) = 'm(H).
-Lemma isog_p_rank p : 'r_p(G) = 'r_p(H).
+Lemma isog_p_rank p : 'r_p(G) = 'r_p(H).
-Lemma isog_rank : 'r(G) = 'r(H).
+Lemma isog_rank : 'r(G) = 'r(H).
End IsogAbelem.
@@ -702,43 +701,43 @@
Section QuotientAbelem.
-Variables (gT : finGroupType) (p : nat).
-Implicit Types E G K H : {group gT}.
+Variables (gT : finGroupType) (p : nat).
+Implicit Types E G K H : {group gT}.
-Lemma exponent_quotient G H : exponent (G / H) %| exponent G.
+Lemma exponent_quotient G H : exponent (G / H) %| exponent G.
-Lemma quotient_LdivT n H : 'Ldiv_n / H \subset 'Ldiv_n.
+Lemma quotient_LdivT n H : 'Ldiv_n / H \subset 'Ldiv_n.
-Lemma quotient_Ldiv n A H : 'Ldiv_n(A) / H \subset 'Ldiv_n(A / H).
+Lemma quotient_Ldiv n A H : 'Ldiv_n(A) / H \subset 'Ldiv_n(A / H).
-Lemma quotient_abelem G H : p.-abelem G → p.-abelem (G / H).
+Lemma quotient_abelem G H : p.-abelem G → p.-abelem (G / H).
-Lemma quotient_pElem G H E : E \in 'E_p(G) → (E / H)%G \in 'E_p(G / H).
+Lemma quotient_pElem G H E : E \in 'E_p(G) → (E / H)%G \in 'E_p(G / H).
-Lemma logn_quotient G H : logn p #|G / H| ≤ logn p #|G|.
+Lemma logn_quotient G H : logn p #|G / H| ≤ logn p #|G|.
Lemma quotient_pnElem G H n E :
- E \in 'E_p^n(G) → {m | m ≤ n & (E / H)%G \in 'E_p^m(G / H)}.
+ E \in 'E_p^n(G) → {m | m ≤ n & (E / H)%G \in 'E_p^m(G / H)}.
-Lemma quotient_grank G H : G \subset 'N(H) → 'm(G / H) ≤ 'm(G).
+Lemma quotient_grank G H : G \subset 'N(H) → 'm(G / H) ≤ 'm(G).
-Lemma p_rank_quotient G H : G \subset 'N(H) → 'r_p(G) - 'r_p(H) ≤ 'r_p(G / H).
+Lemma p_rank_quotient G H : G \subset 'N(H) → 'r_p(G) - 'r_p(H) ≤ 'r_p(G / H).
-Lemma p_rank_dprod K H G : K \x H = G → 'r_p(K) + 'r_p(H) = 'r_p(G).
+Lemma p_rank_dprod K H G : K \x H = G → 'r_p(K) + 'r_p(H) = 'r_p(G).
Lemma p_rank_p'quotient G H :
- (p : nat)^'.-group H → G \subset 'N(H) → 'r_p(G / H) = 'r_p(G).
+ (p : nat)^'.-group H → G \subset 'N(H) → 'r_p(G / H) = 'r_p(G).
End QuotientAbelem.
@@ -750,204 +749,204 @@
Section Generic.
-Variables (n : nat) (gT : finGroupType).
-Implicit Types (p : nat) (x : gT) (rT : finGroupType).
-Implicit Types (A B : {set gT}) (D G H : {group gT}).
+Variables (n : nat) (gT : finGroupType).
+Implicit Types (p : nat) (x : gT) (rT : finGroupType).
+Implicit Types (A B : {set gT}) (D G H : {group gT}).
-Lemma Ohm_sub G : 'Ohm_n(G) \subset G.
+Lemma Ohm_sub G : 'Ohm_n(G) \subset G.
-Lemma Ohm1 : 'Ohm_n([1 gT]) = 1.
+Lemma Ohm1 : 'Ohm_n([1 gT]) = 1.
-Lemma Ohm_id G : 'Ohm_n('Ohm_n(G)) = 'Ohm_n(G).
+Lemma Ohm_id G : 'Ohm_n('Ohm_n(G)) = 'Ohm_n(G).
-Lemma Ohm_cont rT G (f : {morphism G >-> rT}) :
- f @* 'Ohm_n(G) \subset 'Ohm_n(f @* G).
+Lemma Ohm_cont rT G (f : {morphism G >-> rT}) :
+ f @* 'Ohm_n(G) \subset 'Ohm_n(f @* G).
-Lemma OhmS H G : H \subset G → 'Ohm_n(H) \subset 'Ohm_n(G).
+Lemma OhmS H G : H \subset G → 'Ohm_n(H) \subset 'Ohm_n(G).
-Lemma OhmE p G : p.-group G → 'Ohm_n(G) = <<'Ldiv_(p ^ n)(G)>>.
+Lemma OhmE p G : p.-group G → 'Ohm_n(G) = <<'Ldiv_(p ^ n)(G)>>.
Lemma OhmEabelian p G :
- p.-group G → abelian 'Ohm_n(G) → 'Ohm_n(G) = 'Ldiv_(p ^ n)(G).
+ p.-group G → abelian 'Ohm_n(G) → 'Ohm_n(G) = 'Ldiv_(p ^ n)(G).
Lemma Ohm_p_cycle p x :
- p.-elt x → 'Ohm_n(<[x]>) = <[x ^+ (p ^ (logn p #[x] - n))]>.
+ p.-elt x → 'Ohm_n(<[x]>) = <[x ^+ (p ^ (logn p #[x] - n))]>.
-Lemma Ohm_dprod A B G : A \x B = G → 'Ohm_n(A) \x 'Ohm_n(B) = 'Ohm_n(G).
+Lemma Ohm_dprod A B G : A \x B = G → 'Ohm_n(A) \x 'Ohm_n(B) = 'Ohm_n(G).
-Lemma Mho_sub G : 'Mho^n(G) \subset G.
+Lemma Mho_sub G : 'Mho^n(G) \subset G.
-Lemma Mho1 : 'Mho^n([1 gT]) = 1.
+Lemma Mho1 : 'Mho^n([1 gT]) = 1.
-Lemma morphim_Mho rT D G (f : {morphism D >-> rT}) :
- G \subset D → f @* 'Mho^n(G) = 'Mho^n(f @* G).
+Lemma morphim_Mho rT D G (f : {morphism D >-> rT}) :
+ G \subset D → f @* 'Mho^n(G) = 'Mho^n(f @* G).
-Lemma Mho_cont rT G (f : {morphism G >-> rT}) :
- f @* 'Mho^n(G) \subset 'Mho^n(f @* G).
+Lemma Mho_cont rT G (f : {morphism G >-> rT}) :
+ f @* 'Mho^n(G) \subset 'Mho^n(f @* G).
-Lemma MhoS H G : H \subset G → 'Mho^n(H) \subset 'Mho^n(G).
+Lemma MhoS H G : H \subset G → 'Mho^n(H) \subset 'Mho^n(G).
-Lemma MhoE p G : p.-group G → 'Mho^n(G) = <<[set x ^+ (p ^ n) | x in G]>>.
+Lemma MhoE p G : p.-group G → 'Mho^n(G) = <<[set x ^+ (p ^ n) | x in G]>>.
Lemma MhoEabelian p G :
- p.-group G → abelian G → 'Mho^n(G) = [set x ^+ (p ^ n) | x in G].
+ p.-group G → abelian G → 'Mho^n(G) = [set x ^+ (p ^ n) | x in G].
-Lemma trivg_Mho G : 'Mho^n(G) == 1 → 'Ohm_n(G) == G.
+Lemma trivg_Mho G : 'Mho^n(G) == 1 → 'Ohm_n(G) == G.
-Lemma Mho_p_cycle p x : p.-elt x → 'Mho^n(<[x]>) = <[x ^+ (p ^ n)]>.
+Lemma Mho_p_cycle p x : p.-elt x → 'Mho^n(<[x]>) = <[x ^+ (p ^ n)]>.
-Lemma Mho_cprod A B G : A \* B = G → 'Mho^n(A) \* 'Mho^n(B) = 'Mho^n(G).
+Lemma Mho_cprod A B G : A \* B = G → 'Mho^n(A) \* 'Mho^n(B) = 'Mho^n(G).
-Lemma Mho_dprod A B G : A \x B = G → 'Mho^n(A) \x 'Mho^n(B) = 'Mho^n(G).
+Lemma Mho_dprod A B G : A \x B = G → 'Mho^n(A) \x 'Mho^n(B) = 'Mho^n(G).
End Generic.
-Canonical Ohm_igFun i := [igFun by Ohm_sub i & Ohm_cont i].
-Canonical Ohm_gFun i := [gFun by Ohm_cont i].
-Canonical Ohm_mgFun i := [mgFun by OhmS i].
+Canonical Ohm_igFun i := [igFun by Ohm_sub i & Ohm_cont i].
+Canonical Ohm_gFun i := [gFun by Ohm_cont i].
+Canonical Ohm_mgFun i := [mgFun by OhmS i].
-Canonical Mho_igFun i := [igFun by Mho_sub i & Mho_cont i].
-Canonical Mho_gFun i := [gFun by Mho_cont i].
-Canonical Mho_mgFun i := [mgFun by MhoS i].
+Canonical Mho_igFun i := [igFun by Mho_sub i & Mho_cont i].
+Canonical Mho_gFun i := [gFun by Mho_cont i].
+Canonical Mho_mgFun i := [mgFun by MhoS i].
Section char.
-Variables (n : nat) (gT rT : finGroupType) (D G : {group gT}).
+Variables (n : nat) (gT rT : finGroupType) (D G : {group gT}).
-Lemma Ohm_char : 'Ohm_n(G) \char G.
-Lemma Ohm_normal : 'Ohm_n(G) <| G.
+Lemma Ohm_char : 'Ohm_n(G) \char G.
+Lemma Ohm_normal : 'Ohm_n(G) <| G.
-Lemma Mho_char : 'Mho^n(G) \char G.
-Lemma Mho_normal : 'Mho^n(G) <| G.
+Lemma Mho_char : 'Mho^n(G) \char G.
+Lemma Mho_normal : 'Mho^n(G) <| G.
-Lemma morphim_Ohm (f : {morphism D >-> rT}) :
- G \subset D → f @* 'Ohm_n(G) \subset 'Ohm_n(f @* G).
+Lemma morphim_Ohm (f : {morphism D >-> rT}) :
+ G \subset D → f @* 'Ohm_n(G) \subset 'Ohm_n(f @* G).
-Lemma injm_Ohm (f : {morphism D >-> rT}) :
- 'injm f → G \subset D → f @* 'Ohm_n(G) = 'Ohm_n(f @* G).
+Lemma injm_Ohm (f : {morphism D >-> rT}) :
+ 'injm f → G \subset D → f @* 'Ohm_n(G) = 'Ohm_n(f @* G).
-Lemma isog_Ohm (H : {group rT}) : G \isog H → 'Ohm_n(G) \isog 'Ohm_n(H).
+Lemma isog_Ohm (H : {group rT}) : G \isog H → 'Ohm_n(G) \isog 'Ohm_n(H).
-Lemma isog_Mho (H : {group rT}) : G \isog H → 'Mho^n(G) \isog 'Mho^n(H).
+Lemma isog_Mho (H : {group rT}) : G \isog H → 'Mho^n(G) \isog 'Mho^n(H).
End char.
Variable gT : finGroupType.
-Implicit Types (pi : nat_pred) (p : nat).
-Implicit Types (A B C : {set gT}) (D G H E : {group gT}).
+Implicit Types (pi : nat_pred) (p : nat).
+Implicit Types (A B C : {set gT}) (D G H E : {group gT}).
-Lemma Ohm0 G : 'Ohm_0(G) = 1.
+Lemma Ohm0 G : 'Ohm_0(G) = 1.
-Lemma Ohm_leq m n G : m ≤ n → 'Ohm_m(G) \subset 'Ohm_n(G).
+Lemma Ohm_leq m n G : m ≤ n → 'Ohm_m(G) \subset 'Ohm_n(G).
-Lemma OhmJ n G x : 'Ohm_n(G :^ x) = 'Ohm_n(G) :^ x.
+Lemma OhmJ n G x : 'Ohm_n(G :^ x) = 'Ohm_n(G) :^ x.
-Lemma Mho0 G : 'Mho^0(G) = G.
+Lemma Mho0 G : 'Mho^0(G) = G.
-Lemma Mho_leq m n G : m ≤ n → 'Mho^n(G) \subset 'Mho^m(G).
+Lemma Mho_leq m n G : m ≤ n → 'Mho^n(G) \subset 'Mho^m(G).
-Lemma MhoJ n G x : 'Mho^n(G :^ x) = 'Mho^n(G) :^ x.
+Lemma MhoJ n G x : 'Mho^n(G :^ x) = 'Mho^n(G) :^ x.
Lemma extend_cyclic_Mho G p x :
- p.-group G → x \in G → 'Mho^1(G) = <[x ^+ p]> →
- ∀ k, k > 0 → 'Mho^k(G) = <[x ^+ (p ^ k)]>.
+ p.-group G → x \in G → 'Mho^1(G) = <[x ^+ p]> →
+ ∀ k, k > 0 → 'Mho^k(G) = <[x ^+ (p ^ k)]>.
-Lemma Ohm1Eprime G : 'Ohm_1(G) = <<[set x in G | prime #[x]]>>.
+Lemma Ohm1Eprime G : 'Ohm_1(G) = <<[set x in G | prime #[x]]>>.
-Lemma abelem_Ohm1 p G : p.-group G → p.-abelem 'Ohm_1(G) = abelian 'Ohm_1(G).
+Lemma abelem_Ohm1 p G : p.-group G → p.-abelem 'Ohm_1(G) = abelian 'Ohm_1(G).
-Lemma Ohm1_abelem p G : p.-group G → abelian G → p.-abelem ('Ohm_1(G)).
+Lemma Ohm1_abelem p G : p.-group G → abelian G → p.-abelem ('Ohm_1(G)).
-Lemma Ohm1_id p G : p.-abelem G → 'Ohm_1(G) = G.
+Lemma Ohm1_id p G : p.-abelem G → 'Ohm_1(G) = G.
Lemma abelem_Ohm1P p G :
- abelian G → p.-group G → reflect ('Ohm_1(G) = G) (p.-abelem G).
+ abelian G → p.-group G → reflect ('Ohm_1(G) = G) (p.-abelem G).
-Lemma TI_Ohm1 G H : H :&: 'Ohm_1(G) = 1 → H :&: G = 1.
+Lemma TI_Ohm1 G H : H :&: 'Ohm_1(G) = 1 → H :&: G = 1.
-Lemma Ohm1_eq1 G : ('Ohm_1(G) == 1) = (G :==: 1).
+Lemma Ohm1_eq1 G : ('Ohm_1(G) == 1) = (G :==: 1).
-Lemma meet_Ohm1 G H : G :&: H != 1 → G :&: 'Ohm_1(H) != 1.
+Lemma meet_Ohm1 G H : G :&: H != 1 → G :&: 'Ohm_1(H) != 1.
-Lemma Ohm1_cent_max G E p : E \in 'E×_p(G) → p.-group G → 'Ohm_1('C_G(E)) = E.
+Lemma Ohm1_cent_max G E p : E \in 'E×_p(G) → p.-group G → 'Ohm_1('C_G(E)) = E.
Lemma Ohm1_cyclic_pgroup_prime p G :
- cyclic G → p.-group G → G :!=: 1 → #|'Ohm_1(G)| = p.
+ cyclic G → p.-group G → G :!=: 1 → #|'Ohm_1(G)| = p.
Lemma cyclic_pgroup_dprod_trivg p A B C :
- p.-group C → cyclic C → A \x B = C →
- A = 1 ∧ B = C ∨ B = 1 ∧ A = C.
+ p.-group C → cyclic C → A \x B = C →
+ A = 1 ∧ B = C ∨ B = 1 ∧ A = C.
-Lemma piOhm1 G : \pi('Ohm_1(G)) = \pi(G).
+Lemma piOhm1 G : \pi('Ohm_1(G)) = \pi(G).
Lemma Ohm1Eexponent p G :
- prime p → exponent 'Ohm_1(G) %| p → 'Ohm_1(G) = 'Ldiv_p(G).
+ prime p → exponent 'Ohm_1(G) %| p → 'Ohm_1(G) = 'Ldiv_p(G).
-Lemma p_rank_Ohm1 p G : 'r_p('Ohm_1(G)) = 'r_p(G).
+Lemma p_rank_Ohm1 p G : 'r_p('Ohm_1(G)) = 'r_p(G).
-Lemma rank_Ohm1 G : 'r('Ohm_1(G)) = 'r(G).
+Lemma rank_Ohm1 G : 'r('Ohm_1(G)) = 'r(G).
-Lemma p_rank_abelian p G : abelian G → 'r_p(G) = logn p #|'Ohm_1(G)|.
+Lemma p_rank_abelian p G : abelian G → 'r_p(G) = logn p #|'Ohm_1(G)|.
Lemma rank_abelian_pgroup p G :
- p.-group G → abelian G → 'r(G) = logn p #|'Ohm_1(G)|.
+ p.-group G → abelian G → 'r(G) = logn p #|'Ohm_1(G)|.
End OhmProps.
@@ -957,118 +956,118 @@
Variable gT : finGroupType.
-Implicit Types (p : nat) (G H K E : {group gT}).
+Implicit Types (p : nat) (G H K E : {group gT}).
Lemma abelian_splits x G :
- x \in G → #[x] = exponent G → abelian G → [splits G, over <[x]>].
+ x \in G → #[x] = exponent G → abelian G → [splits G, over <[x]>].
-Lemma abelem_splits p G H : p.-abelem G → H \subset G → [splits G, over H].
+Lemma abelem_splits p G H : p.-abelem G → H \subset G → [splits G, over H].
Fact abelian_type_subproof G :
- {H : {group gT} & abelian G → {x | #[x] = exponent G & <[x]> \x H = G}}.
+ {H : {group gT} & abelian G → {x | #[x] = exponent G & <[x]> \x H = G}}.
Fixpoint abelian_type_rec n G :=
- if n is n'.+1 then if abelian G && (G :!=: 1) then
- exponent G :: abelian_type_rec n' (tag (abelian_type_subproof G))
- else [::] else [::].
+ if n is n'.+1 then if abelian G && (G :!=: 1) then
+ exponent G :: abelian_type_rec n' (tag (abelian_type_subproof G))
+ else [::] else [::].
-Definition abelian_type (A : {set gT}) := abelian_type_rec #|A| <<A>>.
+Definition abelian_type (A : {set gT}) := abelian_type_rec #|A| <<A>>.
-Lemma abelian_type_dvdn_sorted A : sorted [rel m n | n %| m] (abelian_type A).
+Lemma abelian_type_dvdn_sorted A : sorted [rel m n | n %| m] (abelian_type A).
-Lemma abelian_type_gt1 A : all [pred m | m > 1] (abelian_type A).
+Lemma abelian_type_gt1 A : all [pred m | m > 1] (abelian_type A).
Lemma abelian_type_sorted A : sorted geq (abelian_type A).
Theorem abelian_structure G :
- abelian G →
- {b | \big[dprod/1]_(x <- b) <[x]> = G & map order b = abelian_type G}.
+ abelian G →
+ {b | \big[dprod/1]_(x <- b) <[x]> = G & map order b = abelian_type G}.
Lemma count_logn_dprod_cycle p n b G :
- \big[dprod/1]_(x <- b) <[x]> = G →
- count [pred x | logn p #[x] > n] b = logn p #|'Ohm_n.+1(G) : 'Ohm_n(G)|.
+ \big[dprod/1]_(x <- b) <[x]> = G →
+ count [pred x | logn p #[x] > n] b = logn p #|'Ohm_n.+1(G) : 'Ohm_n(G)|.
-Lemma perm_eq_abelian_type p b G :
- p.-group G → \big[dprod/1]_(x <- b) <[x]> = G → 1 \notin b →
- perm_eq (map order b) (abelian_type G).
+Lemma abelian_type_pgroup p b G :
+ p.-group G → \big[dprod/1]_(x <- b) <[x]> = G → 1 \notin b →
+ perm_eq (abelian_type G) (map order b).
-Lemma size_abelian_type G : abelian G → size (abelian_type G) = 'r(G).
+Lemma size_abelian_type G : abelian G → size (abelian_type G) = 'r(G).
Lemma mul_card_Ohm_Mho_abelian n G :
- abelian G → (#|'Ohm_n(G)| × #|'Mho^n(G)|)%N = #|G|.
+ abelian G → (#|'Ohm_n(G)| × #|'Mho^n(G)|)%N = #|G|.
-Lemma grank_abelian G : abelian G → 'm(G) = 'r(G).
+Lemma grank_abelian G : abelian G → 'm(G) = 'r(G).
-Lemma rank_cycle (x : gT) : 'r(<[x]>) = (x != 1).
+Lemma rank_cycle (x : gT) : 'r(<[x]>) = (x != 1).
-Lemma abelian_rank1_cyclic G : abelian G → cyclic G = ('r(G) ≤ 1).
+Lemma abelian_rank1_cyclic G : abelian G → cyclic G = ('r(G) ≤ 1).
-Definition homocyclic A := abelian A && constant (abelian_type A).
+Definition homocyclic A := abelian A && constant (abelian_type A).
Lemma homocyclic_Ohm_Mho n p G :
- p.-group G → homocyclic G → 'Ohm_n(G) = 'Mho^(logn p (exponent G) - n)(G).
+ p.-group G → homocyclic G → 'Ohm_n(G) = 'Mho^(logn p (exponent G) - n)(G).
-Lemma Ohm_Mho_homocyclic (n p : nat) G :
- abelian G → p.-group G → 0 < n < logn p (exponent G) →
- 'Ohm_n(G) = 'Mho^(logn p (exponent G) - n)(G) → homocyclic G.
+Lemma Ohm_Mho_homocyclic (n p : nat) G :
+ abelian G → p.-group G → 0 < n < logn p (exponent G) →
+ 'Ohm_n(G) = 'Mho^(logn p (exponent G) - n)(G) → homocyclic G.
-Lemma abelem_homocyclic p G : p.-abelem G → homocyclic G.
+Lemma abelem_homocyclic p G : p.-abelem G → homocyclic G.
-Lemma homocyclic1 : homocyclic [1 gT].
+Lemma homocyclic1 : homocyclic [1 gT].
-Lemma Ohm1_homocyclicP p G : p.-group G → abelian G →
- reflect ('Ohm_1(G) = 'Mho^(logn p (exponent G)).-1(G)) (homocyclic G).
+Lemma Ohm1_homocyclicP p G : p.-group G → abelian G →
+ reflect ('Ohm_1(G) = 'Mho^(logn p (exponent G)).-1(G)) (homocyclic G).
Lemma abelian_type_homocyclic G :
- homocyclic G → abelian_type G = nseq 'r(G) (exponent G).
+ homocyclic G → abelian_type G = nseq 'r(G) (exponent G).
-Lemma abelian_type_abelem p G : p.-abelem G → abelian_type G = nseq 'r(G) p.
+Lemma abelian_type_abelem p G : p.-abelem G → abelian_type G = nseq 'r(G) p.
Lemma max_card_abelian G :
- abelian G → #|G| ≤ exponent G ^ 'r(G) ?= iff homocyclic G.
+ abelian G → #|G| ≤ exponent G ^ 'r(G) ?= iff homocyclic G.
-Lemma card_homocyclic G : homocyclic G → #|G| = (exponent G ^ 'r(G))%N.
+Lemma card_homocyclic G : homocyclic G → #|G| = (exponent G ^ 'r(G))%N.
Lemma abelian_type_dprod_homocyclic p K H G :
- K \x H = G → p.-group G → homocyclic G →
- abelian_type K = nseq 'r(K) (exponent G)
- ∧ abelian_type H = nseq 'r(H) (exponent G).
+ K \x H = G → p.-group G → homocyclic G →
+ abelian_type K = nseq 'r(K) (exponent G)
+ ∧ abelian_type H = nseq 'r(H) (exponent G).
Lemma dprod_homocyclic p K H G :
- K \x H = G → p.-group G → homocyclic G → homocyclic K ∧ homocyclic H.
+ K \x H = G → p.-group G → homocyclic G → homocyclic K ∧ homocyclic H.
Lemma exponent_dprod_homocyclic p K H G :
- K \x H = G → p.-group G → homocyclic G → K :!=: 1 →
- exponent K = exponent G.
+ K \x H = G → p.-group G → homocyclic G → K :!=: 1 →
+ exponent K = exponent G.
End AbelianStructure.
@@ -1080,30 +1079,30 @@
Variables aT rT : finGroupType.
-Implicit Type (gT : finGroupType) (D G : {group aT}) (H : {group rT}).
+Implicit Type (gT : finGroupType) (D G : {group aT}) (H : {group rT}).
-Lemma isog_abelian_type G H : isog G H → abelian_type G = abelian_type H.
+Lemma isog_abelian_type G H : isog G H → abelian_type G = abelian_type H.
Lemma eq_abelian_type_isog G H :
- abelian G → abelian H → isog G H = (abelian_type G == abelian_type H).
+ abelian G → abelian H → isog G H = (abelian_type G == abelian_type H).
Lemma isog_abelem_card p G H :
- p.-abelem G → isog G H = p.-abelem H && (#|H| == #|G|).
+ p.-abelem G → isog G H = p.-abelem H && (#|H| == #|G|).
-Variables (D : {group aT}) (f : {morphism D >-> rT}).
+Variables (D : {group aT}) (f : {morphism D >-> rT}).
-Lemma morphim_rank_abelian G : abelian G → 'r(f @* G) ≤ 'r(G).
+Lemma morphim_rank_abelian G : abelian G → 'r(f @* G) ≤ 'r(G).
-Lemma morphim_p_rank_abelian p G : abelian G → 'r_p(f @* G) ≤ 'r_p(G).
+Lemma morphim_p_rank_abelian p G : abelian G → 'r_p(f @* G) ≤ 'r_p(G).
-Lemma isog_homocyclic G H : G \isog H → homocyclic G = homocyclic H.
+Lemma isog_homocyclic G H : G \isog H → homocyclic G = homocyclic H.
End IsogAbelian.
@@ -1112,14 +1111,14 @@
Section QuotientRank.
-Variables (gT : finGroupType) (p : nat) (G H : {group gT}).
+Variables (gT : finGroupType) (p : nat) (G H : {group gT}).
Hypothesis cGG : abelian G.
-Lemma quotient_rank_abelian : 'r(G / H) ≤ 'r(G).
+Lemma quotient_rank_abelian : 'r(G / H) ≤ 'r(G).
-Lemma quotient_p_rank_abelian : 'r_p(G / H) ≤ 'r_p(G).
+Lemma quotient_p_rank_abelian : 'r_p(G / H) ≤ 'r_p(G).
End QuotientRank.
@@ -1132,15 +1131,15 @@
Lemma fin_lmod_char_abelem p (R : ringType) (V : finLmodType R):
- p \in [char R]%R → p.-abelem [set: V].
+ p \in [char R]%R → p.-abelem [set: V].
-Lemma fin_Fp_lmod_abelem p (V : finLmodType 'F_p) :
- prime p → p.-abelem [set: V].
+Lemma fin_Fp_lmod_abelem p (V : finLmodType 'F_p) :
+ prime p → p.-abelem [set: V].
Lemma fin_ring_char_abelem p (R : finRingType) :
- p \in [char R]%R → p.-abelem [set: R].
+ p \in [char R]%R → p.-abelem [set: R].
End FimModAbelem.
--
cgit v1.2.3