From ed05182cece6bb3706e09b2ce14af4a41a2e8141 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Fri, 20 Apr 2018 10:54:22 +0200
Subject: generate the documentation for 1.7
---
docs/htmldoc/index_lemma_*.html | 478 ++++++++
docs/htmldoc/index_lemma_A.html | 1505 +++++++++++++++++++++++
docs/htmldoc/index_lemma_B.html | 1162 ++++++++++++++++++
docs/htmldoc/index_lemma_C.html | 2518 +++++++++++++++++++++++++++++++++++++++
docs/htmldoc/index_lemma_D.html | 1410 ++++++++++++++++++++++
docs/htmldoc/index_lemma_E.html | 1477 +++++++++++++++++++++++
docs/htmldoc/index_lemma_F.html | 1356 +++++++++++++++++++++
docs/htmldoc/index_lemma_G.html | 1802 ++++++++++++++++++++++++++++
docs/htmldoc/index_lemma_H.html | 1046 ++++++++++++++++
docs/htmldoc/index_lemma_I.html | 1569 ++++++++++++++++++++++++
docs/htmldoc/index_lemma_J.html | 499 ++++++++
docs/htmldoc/index_lemma_K.html | 1007 ++++++++++++++++
docs/htmldoc/index_lemma_L.html | 1396 ++++++++++++++++++++++
docs/htmldoc/index_lemma_M.html | 2258 +++++++++++++++++++++++++++++++++++
docs/htmldoc/index_lemma_N.html | 2030 +++++++++++++++++++++++++++++++
docs/htmldoc/index_lemma_O.html | 1094 +++++++++++++++++
docs/htmldoc/index_lemma_P.html | 2014 +++++++++++++++++++++++++++++++
docs/htmldoc/index_lemma_Q.html | 1091 +++++++++++++++++
docs/htmldoc/index_lemma_R.html | 1424 ++++++++++++++++++++++
docs/htmldoc/index_lemma_S.html | 1912 +++++++++++++++++++++++++++++
docs/htmldoc/index_lemma_T.html | 1115 +++++++++++++++++
docs/htmldoc/index_lemma_U.html | 1007 ++++++++++++++++
docs/htmldoc/index_lemma_V.html | 1019 ++++++++++++++++
docs/htmldoc/index_lemma_W.html | 499 ++++++++
docs/htmldoc/index_lemma_X.html | 505 ++++++++
docs/htmldoc/index_lemma_Y.html | 478 ++++++++
docs/htmldoc/index_lemma_Z.html | 1013 ++++++++++++++++
docs/htmldoc/index_lemma__.html | 478 ++++++++
28 files changed, 35162 insertions(+)
create mode 100644 docs/htmldoc/index_lemma_*.html
create mode 100644 docs/htmldoc/index_lemma_A.html
create mode 100644 docs/htmldoc/index_lemma_B.html
create mode 100644 docs/htmldoc/index_lemma_C.html
create mode 100644 docs/htmldoc/index_lemma_D.html
create mode 100644 docs/htmldoc/index_lemma_E.html
create mode 100644 docs/htmldoc/index_lemma_F.html
create mode 100644 docs/htmldoc/index_lemma_G.html
create mode 100644 docs/htmldoc/index_lemma_H.html
create mode 100644 docs/htmldoc/index_lemma_I.html
create mode 100644 docs/htmldoc/index_lemma_J.html
create mode 100644 docs/htmldoc/index_lemma_K.html
create mode 100644 docs/htmldoc/index_lemma_L.html
create mode 100644 docs/htmldoc/index_lemma_M.html
create mode 100644 docs/htmldoc/index_lemma_N.html
create mode 100644 docs/htmldoc/index_lemma_O.html
create mode 100644 docs/htmldoc/index_lemma_P.html
create mode 100644 docs/htmldoc/index_lemma_Q.html
create mode 100644 docs/htmldoc/index_lemma_R.html
create mode 100644 docs/htmldoc/index_lemma_S.html
create mode 100644 docs/htmldoc/index_lemma_T.html
create mode 100644 docs/htmldoc/index_lemma_U.html
create mode 100644 docs/htmldoc/index_lemma_V.html
create mode 100644 docs/htmldoc/index_lemma_W.html
create mode 100644 docs/htmldoc/index_lemma_X.html
create mode 100644 docs/htmldoc/index_lemma_Y.html
create mode 100644 docs/htmldoc/index_lemma_Z.html
create mode 100644 docs/htmldoc/index_lemma__.html
(limited to 'docs/htmldoc/index_lemma_*.html')
diff --git a/docs/htmldoc/index_lemma_*.html b/docs/htmldoc/index_lemma_*.html
new file mode 100644
index 0000000..c9bd28e
--- /dev/null
+++ b/docs/htmldoc/index_lemma_*.html
@@ -0,0 +1,478 @@
+
+
+
+
+
+mathcomp.ssreflect.tuple
+
+
+
+
+
+
+
+
+
+
+
+
+| Global Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(23233 entries) |
+
+
+| Notation Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(1373 entries) |
+
+
+| Module Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(213 entries) |
+
+
+| Variable Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(3475 entries) |
+
+
+| Library Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(89 entries) |
+
+
+| Lemma Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(11853 entries) |
+
+
+| Constructor Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(359 entries) |
+
+
+| Axiom Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(47 entries) |
+
+
+| Inductive Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(103 entries) |
+
+
+| Projection Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(266 entries) |
+
+
+| Section Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(1118 entries) |
+
+
+| Abbreviation Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(691 entries) |
+
+
+| Definition Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(3461 entries) |
+
+
+| Record Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(185 entries) |
+
+
+
+
+
+
+
+
+
+
\ No newline at end of file
diff --git a/docs/htmldoc/index_lemma_A.html b/docs/htmldoc/index_lemma_A.html
new file mode 100644
index 0000000..fa3086e
--- /dev/null
+++ b/docs/htmldoc/index_lemma_A.html
@@ -0,0 +1,1505 @@
+
+
+
+
+
+mathcomp.ssreflect.tuple
+
+
+
+
+
+
+
+
\ No newline at end of file
diff --git a/docs/htmldoc/index_lemma_B.html b/docs/htmldoc/index_lemma_B.html
new file mode 100644
index 0000000..3f21f60
--- /dev/null
+++ b/docs/htmldoc/index_lemma_B.html
@@ -0,0 +1,1162 @@
+
+
+
+
+
+mathcomp.ssreflect.tuple
+
+
+
+
+
+
+
+
\ No newline at end of file
diff --git a/docs/htmldoc/index_lemma_C.html b/docs/htmldoc/index_lemma_C.html
new file mode 100644
index 0000000..accf48b
--- /dev/null
+++ b/docs/htmldoc/index_lemma_C.html
@@ -0,0 +1,2518 @@
+
+
+
+
+
+mathcomp.ssreflect.tuple
+
+
+
+
+
+
+
+
\ No newline at end of file
diff --git a/docs/htmldoc/index_lemma_D.html b/docs/htmldoc/index_lemma_D.html
new file mode 100644
index 0000000..0ec853a
--- /dev/null
+++ b/docs/htmldoc/index_lemma_D.html
@@ -0,0 +1,1410 @@
+
+
+
+
+
+mathcomp.ssreflect.tuple
+
+
+
+
+
+
+
+
\ No newline at end of file
diff --git a/docs/htmldoc/index_lemma_E.html b/docs/htmldoc/index_lemma_E.html
new file mode 100644
index 0000000..0e90174
--- /dev/null
+++ b/docs/htmldoc/index_lemma_E.html
@@ -0,0 +1,1477 @@
+
+
+
+
+
+mathcomp.ssreflect.tuple
+
+
+
+
+
+
+
+
\ No newline at end of file
diff --git a/docs/htmldoc/index_lemma_F.html b/docs/htmldoc/index_lemma_F.html
new file mode 100644
index 0000000..97a2f94
--- /dev/null
+++ b/docs/htmldoc/index_lemma_F.html
@@ -0,0 +1,1356 @@
+
+
+
+
+
+mathcomp.ssreflect.tuple
+
+
+
+
+
+
+
+
\ No newline at end of file
diff --git a/docs/htmldoc/index_lemma_G.html b/docs/htmldoc/index_lemma_G.html
new file mode 100644
index 0000000..f91903a
--- /dev/null
+++ b/docs/htmldoc/index_lemma_G.html
@@ -0,0 +1,1802 @@
+
+
+
+
+
+mathcomp.ssreflect.tuple
+
+
+
+
+
+
+
+
\ No newline at end of file
diff --git a/docs/htmldoc/index_lemma_H.html b/docs/htmldoc/index_lemma_H.html
new file mode 100644
index 0000000..85ef710
--- /dev/null
+++ b/docs/htmldoc/index_lemma_H.html
@@ -0,0 +1,1046 @@
+
+
+
+
+
+mathcomp.ssreflect.tuple
+
+
+
+
+
+
+
+
\ No newline at end of file
diff --git a/docs/htmldoc/index_lemma_I.html b/docs/htmldoc/index_lemma_I.html
new file mode 100644
index 0000000..e7eb210
--- /dev/null
+++ b/docs/htmldoc/index_lemma_I.html
@@ -0,0 +1,1569 @@
+
+
+
+
+
+mathcomp.ssreflect.tuple
+
+
+
+
+
+
+
+
\ No newline at end of file
diff --git a/docs/htmldoc/index_lemma_J.html b/docs/htmldoc/index_lemma_J.html
new file mode 100644
index 0000000..ade4879
--- /dev/null
+++ b/docs/htmldoc/index_lemma_J.html
@@ -0,0 +1,499 @@
+
+
+
+
+
+mathcomp.ssreflect.tuple
+
+
+
+
+
+
+
+
+
+
+
+
+| Global Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(23233 entries) |
+
+
+| Notation Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(1373 entries) |
+
+
+| Module Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(213 entries) |
+
+
+| Variable Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(3475 entries) |
+
+
+| Library Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(89 entries) |
+
+
+| Lemma Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(11853 entries) |
+
+
+| Constructor Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(359 entries) |
+
+
+| Axiom Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(47 entries) |
+
+
+| Inductive Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(103 entries) |
+
+
+| Projection Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(266 entries) |
+
+
+| Section Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(1118 entries) |
+
+
+| Abbreviation Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(691 entries) |
+
+
+| Definition Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(3461 entries) |
+
+
+| Record Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(185 entries) |
+
+
+
J (lemma)
+
joinGA [in
mathcomp.fingroup.fingroup]
+
joingA [in
mathcomp.fingroup.fingroup]
+
joinGC [in
mathcomp.fingroup.fingroup]
+
joingC [in
mathcomp.fingroup.fingroup]
+
joinGE [in
mathcomp.fingroup.fingroup]
+
joingE [in
mathcomp.fingroup.fingroup]
+
joingG1 [in
mathcomp.fingroup.fingroup]
+
joing_sub [in
mathcomp.fingroup.fingroup]
+
joing_subP [in
mathcomp.fingroup.fingroup]
+
joing_idPr [in
mathcomp.fingroup.fingroup]
+
joing_idPl [in
mathcomp.fingroup.fingroup]
+
joing_subr [in
mathcomp.fingroup.fingroup]
+
joing_subl [in
mathcomp.fingroup.fingroup]
+
joing_idl [in
mathcomp.fingroup.fingroup]
+
joing_idr [in
mathcomp.fingroup.fingroup]
+
joinG1 [in
mathcomp.fingroup.fingroup]
+
joing1G [in
mathcomp.fingroup.fingroup]
+
join_subG [in
mathcomp.fingroup.fingroup]
+
join1G [in
mathcomp.fingroup.fingroup]
+
JordanHolderUniqueness [in
mathcomp.solvable.jordanholder]
+
+
+
+
+
+
+
+
\ No newline at end of file
diff --git a/docs/htmldoc/index_lemma_K.html b/docs/htmldoc/index_lemma_K.html
new file mode 100644
index 0000000..87a0ee2
--- /dev/null
+++ b/docs/htmldoc/index_lemma_K.html
@@ -0,0 +1,1007 @@
+
+
+
+
+
+mathcomp.ssreflect.tuple
+
+
+
+
+
+
+
+
+
+
+
+
+| Global Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(23233 entries) |
+
+
+| Notation Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(1373 entries) |
+
+
+| Module Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(213 entries) |
+
+
+| Variable Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(3475 entries) |
+
+
+| Library Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(89 entries) |
+
+
+| Lemma Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(11853 entries) |
+
+
+| Constructor Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(359 entries) |
+
+
+| Axiom Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(47 entries) |
+
+
+| Inductive Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(103 entries) |
+
+
+| Projection Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(266 entries) |
+
+
+| Section Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(1118 entries) |
+
+
+| Abbreviation Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(691 entries) |
+
+
+| Definition Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(3461 entries) |
+
+
+| Record Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(185 entries) |
+
+
+
K (lemma)
+
kAHomP [in
mathcomp.field.galois]
+
kAutE [in
mathcomp.field.galois]
+
kAutfE [in
mathcomp.field.galois]
+
kAutf_lker0 [in
mathcomp.field.galois]
+
kAutS [in
mathcomp.field.galois]
+
kAut_to_gal [in
mathcomp.field.galois]
+
kAut_eq [in
mathcomp.field.galois]
+
kAut1E [in
mathcomp.field.galois]
+
kercoset_rcoset [in
mathcomp.fingroup.quotient]
+
kerE [in
mathcomp.fingroup.morphism]
+
kermx_centg_module [in
mathcomp.character.mxrepresentation]
+
kermx_hom_module [in
mathcomp.character.mxrepresentation]
+
kermx_eq0 [in
mathcomp.algebra.mxalgebra]
+
kerP [in
mathcomp.fingroup.morphism]
+
ker_quotm [in
mathcomp.fingroup.quotient]
+
ker_coset [in
mathcomp.fingroup.quotient]
+
ker_coset_prim [in
mathcomp.fingroup.quotient]
+
ker_irr_comp_op [in
mathcomp.character.mxrepresentation]
+
ker_dprodm [in
mathcomp.fingroup.gproduct]
+
ker_cprodm [in
mathcomp.fingroup.gproduct]
+
ker_sdprodm [in
mathcomp.fingroup.gproduct]
+
ker_pprodm [in
mathcomp.fingroup.gproduct]
+
ker_conj_aut [in
mathcomp.fingroup.automorphism]
+
ker_autm [in
mathcomp.fingroup.automorphism]
+
ker_restr_perm [in
mathcomp.fingroup.action]
+
ker_actperm [in
mathcomp.fingroup.action]
+
ker_reprGLm [in
mathcomp.character.mxabelem]
+
ker_subg [in
mathcomp.fingroup.morphism]
+
ker_sgval [in
mathcomp.fingroup.morphism]
+
ker_ifactm [in
mathcomp.fingroup.morphism]
+
ker_invm [in
mathcomp.fingroup.morphism]
+
ker_factm_loc [in
mathcomp.fingroup.morphism]
+
ker_factm [in
mathcomp.fingroup.morphism]
+
ker_comp [in
mathcomp.fingroup.morphism]
+
ker_trivm [in
mathcomp.fingroup.morphism]
+
ker_restrm [in
mathcomp.fingroup.morphism]
+
ker_idm [in
mathcomp.fingroup.morphism]
+
ker_injm [in
mathcomp.fingroup.morphism]
+
ker_trivg_morphim [in
mathcomp.fingroup.morphism]
+
ker_normal_pre [in
mathcomp.fingroup.morphism]
+
ker_sub_pre [in
mathcomp.fingroup.morphism]
+
ker_normal [in
mathcomp.fingroup.morphism]
+
ker_norm [in
mathcomp.fingroup.morphism]
+
ker_rcoset [in
mathcomp.fingroup.morphism]
+
ker_in_cprod [in
mathcomp.solvable.center]
+
ker_cprod_by_central [in
mathcomp.solvable.center]
+
ker_cprod_by_is_group [in
mathcomp.solvable.center]
+
ker_sub_ahom_is_aspace [in
mathcomp.field.falgebra]
+
ker_eltm [in
mathcomp.solvable.cyclic]
+
kHomExtendE [in
mathcomp.field.galois]
+
kHomExtendP [in
mathcomp.field.galois]
+
kHomExtend_poly [in
mathcomp.field.galois]
+
kHomExtend_val [in
mathcomp.field.galois]
+
kHomExtend_id [in
mathcomp.field.galois]
+
kHomExtend_subproof [in
mathcomp.field.galois]
+
kHomP [in
mathcomp.field.galois]
+
kHomS [in
mathcomp.field.galois]
+
kHomSl [in
mathcomp.field.galois]
+
kHomSr [in
mathcomp.field.galois]
+
kHom_to_gal [in
mathcomp.field.galois]
+
kHom_to_AEnd [in
mathcomp.field.galois]
+
kHom_extends [in
mathcomp.field.galois]
+
kHom_kAut_sub [in
mathcomp.field.galois]
+
kHom_root_id [in
mathcomp.field.galois]
+
kHom_root [in
mathcomp.field.galois]
+
kHom_horner [in
mathcomp.field.galois]
+
kHom_is_rmorphism [in
mathcomp.field.galois]
+
kHom_dim [in
mathcomp.field.galois]
+
kHom_inv [in
mathcomp.field.galois]
+
kHom_eq [in
mathcomp.field.galois]
+
kHom_poly_id [in
mathcomp.field.galois]
+
kHom_lrmorphism [in
mathcomp.field.galois]
+
kHom1 [in
mathcomp.field.galois]
+
kquo_mx_faithful [in
mathcomp.character.mxrepresentation]
+
kquo_repr_coset [in
mathcomp.character.mxrepresentation]
+
kquo_mxE [in
mathcomp.character.mxrepresentation]
+
k1AHom [in
mathcomp.field.galois]
+
k1HomE [in
mathcomp.field.galois]
+
+
+| Global Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(23233 entries) |
+
+
+| Notation Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(1373 entries) |
+
+
+| Module Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(213 entries) |
+
+
+| Variable Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(3475 entries) |
+
+
+| Library Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(89 entries) |
+
+
+| Lemma Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(11853 entries) |
+
+
+| Constructor Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(359 entries) |
+
+
+| Axiom Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(47 entries) |
+
+
+| Inductive Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(103 entries) |
+
+
+| Projection Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(266 entries) |
+
+
+| Section Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(1118 entries) |
+
+
+| Abbreviation Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(691 entries) |
+
+
+| Definition Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(3461 entries) |
+
+
+| Record Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(185 entries) |
+
+
+
+
+
+
+
+
+
+
\ No newline at end of file
diff --git a/docs/htmldoc/index_lemma_L.html b/docs/htmldoc/index_lemma_L.html
new file mode 100644
index 0000000..01a0b94
--- /dev/null
+++ b/docs/htmldoc/index_lemma_L.html
@@ -0,0 +1,1396 @@
+
+
+
+
+
+mathcomp.ssreflect.tuple
+
+
+
+
+
+
+
+
\ No newline at end of file
diff --git a/docs/htmldoc/index_lemma_M.html b/docs/htmldoc/index_lemma_M.html
new file mode 100644
index 0000000..72cf96d
--- /dev/null
+++ b/docs/htmldoc/index_lemma_M.html
@@ -0,0 +1,2258 @@
+
+
+
+
+
+mathcomp.ssreflect.tuple
+
+
+
+
+
+
+
+
\ No newline at end of file
diff --git a/docs/htmldoc/index_lemma_N.html b/docs/htmldoc/index_lemma_N.html
new file mode 100644
index 0000000..7d12494
--- /dev/null
+++ b/docs/htmldoc/index_lemma_N.html
@@ -0,0 +1,2030 @@
+
+
+
+
+
+mathcomp.ssreflect.tuple
+
+
+
+
+
+
+
+
\ No newline at end of file
diff --git a/docs/htmldoc/index_lemma_O.html b/docs/htmldoc/index_lemma_O.html
new file mode 100644
index 0000000..30aee80
--- /dev/null
+++ b/docs/htmldoc/index_lemma_O.html
@@ -0,0 +1,1094 @@
+
+
+
+
+
+mathcomp.ssreflect.tuple
+
+
+
+
+
+
+
+
\ No newline at end of file
diff --git a/docs/htmldoc/index_lemma_P.html b/docs/htmldoc/index_lemma_P.html
new file mode 100644
index 0000000..4907493
--- /dev/null
+++ b/docs/htmldoc/index_lemma_P.html
@@ -0,0 +1,2014 @@
+
+
+
+
+
+mathcomp.ssreflect.tuple
+
+
+
+
+
+
+
+
\ No newline at end of file
diff --git a/docs/htmldoc/index_lemma_Q.html b/docs/htmldoc/index_lemma_Q.html
new file mode 100644
index 0000000..1b966ed
--- /dev/null
+++ b/docs/htmldoc/index_lemma_Q.html
@@ -0,0 +1,1091 @@
+
+
+
+
+
+mathcomp.ssreflect.tuple
+
+
+
+
+
+
+
+
\ No newline at end of file
diff --git a/docs/htmldoc/index_lemma_R.html b/docs/htmldoc/index_lemma_R.html
new file mode 100644
index 0000000..2022c3a
--- /dev/null
+++ b/docs/htmldoc/index_lemma_R.html
@@ -0,0 +1,1424 @@
+
+
+
+
+
+mathcomp.ssreflect.tuple
+
+
+
+
+
+
+
+
\ No newline at end of file
diff --git a/docs/htmldoc/index_lemma_S.html b/docs/htmldoc/index_lemma_S.html
new file mode 100644
index 0000000..72d70ad
--- /dev/null
+++ b/docs/htmldoc/index_lemma_S.html
@@ -0,0 +1,1912 @@
+
+
+
+
+
+mathcomp.ssreflect.tuple
+
+
+
+
+
+
+
+
\ No newline at end of file
diff --git a/docs/htmldoc/index_lemma_T.html b/docs/htmldoc/index_lemma_T.html
new file mode 100644
index 0000000..7f8e930
--- /dev/null
+++ b/docs/htmldoc/index_lemma_T.html
@@ -0,0 +1,1115 @@
+
+
+
+
+
+mathcomp.ssreflect.tuple
+
+
+
+
+
+
+
+
\ No newline at end of file
diff --git a/docs/htmldoc/index_lemma_U.html b/docs/htmldoc/index_lemma_U.html
new file mode 100644
index 0000000..383e56e
--- /dev/null
+++ b/docs/htmldoc/index_lemma_U.html
@@ -0,0 +1,1007 @@
+
+
+
+
+
+mathcomp.ssreflect.tuple
+
+
+
+
+
+
+
+
+
+
+
+
+| Global Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(23233 entries) |
+
+
+| Notation Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(1373 entries) |
+
+
+| Module Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(213 entries) |
+
+
+| Variable Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(3475 entries) |
+
+
+| Library Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(89 entries) |
+
+
+| Lemma Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(11853 entries) |
+
+
+| Constructor Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(359 entries) |
+
+
+| Axiom Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(47 entries) |
+
+
+| Inductive Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(103 entries) |
+
+
+| Projection Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(266 entries) |
+
+
+| Section Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(1118 entries) |
+
+
+| Abbreviation Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(691 entries) |
+
+
+| Definition Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(3461 entries) |
+
+
+| Record Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(185 entries) |
+
+
+
U (lemma)
+
ucnE [in
mathcomp.solvable.nilpotent]
+
ucnP [in
mathcomp.solvable.nilpotent]
+
ucnSn [in
mathcomp.solvable.nilpotent]
+
ucnSnR [in
mathcomp.solvable.nilpotent]
+
ucn_nilpotent [in
mathcomp.solvable.nilpotent]
+
ucn_id [in
mathcomp.solvable.nilpotent]
+
ucn_nil_classP [in
mathcomp.solvable.nilpotent]
+
ucn_lcnP [in
mathcomp.solvable.nilpotent]
+
ucn_bigdprod [in
mathcomp.solvable.nilpotent]
+
ucn_bigcprod [in
mathcomp.solvable.nilpotent]
+
ucn_dprod [in
mathcomp.solvable.nilpotent]
+
ucn_cprod [in
mathcomp.solvable.nilpotent]
+
ucn_comm [in
mathcomp.solvable.nilpotent]
+
ucn_normalS [in
mathcomp.solvable.nilpotent]
+
ucn_central [in
mathcomp.solvable.nilpotent]
+
ucn_sub_geq [in
mathcomp.solvable.nilpotent]
+
ucn_subS [in
mathcomp.solvable.nilpotent]
+
ucn_normal [in
mathcomp.solvable.nilpotent]
+
ucn_norm [in
mathcomp.solvable.nilpotent]
+
ucn_char [in
mathcomp.solvable.nilpotent]
+
ucn_sub [in
mathcomp.solvable.nilpotent]
+
ucn_group_set [in
mathcomp.solvable.nilpotent]
+
ucn_pmap [in
mathcomp.solvable.nilpotent]
+
ucn0 [in
mathcomp.solvable.nilpotent]
+
ucn1 [in
mathcomp.solvable.nilpotent]
+
ucycle_uniq [in
mathcomp.ssreflect.path]
+
ucycle_cycle [in
mathcomp.ssreflect.path]
+
unbumpK [in
mathcomp.ssreflect.fintype]
+
unbumpKcond [in
mathcomp.ssreflect.fintype]
+
unbumpS [in
mathcomp.ssreflect.fintype]
+
unbump_addl [in
mathcomp.ssreflect.fintype]
+
undup_nil [in
mathcomp.ssreflect.seq]
+
undup_id [in
mathcomp.ssreflect.seq]
+
undup_uniq [in
mathcomp.ssreflect.seq]
+
uniqP [in
mathcomp.ssreflect.seq]
+
uniqPn [in
mathcomp.ssreflect.seq]
+
uniq_normal_Hall [in
mathcomp.solvable.pgroup]
+
uniq_traject_pcycle [in
mathcomp.fingroup.perm]
+
uniq_perm_eq [in
mathcomp.ssreflect.seq]
+
uniq_size_uniq [in
mathcomp.ssreflect.seq]
+
uniq_leq_size [in
mathcomp.ssreflect.seq]
+
uniq_catCA [in
mathcomp.ssreflect.seq]
+
uniq_catC [in
mathcomp.ssreflect.seq]
+
uniq_rootsE [in
mathcomp.algebra.poly]
+
uniq_roots_prod_XsubC [in
mathcomp.algebra.poly]
+
uniq4_uniq6 [in
mathcomp.solvable.burnside_app]
+
unitFpE [in
mathcomp.algebra.zmodp]
+
unitmxE [in
mathcomp.algebra.matrix]
+
unitmxZ [in
mathcomp.algebra.matrix]
+
unitmx_mul [in
mathcomp.algebra.matrix]
+
unitmx_inv [in
mathcomp.algebra.matrix]
+
unitmx_tr [in
mathcomp.algebra.matrix]
+
unitmx_perm [in
mathcomp.algebra.matrix]
+
unitmx1 [in
mathcomp.algebra.matrix]
+
unitrXz [in
mathcomp.algebra.ssrint]
+
unitr_trmx [in
mathcomp.algebra.matrix]
+
unitr_n0expz [in
mathcomp.algebra.ssrint]
+
unitr_algid1 [in
mathcomp.field.falgebra]
+
units_Zp_abelian [in
mathcomp.algebra.zmodp]
+
unity_rootP [in
mathcomp.algebra.poly]
+
unity_rootE [in
mathcomp.algebra.poly]
+
unitZpE [in
mathcomp.algebra.zmodp]
+
unit_ring_quot_mixinP [in
mathcomp.algebra.ring_quotient]
+
unit_enumP [in
mathcomp.ssreflect.fintype]
+
unit_eqP [in
mathcomp.ssreflect.eqtype]
+
unit_Zp_expg [in
mathcomp.algebra.zmodp]
+
unit_Zp_mulgC [in
mathcomp.algebra.zmodp]
+
unliftP [in
mathcomp.ssreflect.fintype]
+
unlift_some [in
mathcomp.ssreflect.fintype]
+
unlift_none [in
mathcomp.ssreflect.fintype]
+
unlift_subproof [in
mathcomp.ssreflect.fintype]
+
unsplitK [in
mathcomp.ssreflect.fintype]
+
unzip1_zip [in
mathcomp.ssreflect.seq]
+
unzip2_zip [in
mathcomp.ssreflect.seq]
+
uphalf_half [in
mathcomp.ssreflect.ssrnat]
+
uphalf_double [in
mathcomp.ssreflect.ssrnat]
+
usubmx_key [in
mathcomp.algebra.matrix]
+
usumx_mul [in
mathcomp.character.character]
+
+
+| Global Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(23233 entries) |
+
+
+| Notation Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(1373 entries) |
+
+
+| Module Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(213 entries) |
+
+
+| Variable Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(3475 entries) |
+
+
+| Library Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(89 entries) |
+
+
+| Lemma Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(11853 entries) |
+
+
+| Constructor Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(359 entries) |
+
+
+| Axiom Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(47 entries) |
+
+
+| Inductive Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(103 entries) |
+
+
+| Projection Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(266 entries) |
+
+
+| Section Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(1118 entries) |
+
+
+| Abbreviation Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(691 entries) |
+
+
+| Definition Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(3461 entries) |
+
+
+| Record Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(185 entries) |
+
+
+
+
+
+
+
+
+
+
\ No newline at end of file
diff --git a/docs/htmldoc/index_lemma_V.html b/docs/htmldoc/index_lemma_V.html
new file mode 100644
index 0000000..cb73143
--- /dev/null
+++ b/docs/htmldoc/index_lemma_V.html
@@ -0,0 +1,1019 @@
+
+
+
+
+
+mathcomp.ssreflect.tuple
+
+
+
+
+
+
+
+
\ No newline at end of file
diff --git a/docs/htmldoc/index_lemma_W.html b/docs/htmldoc/index_lemma_W.html
new file mode 100644
index 0000000..569bf93
--- /dev/null
+++ b/docs/htmldoc/index_lemma_W.html
@@ -0,0 +1,499 @@
+
+
+
+
+
+mathcomp.ssreflect.tuple
+
+
+
+
+
+
+
+
+
+
+
+
+| Global Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(23233 entries) |
+
+
+| Notation Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(1373 entries) |
+
+
+| Module Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(213 entries) |
+
+
+| Variable Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(3475 entries) |
+
+
+| Library Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(89 entries) |
+
+
+| Lemma Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(11853 entries) |
+
+
+| Constructor Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(359 entries) |
+
+
+| Axiom Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(47 entries) |
+
+
+| Inductive Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(103 entries) |
+
+
+| Projection Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(266 entries) |
+
+
+| Section Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(1118 entries) |
+
+
+| Abbreviation Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(691 entries) |
+
+
+| Definition Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(3461 entries) |
+
+
+| Record Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(185 entries) |
+
+
+
W (lemma)
+
weak_second_isog [in
mathcomp.fingroup.quotient]
+
Wedderburn_center [in
mathcomp.character.mxrepresentation]
+
Wedderburn_subring_center [in
mathcomp.character.mxrepresentation]
+
Wedderburn_min_ideal [in
mathcomp.character.mxrepresentation]
+
Wedderburn_is_ring [in
mathcomp.character.mxrepresentation]
+
Wedderburn_closed [in
mathcomp.character.mxrepresentation]
+
Wedderburn_is_id [in
mathcomp.character.mxrepresentation]
+
Wedderburn_id_mem [in
mathcomp.character.mxrepresentation]
+
Wedderburn_sum_id [in
mathcomp.character.mxrepresentation]
+
Wedderburn_sum [in
mathcomp.character.mxrepresentation]
+
Wedderburn_mulmx0 [in
mathcomp.character.mxrepresentation]
+
Wedderburn_annihilate [in
mathcomp.character.mxrepresentation]
+
Wedderburn_disjoint [in
mathcomp.character.mxrepresentation]
+
Wedderburn_direct [in
mathcomp.character.mxrepresentation]
+
Wedderburn_ideal [in
mathcomp.character.mxrepresentation]
+
Wedderburn_id_expansion [in
mathcomp.character.character]
+
wf_ex_elim [in
mathcomp.field.closed_field]
+
widen_partn [in
mathcomp.ssreflect.prime]
+
widen_ord_proof [in
mathcomp.ssreflect.fintype]
+
Wilson [in
mathcomp.ssreflect.binomial]
+
+
+
+
+
+
+
+
\ No newline at end of file
diff --git a/docs/htmldoc/index_lemma_X.html b/docs/htmldoc/index_lemma_X.html
new file mode 100644
index 0000000..5caf809
--- /dev/null
+++ b/docs/htmldoc/index_lemma_X.html
@@ -0,0 +1,505 @@
+
+
+
+
+
+mathcomp.ssreflect.tuple
+
+
+
+
+
+
+
+
+
+
+
+
+| Global Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(23233 entries) |
+
+
+| Notation Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(1373 entries) |
+
+
+| Module Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(213 entries) |
+
+
+| Variable Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(3475 entries) |
+
+
+| Library Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(89 entries) |
+
+
+| Lemma Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(11853 entries) |
+
+
+| Constructor Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(359 entries) |
+
+
+| Axiom Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(47 entries) |
+
+
+| Inductive Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(103 entries) |
+
+
+| Projection Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(266 entries) |
+
+
+| Section Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(1118 entries) |
+
+
+| Abbreviation Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(691 entries) |
+
+
+| Definition Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(3461 entries) |
+
+
+| Record Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(185 entries) |
+
+
+
X (lemma)
+
xcfunG [in
mathcomp.character.character]
+
xcfunZl [in
mathcomp.character.character]
+
xcfunZr [in
mathcomp.character.character]
+
xcfun_id [in
mathcomp.character.character]
+
xcfun_mul_id [in
mathcomp.character.character]
+
xcfun_annihilate [in
mathcomp.character.character]
+
xcfun_repr [in
mathcomp.character.character]
+
xcfun_r_is_additive [in
mathcomp.character.character]
+
xcfun_rE [in
mathcomp.character.character]
+
xcfun_is_additive [in
mathcomp.character.character]
+
xchooseP [in
mathcomp.ssreflect.choice]
+
xcolE [in
mathcomp.algebra.matrix]
+
xcol_const [in
mathcomp.algebra.matrix]
+
xcprodmE [in
mathcomp.solvable.center]
+
xcprodmEl [in
mathcomp.solvable.center]
+
xcprodmEr [in
mathcomp.solvable.center]
+
xcprodmI [in
mathcomp.solvable.center]
+
xcprodm_cent [in
mathcomp.solvable.center]
+
xcprodP [in
mathcomp.solvable.center]
+
xcprod_subproof [in
mathcomp.solvable.center]
+
xpair_eqE [in
mathcomp.ssreflect.eqtype]
+
xrowE [in
mathcomp.algebra.matrix]
+
xrow_const [in
mathcomp.algebra.matrix]
+
xsdprodm_act [in
mathcomp.fingroup.gproduct]
+
xsdprodm_dom2 [in
mathcomp.fingroup.gproduct]
+
xsdprodm_dom1 [in
mathcomp.fingroup.gproduct]
+
+
+
+
+
+
+
+
\ No newline at end of file
diff --git a/docs/htmldoc/index_lemma_Y.html b/docs/htmldoc/index_lemma_Y.html
new file mode 100644
index 0000000..c9bd28e
--- /dev/null
+++ b/docs/htmldoc/index_lemma_Y.html
@@ -0,0 +1,478 @@
+
+
+
+
+
+mathcomp.ssreflect.tuple
+
+
+
+
+
+
+
+
+
+
+
+
+| Global Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(23233 entries) |
+
+
+| Notation Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(1373 entries) |
+
+
+| Module Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(213 entries) |
+
+
+| Variable Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(3475 entries) |
+
+
+| Library Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(89 entries) |
+
+
+| Lemma Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(11853 entries) |
+
+
+| Constructor Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(359 entries) |
+
+
+| Axiom Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(47 entries) |
+
+
+| Inductive Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(103 entries) |
+
+
+| Projection Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(266 entries) |
+
+
+| Section Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(1118 entries) |
+
+
+| Abbreviation Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(691 entries) |
+
+
+| Definition Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(3461 entries) |
+
+
+| Record Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(185 entries) |
+
+
+
+
+
+
+
+
+
+
\ No newline at end of file
diff --git a/docs/htmldoc/index_lemma_Z.html b/docs/htmldoc/index_lemma_Z.html
new file mode 100644
index 0000000..79874c2
--- /dev/null
+++ b/docs/htmldoc/index_lemma_Z.html
@@ -0,0 +1,1013 @@
+
+
+
+
+
+mathcomp.ssreflect.tuple
+
+
+
+
+
+
+
+
+
+
+
+
+| Global Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(23233 entries) |
+
+
+| Notation Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(1373 entries) |
+
+
+| Module Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(213 entries) |
+
+
+| Variable Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(3475 entries) |
+
+
+| Library Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(89 entries) |
+
+
+| Lemma Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(11853 entries) |
+
+
+| Constructor Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(359 entries) |
+
+
+| Axiom Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(47 entries) |
+
+
+| Inductive Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(103 entries) |
+
+
+| Projection Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(266 entries) |
+
+
+| Section Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(1118 entries) |
+
+
+| Abbreviation Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(691 entries) |
+
+
+| Definition Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(3461 entries) |
+
+
+| Record Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(185 entries) |
+
+
+
Z (lemma)
+
zcharD1 [in
mathcomp.character.vcharacter]
+
zcharD1E [in
mathcomp.character.vcharacter]
+
zcharW [in
mathcomp.character.vcharacter]
+
zchar_small_norm [in
mathcomp.character.vcharacter]
+
zchar_filter [in
mathcomp.character.vcharacter]
+
zchar_subseq [in
mathcomp.character.vcharacter]
+
zchar_subset [in
mathcomp.character.vcharacter]
+
zchar_sub_irr [in
mathcomp.character.vcharacter]
+
zchar_trans_on [in
mathcomp.character.vcharacter]
+
zchar_trans [in
mathcomp.character.vcharacter]
+
zchar_span [in
mathcomp.character.vcharacter]
+
zchar_expansion [in
mathcomp.character.vcharacter]
+
zchar_tuple_expansion [in
mathcomp.character.vcharacter]
+
zchar_nth_expansion [in
mathcomp.character.vcharacter]
+
zchar_onG [in
mathcomp.character.vcharacter]
+
zchar_onS [in
mathcomp.character.vcharacter]
+
zchar_on [in
mathcomp.character.vcharacter]
+
zchar_split [in
mathcomp.character.vcharacter]
+
Zchar_zmod [in
mathcomp.character.vcharacter]
+
Zchar_key [in
mathcomp.character.vcharacter]
+
zchinese_mod [in
mathcomp.algebra.intdiv]
+
zchinese_modr [in
mathcomp.algebra.intdiv]
+
zchinese_modl [in
mathcomp.algebra.intdiv]
+
zchinese_remainder [in
mathcomp.algebra.intdiv]
+
zcontentsM [in
mathcomp.algebra.intdiv]
+
zcontentsZ [in
mathcomp.algebra.intdiv]
+
zcontents_primitive [in
mathcomp.algebra.intdiv]
+
zcontents_monic [in
mathcomp.algebra.intdiv]
+
zcontents_eq0 [in
mathcomp.algebra.intdiv]
+
zcontents0 [in
mathcomp.algebra.intdiv]
+
zero_lfunE [in
mathcomp.algebra.vector]
+
ZgroupS [in
mathcomp.solvable.sylow]
+
zip_tupleP [in
mathcomp.ssreflect.tuple]
+
zip_rcons [in
mathcomp.ssreflect.seq]
+
zip_cat [in
mathcomp.ssreflect.seq]
+
zip_unzip [in
mathcomp.ssreflect.seq]
+
Zisometry_inj [in
mathcomp.character.vcharacter]
+
Zisometry_of_iso [in
mathcomp.character.vcharacter]
+
Zisometry_of_cfnorm [in
mathcomp.character.vcharacter]
+
zmod_quot_mixinP [in
mathcomp.algebra.ring_quotient]
+
ZnatP [in
mathcomp.algebra.ssrint]
+
Znat_semiring_closed [in
mathcomp.algebra.ssrint]
+
Znat_def [in
mathcomp.algebra.ssrint]
+
Znat_key [in
mathcomp.algebra.ssrint]
+
ZpmM [in
mathcomp.solvable.cyclic]
+
zpolyEprim [in
mathcomp.algebra.intdiv]
+
zprimitiveM [in
mathcomp.algebra.intdiv]
+
zprimitiveZ [in
mathcomp.algebra.intdiv]
+
zprimitive_irr [in
mathcomp.algebra.intdiv]
+
zprimitive_min [in
mathcomp.algebra.intdiv]
+
zprimitive_monic [in
mathcomp.algebra.intdiv]
+
zprimitive_id [in
mathcomp.algebra.intdiv]
+
zprimitive_eq0 [in
mathcomp.algebra.intdiv]
+
zprimitive0 [in
mathcomp.algebra.intdiv]
+
Zp_group_set [in
mathcomp.algebra.zmodp]
+
Zp_nat_mod [in
mathcomp.algebra.zmodp]
+
Zp_cast [in
mathcomp.algebra.zmodp]
+
Zp_nat [in
mathcomp.algebra.zmodp]
+
Zp_nontrivial [in
mathcomp.algebra.zmodp]
+
Zp_cycle [in
mathcomp.algebra.zmodp]
+
Zp_expg [in
mathcomp.algebra.zmodp]
+
Zp_abelian [in
mathcomp.algebra.zmodp]
+
Zp_mulgC [in
mathcomp.algebra.zmodp]
+
Zp_mulrn [in
mathcomp.algebra.zmodp]
+
Zp_inv_out [in
mathcomp.algebra.zmodp]
+
Zp_intro_unit [in
mathcomp.algebra.zmodp]
+
Zp_mulzV [in
mathcomp.algebra.zmodp]
+
Zp_mulVz [in
mathcomp.algebra.zmodp]
+
Zp_mul_addl [in
mathcomp.algebra.zmodp]
+
Zp_mul_addr [in
mathcomp.algebra.zmodp]
+
Zp_mulA [in
mathcomp.algebra.zmodp]
+
Zp_mulz1 [in
mathcomp.algebra.zmodp]
+
Zp_mulC [in
mathcomp.algebra.zmodp]
+
Zp_mul1z [in
mathcomp.algebra.zmodp]
+
Zp_addC [in
mathcomp.algebra.zmodp]
+
Zp_addA [in
mathcomp.algebra.zmodp]
+
Zp_addNz [in
mathcomp.algebra.zmodp]
+
Zp_add0z [in
mathcomp.algebra.zmodp]
+
Zp_unit_isog [in
mathcomp.solvable.cyclic]
+
Zp_unit_isom [in
mathcomp.solvable.cyclic]
+
Zp_unitmM [in
mathcomp.solvable.cyclic]
+
Zp_isog [in
mathcomp.solvable.cyclic]
+
Zp_isom [in
mathcomp.solvable.cyclic]
+
Zp1_expgz [in
mathcomp.algebra.zmodp]
+
+
+| Global Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(23233 entries) |
+
+
+| Notation Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(1373 entries) |
+
+
+| Module Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(213 entries) |
+
+
+| Variable Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(3475 entries) |
+
+
+| Library Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(89 entries) |
+
+
+| Lemma Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(11853 entries) |
+
+
+| Constructor Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(359 entries) |
+
+
+| Axiom Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(47 entries) |
+
+
+| Inductive Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(103 entries) |
+
+
+| Projection Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(266 entries) |
+
+
+| Section Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(1118 entries) |
+
+
+| Abbreviation Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(691 entries) |
+
+
+| Definition Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(3461 entries) |
+
+
+| Record Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(185 entries) |
+
+
+
+
+
+
+
+
+
+
\ No newline at end of file
diff --git a/docs/htmldoc/index_lemma__.html b/docs/htmldoc/index_lemma__.html
new file mode 100644
index 0000000..c9bd28e
--- /dev/null
+++ b/docs/htmldoc/index_lemma__.html
@@ -0,0 +1,478 @@
+
+
+
+
+
+mathcomp.ssreflect.tuple
+
+
+
+
+
+
+
+
+
+
+
+
+| Global Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(23233 entries) |
+
+
+| Notation Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(1373 entries) |
+
+
+| Module Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(213 entries) |
+
+
+| Variable Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(3475 entries) |
+
+
+| Library Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(89 entries) |
+
+
+| Lemma Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(11853 entries) |
+
+
+| Constructor Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(359 entries) |
+
+
+| Axiom Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(47 entries) |
+
+
+| Inductive Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(103 entries) |
+
+
+| Projection Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(266 entries) |
+
+
+| Section Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(1118 entries) |
+
+
+| Abbreviation Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(691 entries) |
+
+
+| Definition Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(3461 entries) |
+
+
+| Record Index |
+A |
+B |
+C |
+D |
+E |
+F |
+G |
+H |
+I |
+J |
+K |
+L |
+M |
+N |
+O |
+P |
+Q |
+R |
+S |
+T |
+U |
+V |
+W |
+X |
+Y |
+Z |
+_ |
+other |
+(185 entries) |
+
+
+
+
+
+
+
+
+
+
\ No newline at end of file
--
cgit v1.2.3