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.alt.html | 83 ++++++++++++++++-----------------
1 file changed, 41 insertions(+), 42 deletions(-)
(limited to 'docs/htmldoc/mathcomp.solvable.alt.html')
diff --git a/docs/htmldoc/mathcomp.solvable.alt.html b/docs/htmldoc/mathcomp.solvable.alt.html
index dd87d49..f94a27f 100644
--- a/docs/htmldoc/mathcomp.solvable.alt.html
+++ b/docs/htmldoc/mathcomp.solvable.alt.html
@@ -21,7 +21,6 @@
@@ -42,16 +41,16 @@
Import GroupScope.
-Definition bool_groupMixin := FinGroup.Mixin addbA addFb addbb.
-Canonical bool_baseGroup := Eval hnf in BaseFinGroupType bool bool_groupMixin.
-Canonical boolGroup := Eval hnf in FinGroupType addbb.
+Definition bool_groupMixin := FinGroup.Mixin addbA addFb addbb.
+Canonical bool_baseGroup := Eval hnf in BaseFinGroupType bool bool_groupMixin.
+Canonical boolGroup := Eval hnf in FinGroupType addbb.
Section SymAltDef.
Variable T : finType.
-Implicit Types (s : {perm T}) (x y z : T).
+Implicit Types (s : {perm T}) (x y z : T).
@@ -60,132 +59,132 @@
Definitions of the alternate groups and some Properties *
-
Definition Sym of phant T :
{set {perm T}} :=
setT.
+
Definition Sym of phant T :
{set {perm T}} :=
setT.
-
Canonical Sym_group phT :=
Eval hnf in [group of Sym phT].
+
Canonical Sym_group phT :=
Eval hnf in [group of Sym phT].
-
Canonical sign_morph := @
Morphism _ _ 'Sym_T _ (
in2W (@
odd_permM _)).
+
Canonical sign_morph := @
Morphism _ _ 'Sym_T _ (
in2W (@
odd_permM _)).
-
Definition Alt of phant T :=
'ker (@
odd_perm T).
+
Definition Alt of phant T :=
'ker (@
odd_perm T).
-
Canonical Alt_group phT :=
Eval hnf in [group of Alt phT].
+
Canonical Alt_group phT :=
Eval hnf in [group of Alt phT].
-
Lemma Alt_even p :
(p \in 'Alt_T) = ~~ p.
+
Lemma Alt_even p :
(p \in 'Alt_T) = ~~ p.
-
Lemma Alt_subset :
'Alt_T \subset 'Sym_T.
+
Lemma Alt_subset :
'Alt_T \subset 'Sym_T.
-
Lemma Alt_normal :
'Alt_T <| 'Sym_T.
+
Lemma Alt_normal :
'Alt_T <| 'Sym_T.
-
Lemma Alt_norm :
'Sym_T \subset 'N('Alt_T).
+
Lemma Alt_norm :
'Sym_T \subset 'N('Alt_T).
-
Let n :=
#|T|.
+
Let n :=
#|T|.
-
Lemma Alt_index : 1
< n → #|'Sym_T : 'Alt_T| = 2.
+
Lemma Alt_index : 1
< n → #|'Sym_T : 'Alt_T| = 2.
-
Lemma card_Sym :
#|'Sym_T| = n`!.
+
Lemma card_Sym :
#|'Sym_T| = n`!.
-
Lemma card_Alt : 1
< n → (2
× #|'Alt_T|)%
N = n`!.
+
Lemma card_Alt : 1
< n → (2
× #|'Alt_T|)%
N = n`!.
-
Lemma Sym_trans :
[transitive^n 'Sym_T, on setT | 'P].
+
Lemma Sym_trans :
[transitive^n 'Sym_T, on setT | 'P].
-
Lemma Alt_trans :
[transitive^n.-2 'Alt_T, on setT | 'P].
+
Lemma Alt_trans :
[transitive^n.-2 'Alt_T, on setT | 'P].
-
Lemma aperm_faithful (
A :
{group {perm T}}) :
[faithful A, on setT | 'P].
+
Lemma aperm_faithful (
A :
{group {perm T}}) :
[faithful A, on setT | 'P].
End SymAltDef.
-
Notation "''Sym_' T" := (
Sym (
Phant T))
+
Notation "''Sym_' T" := (
Sym (
Phant T))
(
at level 8,
T at level 2,
format "''Sym_' T") :
group_scope.
-
Notation "''Sym_' T" := (
Sym_group (
Phant T)) :
Group_scope.
+
Notation "''Sym_' T" := (
Sym_group (
Phant T)) :
Group_scope.
-
Notation "''Alt_' T" := (
Alt (
Phant T))
+
Notation "''Alt_' T" := (
Alt (
Phant T))
(
at level 8,
T at level 2,
format "''Alt_' T") :
group_scope.
-
Notation "''Alt_' T" := (
Alt_group (
Phant T)) :
Group_scope.
+
Notation "''Alt_' T" := (
Alt_group (
Phant T)) :
Group_scope.
-
Lemma trivial_Alt_2 (
T :
finType) :
#|T| ≤ 2
→ 'Alt_T = 1.
+
Lemma trivial_Alt_2 (
T :
finType) :
#|T| ≤ 2
→ 'Alt_T = 1.
-
Lemma simple_Alt_3 (
T :
finType) :
#|T| = 3
→ simple 'Alt_T.
+
Lemma simple_Alt_3 (
T :
finType) :
#|T| = 3
→ simple 'Alt_T.
-
Lemma not_simple_Alt_4 (
T :
finType) :
#|T| = 4
→ ~~ simple 'Alt_T.
+
Lemma not_simple_Alt_4 (
T :
finType) :
#|T| = 4
→ ~~ simple 'Alt_T.
-
Lemma simple_Alt5_base (
T :
finType) :
#|T| = 5
→ simple 'Alt_T.
+
Lemma simple_Alt5_base (
T :
finType) :
#|T| = 5
→ simple 'Alt_T.
Section Restrict.
Variables (
T :
finType) (
x :
T).
-
Notation T' :=
{y | y != x}.
+
Notation T' :=
{y | y != x}.
-
Lemma rfd_funP (
p :
{perm T}) (
u :
T') :
-
let p1 :=
if p x == x then p else 1
in p1 (
val u)
!= x.
+
Lemma rfd_funP (
p :
{perm T}) (
u :
T') :
+
let p1 :=
if p x == x then p else 1
in p1 (
val u)
!= x.
-
Definition rfd_fun p :=
[fun u ⇒ Sub ((
_ : {perm T})
_) (
rfd_funP p u)
: T'].
+
Definition rfd_fun p :=
[fun u ⇒ Sub ((
_ : {perm T})
_) (
rfd_funP p u)
: T'].
-
Lemma rfdP p :
injective (
rfd_fun p).
+
Lemma rfdP p :
injective (
rfd_fun p).
Definition rfd p :=
perm (@
rfdP p).
-
Hypothesis card_T : 2
< #|T|.
+
Hypothesis card_T : 2
< #|T|.
-
Lemma rfd_morph :
{in 'C_('Sym_T)[x | 'P] &, {morph rfd : y z / y × z}}.
+
Lemma rfd_morph :
{in 'C_('Sym_T)[x | 'P] &, {morph rfd : y z / y × z}}.
Canonical rfd_morphism :=
Morphism rfd_morph.
-
Definition rgd_fun (
p :
{perm T'}) :=
-
[fun x1 ⇒ if insub x1 is Some u then sval (
p u)
else x].
+
Definition rgd_fun (
p :
{perm T'}) :=
+
[fun x1 ⇒ if insub x1 is Some u then sval (
p u)
else x].
-
Lemma rgdP p :
injective (
rgd_fun p).
+
Lemma rgdP p :
injective (
rgd_fun p).
Definition rgd p :=
perm (@
rgdP p).
-
Lemma rfd_odd (
p :
{perm T}) :
p x = x → rfd p = p :> bool.
+
Lemma rfd_odd (
p :
{perm T}) :
p x = x → rfd p = p :> bool.
-
Lemma rfd_iso :
'C_('Alt_T)[x | 'P] \isog 'Alt_T'.
+
Lemma rfd_iso :
'C_('Alt_T)[x | 'P] \isog 'Alt_T'.
End Restrict.
-
Lemma simple_Alt5 (
T :
finType) :
#|T| ≥ 5
→ simple 'Alt_T.
+
Lemma simple_Alt5 (
T :
finType) :
#|T| ≥ 5
→ simple 'Alt_T.