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_notation_*.html | 1876 ++++++++++++++++++++++++++++++++++++
docs/htmldoc/index_notation_A.html | 486 ++++++++++
docs/htmldoc/index_notation_B.html | 480 +++++++++
docs/htmldoc/index_notation_C.html | 503 ++++++++++
docs/htmldoc/index_notation_D.html | 486 ++++++++++
docs/htmldoc/index_notation_E.html | 482 +++++++++
docs/htmldoc/index_notation_F.html | 1010 +++++++++++++++++++
docs/htmldoc/index_notation_G.html | 1054 ++++++++++++++++++++
docs/htmldoc/index_notation_H.html | 478 +++++++++
docs/htmldoc/index_notation_I.html | 961 ++++++++++++++++++
docs/htmldoc/index_notation_J.html | 478 +++++++++
docs/htmldoc/index_notation_K.html | 480 +++++++++
docs/htmldoc/index_notation_L.html | 480 +++++++++
docs/htmldoc/index_notation_M.html | 962 ++++++++++++++++++
docs/htmldoc/index_notation_N.html | 988 +++++++++++++++++++
docs/htmldoc/index_notation_O.html | 478 +++++++++
docs/htmldoc/index_notation_P.html | 498 ++++++++++
docs/htmldoc/index_notation_Q.html | 481 +++++++++
docs/htmldoc/index_notation_R.html | 496 ++++++++++
docs/htmldoc/index_notation_S.html | 485 ++++++++++
docs/htmldoc/index_notation_T.html | 478 +++++++++
docs/htmldoc/index_notation_U.html | 481 +++++++++
docs/htmldoc/index_notation_V.html | 484 ++++++++++
docs/htmldoc/index_notation_W.html | 478 +++++++++
docs/htmldoc/index_notation_X.html | 478 +++++++++
docs/htmldoc/index_notation_Y.html | 478 +++++++++
docs/htmldoc/index_notation_Z.html | 480 +++++++++
docs/htmldoc/index_notation__.html | 478 +++++++++
28 files changed, 17477 insertions(+)
create mode 100644 docs/htmldoc/index_notation_*.html
create mode 100644 docs/htmldoc/index_notation_A.html
create mode 100644 docs/htmldoc/index_notation_B.html
create mode 100644 docs/htmldoc/index_notation_C.html
create mode 100644 docs/htmldoc/index_notation_D.html
create mode 100644 docs/htmldoc/index_notation_E.html
create mode 100644 docs/htmldoc/index_notation_F.html
create mode 100644 docs/htmldoc/index_notation_G.html
create mode 100644 docs/htmldoc/index_notation_H.html
create mode 100644 docs/htmldoc/index_notation_I.html
create mode 100644 docs/htmldoc/index_notation_J.html
create mode 100644 docs/htmldoc/index_notation_K.html
create mode 100644 docs/htmldoc/index_notation_L.html
create mode 100644 docs/htmldoc/index_notation_M.html
create mode 100644 docs/htmldoc/index_notation_N.html
create mode 100644 docs/htmldoc/index_notation_O.html
create mode 100644 docs/htmldoc/index_notation_P.html
create mode 100644 docs/htmldoc/index_notation_Q.html
create mode 100644 docs/htmldoc/index_notation_R.html
create mode 100644 docs/htmldoc/index_notation_S.html
create mode 100644 docs/htmldoc/index_notation_T.html
create mode 100644 docs/htmldoc/index_notation_U.html
create mode 100644 docs/htmldoc/index_notation_V.html
create mode 100644 docs/htmldoc/index_notation_W.html
create mode 100644 docs/htmldoc/index_notation_X.html
create mode 100644 docs/htmldoc/index_notation_Y.html
create mode 100644 docs/htmldoc/index_notation_Z.html
create mode 100644 docs/htmldoc/index_notation__.html
(limited to 'docs/htmldoc/index_notation_*.html')
diff --git a/docs/htmldoc/index_notation_*.html b/docs/htmldoc/index_notation_*.html
new file mode 100644
index 0000000..b464b44
--- /dev/null
+++ b/docs/htmldoc/index_notation_*.html
@@ -0,0 +1,1876 @@
+
+
+
+
+
+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) |
+
+
+
other (notation)
+
'M[ _ ] ( _ ) (abelem_scope) [in
mathcomp.character.mxabelem]
+
'rV[ _ ] ( _ ) (abelem_scope) [in
mathcomp.character.mxabelem]
+
'M ( _ ) (abelem_scope) [in
mathcomp.character.mxabelem]
+
'rV ( _ ) (abelem_scope) [in
mathcomp.character.mxabelem]
+
'dim _ (abelem_scope) [in
mathcomp.character.mxabelem]
+
_ * _ (action_scope) [in
mathcomp.solvable.primitive_action]
+
'Cl (action_scope) [in
mathcomp.character.mxrepresentation]
+
'U (action_scope) [in
mathcomp.algebra.finalg]
+
[ Aut _ ] (action_scope) [in
mathcomp.fingroup.action]
+
'Q (action_scope) [in
mathcomp.fingroup.action]
+
'JG (action_scope) [in
mathcomp.fingroup.action]
+
'Js (action_scope) [in
mathcomp.fingroup.action]
+
'J (action_scope) [in
mathcomp.fingroup.action]
+
'Rs (action_scope) [in
mathcomp.fingroup.action]
+
'R (action_scope) [in
mathcomp.fingroup.action]
+
'P (action_scope) [in
mathcomp.fingroup.action]
+
_ \o _ (action_scope) [in
mathcomp.fingroup.action]
+
<< _ >> (action_scope) [in
mathcomp.fingroup.action]
+
_ %% _ (action_scope) [in
mathcomp.fingroup.action]
+
_ / _ (action_scope) [in
mathcomp.fingroup.action]
+
_ ^? (action_scope) [in
mathcomp.fingroup.action]
+
<[ _ ] > (action_scope) [in
mathcomp.fingroup.action]
+
_ \ _ (action_scope) [in
mathcomp.fingroup.action]
+
_ ^* (action_scope) [in
mathcomp.fingroup.action]
+
'Zm (action_scope) [in
mathcomp.character.mxabelem]
+
'MR _ (action_scope) [in
mathcomp.character.mxabelem]
+
_ != _ %[mod _ ] (algC_scope) [in
mathcomp.field.algnum]
+
_ == _ %[mod _ ] (algC_scope) [in
mathcomp.field.algnum]
+
_ %| _ (algC_scope) [in
mathcomp.field.algnum]
+
_ %| _ (algC_expanded_scope) [in
mathcomp.field.algnum]
+
_ @: _ (aspace_scope) [in
mathcomp.field.fieldext]
+
_ * _ (aspace_scope) [in
mathcomp.field.fieldext]
+
'C_ ( _ ) ( _ ) (aspace_scope) [in
mathcomp.field.fieldext]
+
'C_ _ ( _ ) (aspace_scope) [in
mathcomp.field.fieldext]
+
'C_ ( _ ) [ _ ] (aspace_scope) [in
mathcomp.field.fieldext]
+
'C_ _ [ _ ] (aspace_scope) [in
mathcomp.field.fieldext]
+
_ :&: _ (aspace_scope) [in
mathcomp.field.fieldext]
+
<< _ ; _ >> (aspace_scope) [in
mathcomp.field.falgebra]
+
<< _ & _ >> (aspace_scope) [in
mathcomp.field.falgebra]
+
<< _ >> (aspace_scope) [in
mathcomp.field.falgebra]
+
'Z ( _ ) (aspace_scope) [in
mathcomp.field.falgebra]
+
'C ( _ ) (aspace_scope) [in
mathcomp.field.falgebra]
+
'C [ _ ] (aspace_scope) [in
mathcomp.field.falgebra]
+
{ : _ } (aspace_scope) [in
mathcomp.field.falgebra]
+
1 (aspace_scope) [in
mathcomp.field.falgebra]
+
\big [ _ / _ ]_ ( _ in _ ) _ (big_scope) [in
mathcomp.ssreflect.bigop]
+
\big [ _ / _ ]_ ( _ in _ | _ ) _ (big_scope) [in
mathcomp.ssreflect.bigop]
+
\big [ _ / _ ]_ ( _ < _ ) _ (big_scope) [in
mathcomp.ssreflect.bigop]
+
\big [ _ / _ ]_ ( _ < _ | _ ) _ (big_scope) [in
mathcomp.ssreflect.bigop]
+
\big [ _ / _ ]_ ( _ : _ ) _ (big_scope) [in
mathcomp.ssreflect.bigop]
+
\big [ _ / _ ]_ ( _ : _ | _ ) _ (big_scope) [in
mathcomp.ssreflect.bigop]
+
\big [ _ / _ ]_ _ _ (big_scope) [in
mathcomp.ssreflect.bigop]
+
\big [ _ / _ ]_ ( _ | _ ) _ (big_scope) [in
mathcomp.ssreflect.bigop]
+
\big [ _ / _ ]_ ( _ <= _ < _ ) _ (big_scope) [in
mathcomp.ssreflect.bigop]
+
\big [ _ / _ ]_ ( _ <= _ < _ | _ ) _ (big_scope) [in
mathcomp.ssreflect.bigop]
+
\big [ _ / _ ]_ ( _ <- _ ) _ (big_scope) [in
mathcomp.ssreflect.bigop]
+
\big [ _ / _ ]_ ( _ <- _ | _ ) _ (big_scope) [in
mathcomp.ssreflect.bigop]
+
_ \proper _ (bool_scope) [in
mathcomp.ssreflect.fintype]
+
_ \subset _ (bool_scope) [in
mathcomp.ssreflect.fintype]
+
[ disjoint _ & _ ] (bool_scope) [in
mathcomp.ssreflect.fintype]
+
_ != _ :> _ (bool_scope) [in
mathcomp.ssreflect.eqtype]
+
_ != _ (bool_scope) [in
mathcomp.ssreflect.eqtype]
+
_ == _ :> _ (bool_scope) [in
mathcomp.ssreflect.eqtype]
+
_ == _ (bool_scope) [in
mathcomp.ssreflect.eqtype]
+
'Z ( _ ) (cfun_scope) [in
mathcomp.character.character]
+
'o ( _ ) (cfun_scope) [in
mathcomp.character.character]
+
_ .[ _ ] (cfun_scope) [in
mathcomp.character.character]
+
_ ^: _ (cfun_scope) [in
mathcomp.character.inertia]
+
_ ^ _ (cfun_scope) [in
mathcomp.character.inertia]
+
_ %% _ (cfun_scope) [in
mathcomp.character.classfun]
+
_ / _ (cfun_scope) [in
mathcomp.character.classfun]
+
#[ _ ] (cfun_scope) [in
mathcomp.character.classfun]
+
_ ^* (cfun_scope) [in
mathcomp.character.classfun]
+
1 (cfun_scope) [in
mathcomp.character.classfun]
+
_ > _ (coq_nat_scope) [in
mathcomp.ssreflect.ssrnat]
+
_ >= _ (coq_nat_scope) [in
mathcomp.ssreflect.ssrnat]
+
_ < _ (coq_nat_scope) [in
mathcomp.ssreflect.ssrnat]
+
_ <= _ (coq_nat_scope) [in
mathcomp.ssreflect.ssrnat]
+
_ * _ (coq_nat_scope) [in
mathcomp.ssreflect.ssrnat]
+
_ - _ (coq_nat_scope) [in
mathcomp.ssreflect.ssrnat]
+
_ + _ (coq_nat_scope) [in
mathcomp.ssreflect.ssrnat]
+
#[ _ ] (C_scope) [in
mathcomp.field.algnum]
+
_ - _ (distn_scope) [in
mathcomp.algebra.ssrint]
+
_ =P _ :> _ (eq_scope) [in
mathcomp.ssreflect.eqtype]
+
_ =P _ (eq_scope) [in
mathcomp.ssreflect.eqtype]
+
[ transitive ^ _ _ , on _ | _ ] (form_scope) [in
mathcomp.solvable.primitive_action]
+
[ primitive _ , on _ | _ ] (form_scope) [in
mathcomp.solvable.primitive_action]
+
[ unitRingQuotType _ & _ of _ ] (form_scope) [in
mathcomp.algebra.ring_quotient]
+
[ ringQuotType _ & _ of _ ] (form_scope) [in
mathcomp.algebra.ring_quotient]
+
[ zmodQuotType _ , _ & _ of _ ] (form_scope) [in
mathcomp.algebra.ring_quotient]
+
[ equiv_rel of _ ] (form_scope) [in
mathcomp.ssreflect.generic_quotient]
+
[ finMixin of _ by <:%/ ] (form_scope) [in
mathcomp.ssreflect.generic_quotient]
+
[ countMixin of _ by <:%/ ] (form_scope) [in
mathcomp.ssreflect.generic_quotient]
+
[ choiceMixin of _ by <:%/ ] (form_scope) [in
mathcomp.ssreflect.generic_quotient]
+
[ eqMixin of _ by <:%/ ] (form_scope) [in
mathcomp.ssreflect.generic_quotient]
+
[ subType _ of _ by %/ ] (form_scope) [in
mathcomp.ssreflect.generic_quotient]
+
[ eqQuotType _ of _ ] (form_scope) [in
mathcomp.ssreflect.generic_quotient]
+
[ quotType of _ ] (form_scope) [in
mathcomp.ssreflect.generic_quotient]
+
[ tuple _ | _ < _ ] (form_scope) [in
mathcomp.ssreflect.tuple]
+
[ tuple ] (form_scope) [in
mathcomp.ssreflect.tuple]
+
[ tuple _ ; .. ; _ ] (form_scope) [in
mathcomp.ssreflect.tuple]
+
[ tnth _ _ ] (form_scope) [in
mathcomp.ssreflect.tuple]
+
[ tuple of _ ] (form_scope) [in
mathcomp.ssreflect.tuple]
+
{ tuple _ of _ } (form_scope) [in
mathcomp.ssreflect.tuple]
+
[ subCountType of _ ] (form_scope) [in
mathcomp.ssreflect.choice]
+
[ countMixin of _ by <: ] (form_scope) [in
mathcomp.ssreflect.choice]
+
[ choiceMixin of _ by <: ] (form_scope) [in
mathcomp.ssreflect.choice]
+
[ finMixin of _ by <: ] (form_scope) [in
mathcomp.ssreflect.fintype]
+
[ subFinType of _ ] (form_scope) [in
mathcomp.ssreflect.fintype]
+
[ arg max_ ( _ > _ ) _ ] (form_scope) [in
mathcomp.ssreflect.fintype]
+
[ arg max_ ( _ > _ in _ ) _ ] (form_scope) [in
mathcomp.ssreflect.fintype]
+
[ arg max_ ( _ > _ | _ ) _ ] (form_scope) [in
mathcomp.ssreflect.fintype]
+
[ arg min_ ( _ < _ ) _ ] (form_scope) [in
mathcomp.ssreflect.fintype]
+
[ arg min_ ( _ < _ in _ ) _ ] (form_scope) [in
mathcomp.ssreflect.fintype]
+
[ arg min_ ( _ < _ | _ ) _ ] (form_scope) [in
mathcomp.ssreflect.fintype]
+
[ pick _ : _ in _ | _ & _ ] (form_scope) [in
mathcomp.ssreflect.fintype]
+
[ pick _ in _ | _ & _ ] (form_scope) [in
mathcomp.ssreflect.fintype]
+
[ pick _ : _ in _ | _ ] (form_scope) [in
mathcomp.ssreflect.fintype]
+
[ pick _ in _ | _ ] (form_scope) [in
mathcomp.ssreflect.fintype]
+
[ pick _ : _ in _ ] (form_scope) [in
mathcomp.ssreflect.fintype]
+
[ pick _ in _ ] (form_scope) [in
mathcomp.ssreflect.fintype]
+
[ pick _ : _ | _ & _ ] (form_scope) [in
mathcomp.ssreflect.fintype]
+
[ pick _ | _ & _ ] (form_scope) [in
mathcomp.ssreflect.fintype]
+
[ pic k _ : _ ] (form_scope) [in
mathcomp.ssreflect.fintype]
+
[ pick _ ] (form_scope) [in
mathcomp.ssreflect.fintype]
+
[ pick _ : _ | _ ] (form_scope) [in
mathcomp.ssreflect.fintype]
+
[ pick _ | _ ] (form_scope) [in
mathcomp.ssreflect.fintype]
+
{ acts _ , on group _ | _ } (form_scope) [in
mathcomp.fingroup.action]
+
[ groupAction of _ ] (form_scope) [in
mathcomp.fingroup.action]
+
[ faithful _ , on _ | _ ] (form_scope) [in
mathcomp.fingroup.action]
+
[ transitive _ , on _ | _ ] (form_scope) [in
mathcomp.fingroup.action]
+
{ acts _ , on _ | _ } (form_scope) [in
mathcomp.fingroup.action]
+
[ acts _ , on _ | _ ] (form_scope) [in
mathcomp.fingroup.action]
+
[ action of _ ] (form_scope) [in
mathcomp.fingroup.action]
+
[ eqMixin of _ by <: ] (form_scope) [in
mathcomp.ssreflect.eqtype]
+
[ newType for _ by _ ] (form_scope) [in
mathcomp.ssreflect.eqtype]
+
[ new Type for _ ] (form_scope) [in
mathcomp.ssreflect.eqtype]
+
[ newType for _ ] (form_scope) [in
mathcomp.ssreflect.eqtype]
+
[ subType of _ ] (form_scope) [in
mathcomp.ssreflect.eqtype]
+
[ subType of _ for _ ] (form_scope) [in
mathcomp.ssreflect.eqtype]
+
[ subType for _ by _ ] (form_scope) [in
mathcomp.ssreflect.eqtype]
+
[ sub Type for _ ] (form_scope) [in
mathcomp.ssreflect.eqtype]
+
[ subType for _ ] (form_scope) [in
mathcomp.ssreflect.eqtype]
+
[ morphism of _ ] (form_scope) [in
mathcomp.fingroup.morphism]
+
[ morphism _ of _ ] (form_scope) [in
mathcomp.fingroup.morphism]
+
[ group of _ ] (form_scope) [in
mathcomp.fingroup.fingroup]
+
[ aspace of _ for _ ] (form_scope) [in
mathcomp.field.falgebra]
+
[ aspace of _ ] (form_scope) [in
mathcomp.field.falgebra]
+
_ ^* (fun_scope) [in
mathcomp.fingroup.action]
+
_ .-support (fun_scope) [in
mathcomp.ssreflect.finfun]
+
[ ffun => _ ] (fun_scope) [in
mathcomp.ssreflect.finfun]
+
[ ffun _ => _ ] (fun_scope) [in
mathcomp.ssreflect.finfun]
+
[ ffun : _ => _ ] (fun_scope) [in
mathcomp.ssreflect.finfun]
+
[ ffun _ : _ => _ ] (fun_scope) [in
mathcomp.ssreflect.finfun]
+
[ predX _ & _ ] (fun_scope) [in
mathcomp.ssreflect.eqtype]
+
[ eta _ with _ , .. , _ ] (fun_scope) [in
mathcomp.ssreflect.eqtype]
+
[ fun _ => _ with _ , .. , _ ] (fun_scope) [in
mathcomp.ssreflect.eqtype]
+
[ fun _ : _ => _ with _ , .. , _ ] (fun_scope) [in
mathcomp.ssreflect.eqtype]
+
_ |-> _ (fun_delta_scope) [in
mathcomp.ssreflect.eqtype]
+
[ predD1 _ & _ ] (fun_scope) [in
mathcomp.ssreflect.eqtype]
+
[ predU1 _ & _ ] (fun_scope) [in
mathcomp.ssreflect.eqtype]
+
_ %% _ (gFun_scope) [in
mathcomp.solvable.gfunctor]
+
_ \o _ (gFun_scope) [in
mathcomp.solvable.gfunctor]
+
'U (groupAction_scope) [in
mathcomp.algebra.finalg]
+
[ Aut _ ] (groupAction_scope) [in
mathcomp.fingroup.action]
+
'Q (groupAction_scope) [in
mathcomp.fingroup.action]
+
'J (groupAction_scope) [in
mathcomp.fingroup.action]
+
_ \o _ (groupAction_scope) [in
mathcomp.fingroup.action]
+
_ %% _ (groupAction_scope) [in
mathcomp.fingroup.action]
+
_ / _ (groupAction_scope) [in
mathcomp.fingroup.action]
+
<[ _ ] > (groupAction_scope) [in
mathcomp.fingroup.action]
+
_ \ _ (groupAction_scope) [in
mathcomp.fingroup.action]
+
'Zm (groupAction_scope) [in
mathcomp.character.mxabelem]
+
'MR _ (groupAction_scope) [in
mathcomp.character.mxabelem]
+
'Gal ( _ / _ ) (Group_scope) [in
mathcomp.field.galois]
+
'Gal ( _ / _ ) (group_scope) [in
mathcomp.field.galois]
+
'Alt_ _ (Group_scope) [in
mathcomp.solvable.alt]
+
'Alt_ _ (group_scope) [in
mathcomp.solvable.alt]
+
'Sym_ _ (Group_scope) [in
mathcomp.solvable.alt]
+
'Sym_ _ (group_scope) [in
mathcomp.solvable.alt]
+
'O_{ _ , .. , _ } ( _ ) (Group_scope) [in
mathcomp.solvable.pgroup]
+
'O_{ _ , .. , _ } ( _ ) (group_scope) [in
mathcomp.solvable.pgroup]
+
'O_ _ ( _ ) (Group_scope) [in
mathcomp.solvable.pgroup]
+
'O_ _ ( _ ) (group_scope) [in
mathcomp.solvable.pgroup]
+
'Syl_ _ ( _ ) (group_scope) [in
mathcomp.solvable.pgroup]
+
_ .-Sylow ( _ ) (group_scope) [in
mathcomp.solvable.pgroup]
+
_ .-Hall ( _ ) (group_scope) [in
mathcomp.solvable.pgroup]
+
_ .`_ _ (group_scope) [in
mathcomp.solvable.pgroup]
+
_ .-elt (group_scope) [in
mathcomp.solvable.pgroup]
+
_ .-subgroup ( _ ) (group_scope) [in
mathcomp.solvable.pgroup]
+
_ .-group (group_scope) [in
mathcomp.solvable.pgroup]
+
_ / _ (Group_scope) [in
mathcomp.fingroup.quotient]
+
_ / _ (group_scope) [in
mathcomp.fingroup.quotient]
+
[ Frobenius _ = _ ><| _ ] (group_scope) [in
mathcomp.solvable.frobenius]
+
[ Frobenius _ ] (group_scope) [in
mathcomp.solvable.frobenius]
+
[ Frobenius _ with kernel _ ] (group_scope) [in
mathcomp.solvable.frobenius]
+
[ Frobenius _ with complement _ ] (group_scope) [in
mathcomp.solvable.frobenius]
+
'Z[ _ ] (group_scope) [in
mathcomp.character.vcharacter]
+
'Z[ _ , _ ] (group_scope) [in
mathcomp.character.vcharacter]
+
'e_ _ (group_ring_scope) [in
mathcomp.character.mxrepresentation]
+
'R_ _ (group_ring_scope) [in
mathcomp.character.mxrepresentation]
+
'n_ _ (group_ring_scope) [in
mathcomp.character.mxrepresentation]
+
[ splits _ , over _ ] (group_scope) [in
mathcomp.fingroup.gproduct]
+
[ complements to _ in _ ] (group_scope) [in
mathcomp.fingroup.gproduct]
+
'D^ _ * Q (Group_scope) [in
mathcomp.solvable.extraspecial]
+
'D^ _ * Q (group_scope) [in
mathcomp.solvable.extraspecial]
+
'D^ _ (Group_scope) [in
mathcomp.solvable.extraspecial]
+
'D^ _ (group_scope) [in
mathcomp.solvable.extraspecial]
+
_ ^{1+2* _ } (Group_scope) [in
mathcomp.solvable.extraspecial]
+
_ ^{1+2* _ } (group_scope) [in
mathcomp.solvable.extraspecial]
+
_ ^{1+2} (Group_scope) [in
mathcomp.solvable.extraspecial]
+
_ ^{1+2} (group_scope) [in
mathcomp.solvable.extraspecial]
+
'GL_ _ ( _ ) (Group_scope) [in
mathcomp.algebra.matrix]
+
'GL_ _ [ _ ] (Group_scope) [in
mathcomp.algebra.matrix]
+
'GL_ _ ( _ ) (group_scope) [in
mathcomp.algebra.matrix]
+
'GL_ _ [ _ ] (group_scope) [in
mathcomp.algebra.matrix]
+
_ \char _ (group_scope) [in
mathcomp.fingroup.automorphism]
+
[ Aut _ ] (group_scope) [in
mathcomp.fingroup.automorphism]
+
[ Aut _ ] (Group_scope) [in
mathcomp.fingroup.automorphism]
+
'Q_ _ (Group_scope) [in
mathcomp.solvable.extremal]
+
'Q_ _ (group_scope) [in
mathcomp.solvable.extremal]
+
'SD_ _ (Group_scope) [in
mathcomp.solvable.extremal]
+
'SD_ _ (group_scope) [in
mathcomp.solvable.extremal]
+
'D_ _ (Group_scope) [in
mathcomp.solvable.extremal]
+
'D_ _ (group_scope) [in
mathcomp.solvable.extremal]
+
'Mod_ _ (Group_scope) [in
mathcomp.solvable.extremal]
+
'Mod_ _ (group_scope) [in
mathcomp.solvable.extremal]
+
'I_ _ [ _ ] (Group_scope) [in
mathcomp.character.inertia]
+
'I_ _ [ _ ] (group_scope) [in
mathcomp.character.inertia]
+
'I[ _ ] (Group_scope) [in
mathcomp.character.inertia]
+
'I[ _ ] (group_scope) [in
mathcomp.character.inertia]
+
'Mho^ _ ( _ ) (Group_scope) [in
mathcomp.solvable.abelian]
+
'Mho^ _ ( _ ) (group_scope) [in
mathcomp.solvable.abelian]
+
'Ohm_ _ ( _ ) (Group_scope) [in
mathcomp.solvable.abelian]
+
'Ohm_ _ ( _ ) (group_scope) [in
mathcomp.solvable.abelian]
+
'r_ _ ( _ ) (group_scope) [in
mathcomp.solvable.abelian]
+
'r ( _ ) (group_scope) [in
mathcomp.solvable.abelian]
+
'm ( _ ) (group_scope) [in
mathcomp.solvable.abelian]
+
'E*_ _ ( _ ) (group_scope) [in
mathcomp.solvable.abelian]
+
'E ^ _ ( _ ) (group_scope) [in
mathcomp.solvable.abelian]
+
'E_ _ ^ _ ( _ ) (group_scope) [in
mathcomp.solvable.abelian]
+
'E_ _ ( _ ) (group_scope) [in
mathcomp.solvable.abelian]
+
_ .-abelem (group_scope) [in
mathcomp.solvable.abelian]
+
'Ldiv_ _ ( _ ) (group_scope) [in
mathcomp.solvable.abelian]
+
'Ldiv_ _ (group_scope) [in
mathcomp.solvable.abelian]
+
_ \isog Grp ( _ : _ ) (group_scope) [in
mathcomp.fingroup.presentation]
+
_ \homg Grp ( _ : _ ) (group_scope) [in
mathcomp.fingroup.presentation]
+
_ \isog Grp _ (group_scope) [in
mathcomp.fingroup.presentation]
+
_ \homg Grp _ (group_scope) [in
mathcomp.fingroup.presentation]
+
_ : _ (group_presentation) [in
mathcomp.fingroup.presentation]
+
( _ , _ , .. , _ ) (group_presentation) [in
mathcomp.fingroup.presentation]
+
_ = _ = _ (group_presentation) [in
mathcomp.fingroup.presentation]
+
_ = _ (group_presentation) [in
mathcomp.fingroup.presentation]
+
[ ~ _ , _ , .. , _ ] (group_presentation) [in
mathcomp.fingroup.presentation]
+
_ ^- _ (group_presentation) [in
mathcomp.fingroup.presentation]
+
_ ^-1 (group_presentation) [in
mathcomp.fingroup.presentation]
+
_ ^ _ (group_presentation) [in
mathcomp.fingroup.presentation]
+
_ ^+ _ (group_presentation) [in
mathcomp.fingroup.presentation]
+
_ * _ (group_presentation) [in
mathcomp.fingroup.presentation]
+
1 (group_presentation) [in
mathcomp.fingroup.presentation]
+
_ .-series (group_scope) [in
mathcomp.solvable.gseries]
+
_ .-chief (group_rel_scope) [in
mathcomp.solvable.gseries]
+
_ .-central (group_rel_scope) [in
mathcomp.solvable.gseries]
+
_ .-stable (group_rel_scope) [in
mathcomp.solvable.gseries]
+
_ .-invariant (group_rel_scope) [in
mathcomp.solvable.gseries]
+
_ <|<| _ (group_scope) [in
mathcomp.solvable.gseries]
+
'SCN_ _ ( _ ) (group_scope) [in
mathcomp.solvable.maximal]
+
'SCN ( _ ) (group_scope) [in
mathcomp.solvable.maximal]
+
'F ( _ ) (Group_scope) [in
mathcomp.solvable.maximal]
+
'F ( _ ) (group_scope) [in
mathcomp.solvable.maximal]
+
'Phi ( _ ) (Group_scope) [in
mathcomp.solvable.maximal]
+
'Phi ( _ ) (group_scope) [in
mathcomp.solvable.maximal]
+
'C_ ( _ | _ ) [ _ ] (Group_scope) [in
mathcomp.fingroup.action]
+
'C_ ( | _ ) [ _ ] (Group_scope) [in
mathcomp.fingroup.action]
+
'C_ ( _ | _ ) ( _ ) (Group_scope) [in
mathcomp.fingroup.action]
+
'C_ ( | _ ) ( _ ) (Group_scope) [in
mathcomp.fingroup.action]
+
'C_ ( _ | _ ) [ _ ] (group_scope) [in
mathcomp.fingroup.action]
+
'C_ ( | _ ) [ _ ] (group_scope) [in
mathcomp.fingroup.action]
+
'C_ ( _ | _ ) ( _ ) (group_scope) [in
mathcomp.fingroup.action]
+
'C_ ( | _ ) ( _ ) (group_scope) [in
mathcomp.fingroup.action]
+
'N_ _ ( _ | _ ) (Group_scope) [in
mathcomp.fingroup.action]
+
'N ( _ | _ ) (Group_scope) [in
mathcomp.fingroup.action]
+
'C_ ( _ ) [ _ | _ ] (Group_scope) [in
mathcomp.fingroup.action]
+
'C_ _ [ _ | _ ] (Group_scope) [in
mathcomp.fingroup.action]
+
'C [ _ | _ ] (Group_scope) [in
mathcomp.fingroup.action]
+
'C_ ( _ ) ( _ | _ ) (Group_scope) [in
mathcomp.fingroup.action]
+
'C_ _ ( _ | _ ) (Group_scope) [in
mathcomp.fingroup.action]
+
'C ( _ | _ ) (Group_scope) [in
mathcomp.fingroup.action]
+
'N_ _ ( _ | _ ) (group_scope) [in
mathcomp.fingroup.action]
+
'N ( _ | _ ) (group_scope) [in
mathcomp.fingroup.action]
+
'C_ ( _ ) [ _ | _ ] (group_scope) [in
mathcomp.fingroup.action]
+
'C_ _ [ _ | _ ] (group_scope) [in
mathcomp.fingroup.action]
+
'C [ _ | _ ] (group_scope) [in
mathcomp.fingroup.action]
+
'C_ ( _ ) ( _ | _ ) (group_scope) [in
mathcomp.fingroup.action]
+
'C_ _ ( _ | _ ) (group_scope) [in
mathcomp.fingroup.action]
+
'C ( _ | _ ) (group_scope) [in
mathcomp.fingroup.action]
+
'Fix_ ( _ | _ ) [ _ ] (group_scope) [in
mathcomp.fingroup.action]
+
'Fix_ _ [ _ ] (group_scope) [in
mathcomp.fingroup.action]
+
'Fix_ ( _ | _ ) ( _ ) (group_scope) [in
mathcomp.fingroup.action]
+
'Fix_ ( _ ) ( _ ) (group_scope) [in
mathcomp.fingroup.action]
+
'Fix_ _ ( _ ) (group_scope) [in
mathcomp.fingroup.action]
+
'Z_ _ ( _ ) (Group_scope) [in
mathcomp.solvable.nilpotent]
+
'L_ _ ( _ ) (Group_scope) [in
mathcomp.solvable.nilpotent]
+
'Z_ _ ( _ ) (group_scope) [in
mathcomp.solvable.nilpotent]
+
'L_ _ ( _ ) (group_scope) [in
mathcomp.solvable.nilpotent]
+
_ ^` ( _ ) (Group_scope) [in
mathcomp.solvable.commutator]
+
_ ^` ( _ ) (group_scope) [in
mathcomp.solvable.commutator]
+
_ \homg _ (group_scope) [in
mathcomp.fingroup.morphism]
+
_ @: _ (Group_scope) [in
mathcomp.fingroup.morphism]
+
_ @*^-1 _ (Group_scope) [in
mathcomp.fingroup.morphism]
+
_ @* _ (Group_scope) [in
mathcomp.fingroup.morphism]
+
'ker_ _ _ (Group_scope) [in
mathcomp.fingroup.morphism]
+
'ker _ (Group_scope) [in
mathcomp.fingroup.morphism]
+
'injm _ (group_scope) [in
mathcomp.fingroup.morphism]
+
_ @*^-1 _ (group_scope) [in
mathcomp.fingroup.morphism]
+
_ @* _ (group_scope) [in
mathcomp.fingroup.morphism]
+
'ker_ _ _ (group_scope) [in
mathcomp.fingroup.morphism]
+
'ker _ (group_scope) [in
mathcomp.fingroup.morphism]
+
'dom _ (group_scope) [in
mathcomp.fingroup.morphism]
+
{ morphism _ >-> _ } (group_scope) [in
mathcomp.fingroup.morphism]
+
[ min _ | _ & _ ] (group_scope) [in
mathcomp.fingroup.fingroup]
+
[ min _ of _ | _ & _ ] (group_scope) [in
mathcomp.fingroup.fingroup]
+
[ min _ | _ ] (group_scope) [in
mathcomp.fingroup.fingroup]
+
[ min _ of _ | _ ] (group_scope) [in
mathcomp.fingroup.fingroup]
+
[ max _ | _ & _ ] (group_scope) [in
mathcomp.fingroup.fingroup]
+
[ max _ of _ | _ & _ ] (group_scope) [in
mathcomp.fingroup.fingroup]
+
[ max _ | _ ] (group_scope) [in
mathcomp.fingroup.fingroup]
+
[ max _ of _ | _ ] (group_scope) [in
mathcomp.fingroup.fingroup]
+
'C_ ( _ ) [ _ ] (Group_scope) [in
mathcomp.fingroup.fingroup]
+
'C_ _ [ _ ] (Group_scope) [in
mathcomp.fingroup.fingroup]
+
'C_ ( _ ) ( _ ) (Group_scope) [in
mathcomp.fingroup.fingroup]
+
'C_ _ ( _ ) (Group_scope) [in
mathcomp.fingroup.fingroup]
+
'N_ _ ( _ ) (Group_scope) [in
mathcomp.fingroup.fingroup]
+
'C [ _ ] (Group_scope) [in
mathcomp.fingroup.fingroup]
+
'C ( _ ) (Group_scope) [in
mathcomp.fingroup.fingroup]
+
'N ( _ ) (Group_scope) [in
mathcomp.fingroup.fingroup]
+
\prod_ ( _ in _ ) _ (Group_scope) [in
mathcomp.fingroup.fingroup]
+
\prod_ ( _ in _ | _ ) _ (Group_scope) [in
mathcomp.fingroup.fingroup]
+
\prod_ ( _ < _ ) _ (Group_scope) [in
mathcomp.fingroup.fingroup]
+
\prod_ ( _ < _ | _ ) _ (Group_scope) [in
mathcomp.fingroup.fingroup]
+
\prod_ ( _ : _ ) _ (Group_scope) [in
mathcomp.fingroup.fingroup]
+
\prod_ ( _ : _ | _ ) _ (Group_scope) [in
mathcomp.fingroup.fingroup]
+
\prod_ _ _ (Group_scope) [in
mathcomp.fingroup.fingroup]
+
\prod_ ( _ | _ ) _ (Group_scope) [in
mathcomp.fingroup.fingroup]
+
\prod_ ( _ <= _ < _ ) _ (Group_scope) [in
mathcomp.fingroup.fingroup]
+
\prod_ ( _ <= _ < _ | _ ) _ (Group_scope) [in
mathcomp.fingroup.fingroup]
+
\prod_ ( _ <- _ ) _ (Group_scope) [in
mathcomp.fingroup.fingroup]
+
\prod_ ( _ <- _ | _ ) _ (Group_scope) [in
mathcomp.fingroup.fingroup]
+
_ * _ (Group_scope) [in
mathcomp.fingroup.fingroup]
+
_ <*> _ (Group_scope) [in
mathcomp.fingroup.fingroup]
+
[ ~: _ , _ , .. , _ ] (Group_scope) [in
mathcomp.fingroup.fingroup]
+
<[ _ ] > (Group_scope) [in
mathcomp.fingroup.fingroup]
+
<< _ >> (Group_scope) [in
mathcomp.fingroup.fingroup]
+
_ :&: _ (Group_scope) [in
mathcomp.fingroup.fingroup]
+
[ subg _ ] (Group_scope) [in
mathcomp.fingroup.fingroup]
+
[ subg _ ] (group_scope) [in
mathcomp.fingroup.fingroup]
+
_ :^ _ (Group_scope) [in
mathcomp.fingroup.fingroup]
+
[ ~: _ , _ , .. , _ ] (group_scope) [in
mathcomp.fingroup.fingroup]
+
_ <*> _ (group_scope) [in
mathcomp.fingroup.fingroup]
+
#[ _ ] (group_scope) [in
mathcomp.fingroup.fingroup]
+
<[ _ ] > (group_scope) [in
mathcomp.fingroup.fingroup]
+
<< _ >> (group_scope) [in
mathcomp.fingroup.fingroup]
+
[ set : _ ] (Group_scope) [in
mathcomp.fingroup.fingroup]
+
[ 1 _ ] (Group_scope) [in
mathcomp.fingroup.fingroup]
+
1 (Group_scope) [in
mathcomp.fingroup.fingroup]
+
'C_ ( _ ) [ _ ] (group_scope) [in
mathcomp.fingroup.fingroup]
+
'C_ _ [ _ ] (group_scope) [in
mathcomp.fingroup.fingroup]
+
'C [ _ ] (group_scope) [in
mathcomp.fingroup.fingroup]
+
'C_ ( _ ) ( _ ) (group_scope) [in
mathcomp.fingroup.fingroup]
+
'C_ _ ( _ ) (group_scope) [in
mathcomp.fingroup.fingroup]
+
'C ( _ ) (group_scope) [in
mathcomp.fingroup.fingroup]
+
_ <| _ (group_scope) [in
mathcomp.fingroup.fingroup]
+
'N_ _ ( _ ) (group_scope) [in
mathcomp.fingroup.fingroup]
+
'N ( _ ) (group_scope) [in
mathcomp.fingroup.fingroup]
+
#| _ : _ | (group_scope) [in
mathcomp.fingroup.fingroup]
+
_ :^: _ (group_scope) [in
mathcomp.fingroup.fingroup]
+
_ ^: _ (group_scope) [in
mathcomp.fingroup.fingroup]
+
_ :^ _ (group_scope) [in
mathcomp.fingroup.fingroup]
+
_ :* _ (group_scope) [in
mathcomp.fingroup.fingroup]
+
_ *: _ (group_scope) [in
mathcomp.fingroup.fingroup]
+
_ ^# (group_scope) [in
mathcomp.fingroup.fingroup]
+
[ 1 ] (group_scope) [in
mathcomp.fingroup.fingroup]
+
[ 1 _ ] (group_scope) [in
mathcomp.fingroup.fingroup]
+
\prod_ ( _ in _ ) _ (group_scope) [in
mathcomp.fingroup.fingroup]
+
\prod_ ( _ in _ | _ ) _ (group_scope) [in
mathcomp.fingroup.fingroup]
+
\prod_ ( _ < _ ) _ (group_scope) [in
mathcomp.fingroup.fingroup]
+
\prod_ ( _ < _ | _ ) _ (group_scope) [in
mathcomp.fingroup.fingroup]
+
\prod_ ( _ : _ ) _ (group_scope) [in
mathcomp.fingroup.fingroup]
+
\prod_ ( _ : _ | _ ) _ (group_scope) [in
mathcomp.fingroup.fingroup]
+
\prod_ _ _ (group_scope) [in
mathcomp.fingroup.fingroup]
+
\prod_ ( _ | _ ) _ (group_scope) [in
mathcomp.fingroup.fingroup]
+
\prod_ ( _ <= _ < _ ) _ (group_scope) [in
mathcomp.fingroup.fingroup]
+
\prod_ ( _ <= _ < _ | _ ) _ (group_scope) [in
mathcomp.fingroup.fingroup]
+
\prod_ ( _ <- _ ) _ (group_scope) [in
mathcomp.fingroup.fingroup]
+
\prod_ ( _ <- _ | _ ) _ (group_scope) [in
mathcomp.fingroup.fingroup]
+
[ ~ _ , _ , .. , _ ] (group_scope) [in
mathcomp.fingroup.fingroup]
+
_ ^ _ (group_scope) [in
mathcomp.fingroup.fingroup]
+
_ ^- _ (group_scope) [in
mathcomp.fingroup.fingroup]
+
_ ^+ _ (group_scope) [in
mathcomp.fingroup.fingroup]
+
_ ^-1 (group_scope) [in
mathcomp.fingroup.fingroup]
+
_ * _ (group_scope) [in
mathcomp.fingroup.fingroup]
+
1 (group_scope) [in
mathcomp.fingroup.fingroup]
+
'Z ( _ ) (Group_scope) [in
mathcomp.solvable.center]
+
'Z ( _ ) (group_scope) [in
mathcomp.solvable.center]
+
_ != _ %[mod _ ] (int_scope) [in
mathcomp.algebra.intdiv]
+
_ <> _ %[mod _ ] (int_scope) [in
mathcomp.algebra.intdiv]
+
_ == _ %[mod _ ] (int_scope) [in
mathcomp.algebra.intdiv]
+
_ = _ %[mod _ ] (int_scope) [in
mathcomp.algebra.intdiv]
+
_ %| _ (int_scope) [in
mathcomp.algebra.intdiv]
+
_ %% _ (int_scope) [in
mathcomp.algebra.intdiv]
+
_ %/ _ (int_scope) [in
mathcomp.algebra.intdiv]
+
_ %:Z (int_scope) [in
mathcomp.algebra.ssrint]
+
[ 1 _ ] (irrType_scope) [in
mathcomp.character.mxrepresentation]
+
_ ^-1 (lfun_scope) [in
mathcomp.algebra.vector]
+
_ \o _ (lfun_scope) [in
mathcomp.algebra.vector]
+
\1 (lfun_scope) [in
mathcomp.algebra.vector]
+
_ ^-1 (lrfun_scope) [in
mathcomp.field.galois]
+
_ \o _ (lrfun_scope) [in
mathcomp.field.falgebra]
+
\1 (lrfun_scope) [in
mathcomp.field.falgebra]
+
'Z ( _ ) (matrix_set_scope) [in
mathcomp.algebra.mxalgebra]
+
'C_ ( _ ) ( _ ) (matrix_set_scope) [in
mathcomp.algebra.mxalgebra]
+
'C_ _ ( _ ) (matrix_set_scope) [in
mathcomp.algebra.mxalgebra]
+
'C ( _ ) (matrix_set_scope) [in
mathcomp.algebra.mxalgebra]
+
_ * _ (matrix_set_scope) [in
mathcomp.algebra.mxalgebra]
+
_ \in _ (matrix_set_scope) [in
mathcomp.algebra.mxalgebra]
+
\bigcap_ ( _ in _ ) _ (matrix_set_scope) [in
mathcomp.algebra.mxalgebra]
+
\bigcap_ ( _ in _ | _ ) _ (matrix_set_scope) [in
mathcomp.algebra.mxalgebra]
+
\bigcap_ ( _ < _ ) _ (matrix_set_scope) [in
mathcomp.algebra.mxalgebra]
+
\bigcap_ ( _ < _ | _ ) _ (matrix_set_scope) [in
mathcomp.algebra.mxalgebra]
+
\bigcap_ ( _ : _ ) _ (matrix_set_scope) [in
mathcomp.algebra.mxalgebra]
+
\bigcap_ ( _ : _ | _ ) _ (matrix_set_scope) [in
mathcomp.algebra.mxalgebra]
+
\bigcap_ _ _ (matrix_set_scope) [in
mathcomp.algebra.mxalgebra]
+
\bigcap_ ( _ | _ ) _ (matrix_set_scope) [in
mathcomp.algebra.mxalgebra]
+
\bigcap_ ( _ <= _ < _ ) _ (matrix_set_scope) [in
mathcomp.algebra.mxalgebra]
+
\bigcap_ ( _ <= _ < _ | _ ) _ (matrix_set_scope) [in
mathcomp.algebra.mxalgebra]
+
\bigcap_ ( _ <- _ ) _ (matrix_set_scope) [in
mathcomp.algebra.mxalgebra]
+
\bigcap_ ( _ <- _ | _ ) _ (matrix_set_scope) [in
mathcomp.algebra.mxalgebra]
+
\sum_ ( _ in _ ) _ (matrix_set_scope) [in
mathcomp.algebra.mxalgebra]
+
\sum_ ( _ in _ | _ ) _ (matrix_set_scope) [in
mathcomp.algebra.mxalgebra]
+
\sum_ ( _ < _ ) _ (matrix_set_scope) [in
mathcomp.algebra.mxalgebra]
+
\sum_ ( _ < _ | _ ) _ (matrix_set_scope) [in
mathcomp.algebra.mxalgebra]
+
\sum_ ( _ : _ ) _ (matrix_set_scope) [in
mathcomp.algebra.mxalgebra]
+
\sum_ ( _ : _ | _ ) _ (matrix_set_scope) [in
mathcomp.algebra.mxalgebra]
+
\sum_ _ _ (matrix_set_scope) [in
mathcomp.algebra.mxalgebra]
+
\sum_ ( _ | _ ) _ (matrix_set_scope) [in
mathcomp.algebra.mxalgebra]
+
\sum_ ( _ <= _ < _ ) _ (matrix_set_scope) [in
mathcomp.algebra.mxalgebra]
+
\sum_ ( _ <= _ < _ | _ ) _ (matrix_set_scope) [in
mathcomp.algebra.mxalgebra]
+
\sum_ ( _ <- _ ) _ (matrix_set_scope) [in
mathcomp.algebra.mxalgebra]
+
\sum_ ( _ <- _ | _ ) _ (matrix_set_scope) [in
mathcomp.algebra.mxalgebra]
+
_ :\: _ (matrix_set_scope) [in
mathcomp.algebra.mxalgebra]
+
_ :&: _ (matrix_set_scope) [in
mathcomp.algebra.mxalgebra]
+
_ + _ (matrix_set_scope) [in
mathcomp.algebra.mxalgebra]
+
_ :=: _ (matrix_set_scope) [in
mathcomp.algebra.mxalgebra]
+
_ == _ (matrix_set_scope) [in
mathcomp.algebra.mxalgebra]
+
_ < _ < _ (matrix_set_scope) [in
mathcomp.algebra.mxalgebra]
+
_ <= _ < _ (matrix_set_scope) [in
mathcomp.algebra.mxalgebra]
+
_ < _ <= _ (matrix_set_scope) [in
mathcomp.algebra.mxalgebra]
+
_ <= _ <= _ (matrix_set_scope) [in
mathcomp.algebra.mxalgebra]
+
_ < _ (matrix_set_scope) [in
mathcomp.algebra.mxalgebra]
+
_ <= _ (matrix_set_scope) [in
mathcomp.algebra.mxalgebra]
+
_ ^C (matrix_set_scope) [in
mathcomp.algebra.mxalgebra]
+
<< _ >> (matrix_set_scope) [in
mathcomp.algebra.mxalgebra]
+
'C ( _ , _ ) (nat_scope) [in
mathcomp.ssreflect.binomial]
+
_ ^_ _ (nat_scope) [in
mathcomp.ssreflect.binomial]
+
_ `_ _ (nat_scope) [in
mathcomp.ssreflect.prime]
+
_ .-nat (nat_scope) [in
mathcomp.ssreflect.prime]
+
_ ^' (nat_scope) [in
mathcomp.ssreflect.prime]
+
\p i ( _ ) (nat_scope) [in
mathcomp.ssreflect.prime]
+
\pi ( _ ) (nat_scope) [in
mathcomp.ssreflect.prime]
+
_ ^? _ :: _ (nat_scope) [in
mathcomp.ssreflect.prime]
+
_ %| _ (nat_scope) [in
mathcomp.ssreflect.div]
+
_ != _ %[mod _ ] (nat_scope) [in
mathcomp.ssreflect.div]
+
_ <> _ %[mod _ ] (nat_scope) [in
mathcomp.ssreflect.div]
+
_ == _ %[mod _ ] (nat_scope) [in
mathcomp.ssreflect.div]
+
_ = _ %[mod _ ] (nat_scope) [in
mathcomp.ssreflect.div]
+
_ %% _ (nat_scope) [in
mathcomp.ssreflect.div]
+
_ %/ _ (nat_scope) [in
mathcomp.ssreflect.div]
+
\dim _ (nat_scope) [in
mathcomp.algebra.vector]
+
#| _ | (nat_scope) [in
mathcomp.ssreflect.fintype]
+
[ Num of _ ] (nat_scope) [in
mathcomp.ssreflect.ssrnat]
+
_ <= _ ?= iff _ (nat_scope) [in
mathcomp.ssreflect.ssrnat]
+
_ ./2 (nat_scope) [in
mathcomp.ssreflect.ssrnat]
+
_ .*2 (nat_scope) [in
mathcomp.ssreflect.ssrnat]
+
_ .*2 (nat_rec_scope) [in
mathcomp.ssreflect.ssrnat]
+
_ `! (nat_scope) [in
mathcomp.ssreflect.ssrnat]
+
_ ^ _ (nat_scope) [in
mathcomp.ssreflect.ssrnat]
+
_ ^ _ (nat_rec_scope) [in
mathcomp.ssreflect.ssrnat]
+
_ * _ (nat_scope) [in
mathcomp.ssreflect.ssrnat]
+
_ * _ (nat_rec_scope) [in
mathcomp.ssreflect.ssrnat]
+
_ < _ < _ (nat_scope) [in
mathcomp.ssreflect.ssrnat]
+
_ <= _ < _ (nat_scope) [in
mathcomp.ssreflect.ssrnat]
+
_ < _ <= _ (nat_scope) [in
mathcomp.ssreflect.ssrnat]
+
_ <= _ <= _ (nat_scope) [in
mathcomp.ssreflect.ssrnat]
+
_ > _ (nat_scope) [in
mathcomp.ssreflect.ssrnat]
+
_ >= _ (nat_scope) [in
mathcomp.ssreflect.ssrnat]
+
_ < _ (nat_scope) [in
mathcomp.ssreflect.ssrnat]
+
_ <= _ (nat_scope) [in
mathcomp.ssreflect.ssrnat]
+
_ - _ (nat_scope) [in
mathcomp.ssreflect.ssrnat]
+
_ - _ (nat_rec_scope) [in
mathcomp.ssreflect.ssrnat]
+
_ + _ (nat_scope) [in
mathcomp.ssreflect.ssrnat]
+
_ + _ (nat_rec_scope) [in
mathcomp.ssreflect.ssrnat]
+
_ .-2 (nat_scope) [in
mathcomp.ssreflect.ssrnat]
+
_ .-1 (nat_scope) [in
mathcomp.ssreflect.ssrnat]
+
_ .+4 (nat_scope) [in
mathcomp.ssreflect.ssrnat]
+
_ .+3 (nat_scope) [in
mathcomp.ssreflect.ssrnat]
+
_ .+2 (nat_scope) [in
mathcomp.ssreflect.ssrnat]
+
_ .+1 (nat_scope) [in
mathcomp.ssreflect.ssrnat]
+
\max_ ( _ in _ ) _ (nat_scope) [in
mathcomp.ssreflect.bigop]
+
\max_ ( _ in _ | _ ) _ (nat_scope) [in
mathcomp.ssreflect.bigop]
+
\max_ ( _ < _ ) _ (nat_scope) [in
mathcomp.ssreflect.bigop]
+
\max_ ( _ < _ | _ ) _ (nat_scope) [in
mathcomp.ssreflect.bigop]
+
\max_ ( _ <= _ < _ ) _ (nat_scope) [in
mathcomp.ssreflect.bigop]
+
\max_ ( _ <= _ < _ | _ ) _ (nat_scope) [in
mathcomp.ssreflect.bigop]
+
\max_ ( _ : _ ) _ (nat_scope) [in
mathcomp.ssreflect.bigop]
+
\max_ ( _ : _ | _ ) _ (nat_scope) [in
mathcomp.ssreflect.bigop]
+
\max_ _ _ (nat_scope) [in
mathcomp.ssreflect.bigop]
+
\max_ ( _ | _ ) _ (nat_scope) [in
mathcomp.ssreflect.bigop]
+
\max_ ( _ <- _ ) _ (nat_scope) [in
mathcomp.ssreflect.bigop]
+
\max_ ( _ <- _ | _ ) _ (nat_scope) [in
mathcomp.ssreflect.bigop]
+
\prod_ ( _ in _ ) _ (nat_scope) [in
mathcomp.ssreflect.bigop]
+
\prod_ ( _ in _ | _ ) _ (nat_scope) [in
mathcomp.ssreflect.bigop]
+
\prod_ ( _ < _ ) _ (nat_scope) [in
mathcomp.ssreflect.bigop]
+
\prod_ ( _ < _ | _ ) _ (nat_scope) [in
mathcomp.ssreflect.bigop]
+
\prod_ ( _ : _ ) _ (nat_scope) [in
mathcomp.ssreflect.bigop]
+
\prod_ ( _ : _ | _ ) _ (nat_scope) [in
mathcomp.ssreflect.bigop]
+
\prod_ _ _ (nat_scope) [in
mathcomp.ssreflect.bigop]
+
\prod_ ( _ | _ ) _ (nat_scope) [in
mathcomp.ssreflect.bigop]
+
\prod_ ( _ <= _ < _ ) _ (nat_scope) [in
mathcomp.ssreflect.bigop]
+
\prod_ ( _ <= _ < _ | _ ) _ (nat_scope) [in
mathcomp.ssreflect.bigop]
+
\prod_ ( _ <- _ ) _ (nat_scope) [in
mathcomp.ssreflect.bigop]
+
\prod_ ( _ <- _ | _ ) _ (nat_scope) [in
mathcomp.ssreflect.bigop]
+
\sum_ ( _ in _ ) _ (nat_scope) [in
mathcomp.ssreflect.bigop]
+
\sum_ ( _ in _ | _ ) _ (nat_scope) [in
mathcomp.ssreflect.bigop]
+
\sum_ ( _ < _ ) _ (nat_scope) [in
mathcomp.ssreflect.bigop]
+
\sum_ ( _ < _ | _ ) _ (nat_scope) [in
mathcomp.ssreflect.bigop]
+
\sum_ ( _ : _ ) _ (nat_scope) [in
mathcomp.ssreflect.bigop]
+
\sum_ ( _ : _ | _ ) _ (nat_scope) [in
mathcomp.ssreflect.bigop]
+
\sum_ _ _ (nat_scope) [in
mathcomp.ssreflect.bigop]
+
\sum_ ( _ | _ ) _ (nat_scope) [in
mathcomp.ssreflect.bigop]
+
\sum_ ( _ <= _ < _ ) _ (nat_scope) [in
mathcomp.ssreflect.bigop]
+
\sum_ ( _ <= _ < _ | _ ) _ (nat_scope) [in
mathcomp.ssreflect.bigop]
+
\sum_ ( _ <- _ ) _ (nat_scope) [in
mathcomp.ssreflect.bigop]
+
\sum_ ( _ <- _ | _ ) _ (nat_scope) [in
mathcomp.ssreflect.bigop]
+
`| _ | (nat_scope) [in
mathcomp.algebra.ssrint]
+
\dim_ _ _ (nat_scope) [in
mathcomp.field.falgebra]
+
\rank _ (nat_scope) [in
mathcomp.algebra.mxalgebra]
+
_ : _ (nt_group_presentation) [in
mathcomp.fingroup.presentation]
+
_ <> _ %[mod_ideal _ ] (quotient_scope) [in
mathcomp.algebra.ring_quotient]
+
_ != _ %[mod_ideal _ ] (quotient_scope) [in
mathcomp.algebra.ring_quotient]
+
_ = _ %[mod_ideal _ ] (quotient_scope) [in
mathcomp.algebra.ring_quotient]
+
_ == _ %[mod_ideal _ ] (quotient_scope) [in
mathcomp.algebra.ring_quotient]
+
_ <> _ %[mod_eq _ ] (quotient_scope) [in
mathcomp.ssreflect.generic_quotient]
+
_ != _ %[mod_eq _ ] (quotient_scope) [in
mathcomp.ssreflect.generic_quotient]
+
_ = _ %[mod_eq _ ] (quotient_scope) [in
mathcomp.ssreflect.generic_quotient]
+
_ == _ %[mod_eq _ ] (quotient_scope) [in
mathcomp.ssreflect.generic_quotient]
+
{eq_quot _ } (quotient_scope) [in
mathcomp.ssreflect.generic_quotient]
+
{pi _ } (quotient_scope) [in
mathcomp.ssreflect.generic_quotient]
+
{pi_ _ _ } (quotient_scope) [in
mathcomp.ssreflect.generic_quotient]
+
_ <> _ %[mod _ ] (quotient_scope) [in
mathcomp.ssreflect.generic_quotient]
+
_ != _ %[mod _ ] (quotient_scope) [in
mathcomp.ssreflect.generic_quotient]
+
_ = _ %[mod _ ] (quotient_scope) [in
mathcomp.ssreflect.generic_quotient]
+
_ == _ %[mod _ ] (quotient_scope) [in
mathcomp.ssreflect.generic_quotient]
+
\pi (quotient_scope) [in
mathcomp.ssreflect.generic_quotient]
+
\pi_ _ (quotient_scope) [in
mathcomp.ssreflect.generic_quotient]
+
_ / _ (rat_scope) [in
mathcomp.algebra.rat]
+
_ - _ (rat_scope) [in
mathcomp.algebra.rat]
+
_ ^-1 (rat_scope) [in
mathcomp.algebra.rat]
+
_ * _ (rat_scope) [in
mathcomp.algebra.rat]
+
- _ (rat_scope) [in
mathcomp.algebra.rat]
+
_ + _ (rat_scope) [in
mathcomp.algebra.rat]
+
1 (rat_scope) [in
mathcomp.algebra.rat]
+
0 (rat_scope) [in
mathcomp.algebra.rat]
+
'omega_ _ [ _ ] (ring_scope) [in
mathcomp.character.integral_char]
+
'K_ _ (ring_scope) [in
mathcomp.character.integral_char]
+
_ %:Q (ring_scope) [in
mathcomp.algebra.rat]
+
\prod_ ( _ in _ ) _ (ring_scope) [in
mathcomp.algebra.ssralg]
+
\prod_ ( _ in _ | _ ) _ (ring_scope) [in
mathcomp.algebra.ssralg]
+
\prod_ ( _ < _ ) _ (ring_scope) [in
mathcomp.algebra.ssralg]
+
\prod_ ( _ < _ | _ ) _ (ring_scope) [in
mathcomp.algebra.ssralg]
+
\prod_ ( _ : _ ) _ (ring_scope) [in
mathcomp.algebra.ssralg]
+
\prod_ ( _ : _ | _ ) _ (ring_scope) [in
mathcomp.algebra.ssralg]
+
\prod_ _ _ (ring_scope) [in
mathcomp.algebra.ssralg]
+
\prod_ ( _ | _ ) _ (ring_scope) [in
mathcomp.algebra.ssralg]
+
\prod_ ( _ <= _ < _ ) _ (ring_scope) [in
mathcomp.algebra.ssralg]
+
\prod_ ( _ <= _ < _ | _ ) _ (ring_scope) [in
mathcomp.algebra.ssralg]
+
\prod_ ( _ <- _ ) _ (ring_scope) [in
mathcomp.algebra.ssralg]
+
\prod_ ( _ <- _ | _ ) _ (ring_scope) [in
mathcomp.algebra.ssralg]
+
\sum_ ( _ in _ ) _ (ring_scope) [in
mathcomp.algebra.ssralg]
+
\sum_ ( _ in _ | _ ) _ (ring_scope) [in
mathcomp.algebra.ssralg]
+
\sum_ ( _ < _ ) _ (ring_scope) [in
mathcomp.algebra.ssralg]
+
\sum_ ( _ < _ | _ ) _ (ring_scope) [in
mathcomp.algebra.ssralg]
+
\sum_ ( _ : _ ) _ (ring_scope) [in
mathcomp.algebra.ssralg]
+
\sum_ ( _ : _ | _ ) _ (ring_scope) [in
mathcomp.algebra.ssralg]
+
\sum_ _ _ (ring_scope) [in
mathcomp.algebra.ssralg]
+
\sum_ ( _ | _ ) _ (ring_scope) [in
mathcomp.algebra.ssralg]
+
\sum_ ( _ <= _ < _ ) _ (ring_scope) [in
mathcomp.algebra.ssralg]
+
\sum_ ( _ <= _ < _ | _ ) _ (ring_scope) [in
mathcomp.algebra.ssralg]
+
\sum_ ( _ <- _ ) _ (ring_scope) [in
mathcomp.algebra.ssralg]
+
\sum_ ( _ <- _ | _ ) _ (ring_scope) [in
mathcomp.algebra.ssralg]
+
_ \o* _ (ring_scope) [in
mathcomp.algebra.ssralg]
+
_ \*o _ (ring_scope) [in
mathcomp.algebra.ssralg]
+
_ \*: _ (ring_scope) [in
mathcomp.algebra.ssralg]
+
_ \- _ (ring_scope) [in
mathcomp.algebra.ssralg]
+
_ \+ _ (ring_scope) [in
mathcomp.algebra.ssralg]
+
\0 (ring_scope) [in
mathcomp.algebra.ssralg]
+
_ %:A (ring_scope) [in
mathcomp.algebra.ssralg]
+
_ *: _ (ring_scope) [in
mathcomp.algebra.ssralg]
+
_ / _ (ring_scope) [in
mathcomp.algebra.ssralg]
+
_ ^- _ (ring_scope) [in
mathcomp.algebra.ssralg]
+
_ ^-1 (ring_scope) [in
mathcomp.algebra.ssralg]
+
_ ^+ _ (ring_scope) [in
mathcomp.algebra.ssralg]
+
_ * _ (ring_scope) [in
mathcomp.algebra.ssralg]
+
[ char _ ] (ring_scope) [in
mathcomp.algebra.ssralg]
+
_ %:R (ring_scope) [in
mathcomp.algebra.ssralg]
+
- 1 (ring_scope) [in
mathcomp.algebra.ssralg]
+
1 (ring_scope) [in
mathcomp.algebra.ssralg]
+
_ `_ _ (ring_scope) [in
mathcomp.algebra.ssralg]
+
_ *- _ (ring_scope) [in
mathcomp.algebra.ssralg]
+
_ *+ _ (ring_scope) [in
mathcomp.algebra.ssralg]
+
_ - _ (ring_scope) [in
mathcomp.algebra.ssralg]
+
_ + _ (ring_scope) [in
mathcomp.algebra.ssralg]
+
- _ (ring_scope) [in
mathcomp.algebra.ssralg]
+
-%R (ring_scope) [in
mathcomp.algebra.ssralg]
+
0 (ring_scope) [in
mathcomp.algebra.ssralg]
+
_ <= _ ?< if _ (ring_scope) [in
mathcomp.algebra.interval]
+
`] -oo , +oo [ (ring_scope) [in
mathcomp.algebra.interval]
+
`] _ , +oo [ (ring_scope) [in
mathcomp.algebra.interval]
+
`[ _ , +oo [ (ring_scope) [in
mathcomp.algebra.interval]
+
`] -oo , _ [ (ring_scope) [in
mathcomp.algebra.interval]
+
`] -oo , _ ] (ring_scope) [in
mathcomp.algebra.interval]
+
`] _ , _ [ (ring_scope) [in
mathcomp.algebra.interval]
+
`[ _ , _ [ (ring_scope) [in
mathcomp.algebra.interval]
+
`] _ , _ ] (ring_scope) [in
mathcomp.algebra.interval]
+
`[ _ , _ ] (ring_scope) [in
mathcomp.algebra.interval]
+
\adj _ (ring_scope) [in
mathcomp.algebra.matrix]
+
\det _ (ring_scope) [in
mathcomp.algebra.matrix]
+
\tr _ (ring_scope) [in
mathcomp.algebra.matrix]
+
_ *m _ (ring_scope) [in
mathcomp.algebra.matrix]
+
_ %:M (ring_scope) [in
mathcomp.algebra.matrix]
+
_ ^T (ring_scope) [in
mathcomp.algebra.matrix]
+
\row_ _ _ (ring_scope) [in
mathcomp.algebra.matrix]
+
\row_ ( _ < _ ) _ (ring_scope) [in
mathcomp.algebra.matrix]
+
\col_ _ _ (ring_scope) [in
mathcomp.algebra.matrix]
+
\col_ ( _ < _ ) _ (ring_scope) [in
mathcomp.algebra.matrix]
+
\matrix_ _ _ (ring_scope) [in
mathcomp.algebra.matrix]
+
\matrix_ ( _ < _ ) _ (ring_scope) [in
mathcomp.algebra.matrix]
+
\matrix_ ( _ , _ ) _ (ring_scope) [in
mathcomp.algebra.matrix]
+
\matrix_ ( _ , _ < _ ) _ (ring_scope) [in
mathcomp.algebra.matrix]
+
\matrix_ ( _ < _ , _ < _ ) _ (ring_scope) [in
mathcomp.algebra.matrix]
+
\matrix[ _ ]_ ( _ , _ ) _ (ring_scope) [in
mathcomp.algebra.matrix]
+
_ .[ _ , _ ] (ring_scope) [in
mathcomp.algebra.polyXY]
+
_ ^:P (ring_scope) [in
mathcomp.algebra.polyXY]
+
'Y (ring_scope) [in
mathcomp.algebra.polyXY]
+
_ ^ _ (ring_scope) [in
mathcomp.algebra.polyXY]
+
'chi[ _ ]_ _ (ring_scope) [in
mathcomp.character.character]
+
'chi_ _ (ring_scope) [in
mathcomp.character.character]
+
'Ind (ring_scope) [in
mathcomp.character.classfun]
+
'Ind[ _ ] (ring_scope) [in
mathcomp.character.classfun]
+
'Ind[ _ , _ ] (ring_scope) [in
mathcomp.character.classfun]
+
'Res (ring_scope) [in
mathcomp.character.classfun]
+
'Res[ _ ] (ring_scope) [in
mathcomp.character.classfun]
+
'Res[ _ , _ ] (ring_scope) [in
mathcomp.character.classfun]
+
'CF ( _ , _ ) (ring_scope) [in
mathcomp.character.classfun]
+
'[ _ ] (ring_scope) [in
mathcomp.character.classfun]
+
'[ _ ]_ _ (ring_scope) [in
mathcomp.character.classfun]
+
'[ _ , _ ] (ring_scope) [in
mathcomp.character.classfun]
+
'[ _ , _ ]_ _ (ring_scope) [in
mathcomp.character.classfun]
+
'CF ( _ , _ ) (ring_scope) [in
mathcomp.character.classfun]
+
'1_ _ (ring_scope) [in
mathcomp.character.classfun]
+
_ \Po _ (ring_scope) [in
mathcomp.algebra.poly]
+
_ ^:P (ring_scope) [in
mathcomp.algebra.poly]
+
_ ^`N ( _ ) (ring_scope) [in
mathcomp.algebra.poly]
+
_ ^` ( _ ) (ring_scope) [in
mathcomp.algebra.poly]
+
_ ^` (ring_scope) [in
mathcomp.algebra.poly]
+
_ .-primitive_root (ring_scope) [in
mathcomp.algebra.poly]
+
_ .-unity_root (ring_scope) [in
mathcomp.algebra.poly]
+
_ .[ _ ] (ring_scope) [in
mathcomp.algebra.poly]
+
'X^ _ (ring_scope) [in
mathcomp.algebra.poly]
+
'X (ring_scope) [in
mathcomp.algebra.poly]
+
_ %:P (ring_scope) [in
mathcomp.algebra.poly]
+
\poly_ ( _ < _ ) _ (ring_scope) [in
mathcomp.algebra.poly]
+
_ ^ _ (ring_scope) [in
mathcomp.algebra.ssrint]
+
_ %:~R (ring_scope) [in
mathcomp.algebra.ssrint]
+
_ *~ _ (ring_scope) [in
mathcomp.algebra.ssrint]
+
*~%R (ring_scope) [in
mathcomp.algebra.ssrint]
+
_ <> _ :> in t (ring_scope) [in
mathcomp.algebra.ssrint]
+
_ != _ :> in t (ring_scope) [in
mathcomp.algebra.ssrint]
+
_ == _ :> in t (ring_scope) [in
mathcomp.algebra.ssrint]
+
_ = _ :> in t (ring_scope) [in
mathcomp.algebra.ssrint]
+
_ %:Z (ring_scope) [in
mathcomp.algebra.ssrint]
+
_ ^@ (ring_scope) [in
mathcomp.field.algebraics_fundamentals]
+
_ ^ _ (ring_scope) [in
mathcomp.field.algebraics_fundamentals]
+
_ / _ (section_scope) [in
mathcomp.solvable.jordanholder]
+
[ seq _ | _ : _ <- _ , _ : _ <- _ ] (seq_scope) [in
mathcomp.ssreflect.seq]
+
[ seq _ | _ <- _ , _ <- _ ] (seq_scope) [in
mathcomp.ssreflect.seq]
+
[ seq _ | _ : _ <- _ & _ ] (seq_scope) [in
mathcomp.ssreflect.seq]
+
[ seq _ | _ : _ <- _ ] (seq_scope) [in
mathcomp.ssreflect.seq]
+
[ seq _ | _ <- _ & _ ] (seq_scope) [in
mathcomp.ssreflect.seq]
+
[ seq _ | _ <- _ ] (seq_scope) [in
mathcomp.ssreflect.seq]
+
[ seq _ <- _ | _ & _ ] (seq_scope) [in
mathcomp.ssreflect.seq]
+
[ seq _ <- _ | _ ] (seq_scope) [in
mathcomp.ssreflect.seq]
+
_ ++ _ (seq_scope) [in
mathcomp.ssreflect.seq]
+
[ :: _ ; _ ; .. ; _ ] (seq_scope) [in
mathcomp.ssreflect.seq]
+
[ :: _ , _ , .. , _ & _ ] (seq_scope) [in
mathcomp.ssreflect.seq]
+
[ :: _ & _ ] (seq_scope) [in
mathcomp.ssreflect.seq]
+
[ :: _ ] (seq_scope) [in
mathcomp.ssreflect.seq]
+
[ :: ] (seq_scope) [in
mathcomp.ssreflect.seq]
+
_ :: _ (seq_scope) [in
mathcomp.ssreflect.seq]
+
[ seq _ , _ ] (seq_scope) [in
mathcomp.ssreflect.fintype]
+
[ seq _ | _ : _ ] (seq_scope) [in
mathcomp.ssreflect.fintype]
+
[ seq _ | _ : _ in _ ] (seq_scope) [in
mathcomp.ssreflect.fintype]
+
[ seq _ | _ in _ ] (seq_scope) [in
mathcomp.ssreflect.fintype]
+
_ .-dtuple ( _ ) (set_scope) [in
mathcomp.solvable.primitive_action]
+
\bigcap_ ( _ in _ ) _ (set_scope) [in
mathcomp.ssreflect.finset]
+
\bigcap_ ( _ in _ | _ ) _ (set_scope) [in
mathcomp.ssreflect.finset]
+
\bigcap_ ( _ < _ ) _ (set_scope) [in
mathcomp.ssreflect.finset]
+
\bigcap_ ( _ < _ | _ ) _ (set_scope) [in
mathcomp.ssreflect.finset]
+
\bigcap_ ( _ : _ ) _ (set_scope) [in
mathcomp.ssreflect.finset]
+
\bigcap_ ( _ : _ | _ ) _ (set_scope) [in
mathcomp.ssreflect.finset]
+
\bigcap_ _ _ (set_scope) [in
mathcomp.ssreflect.finset]
+
\bigcap_ ( _ | _ ) _ (set_scope) [in
mathcomp.ssreflect.finset]
+
\bigcap_ ( _ <= _ < _ ) _ (set_scope) [in
mathcomp.ssreflect.finset]
+
\bigcap_ ( _ <= _ < _ | _ ) _ (set_scope) [in
mathcomp.ssreflect.finset]
+
\bigcap_ ( _ <- _ ) _ (set_scope) [in
mathcomp.ssreflect.finset]
+
\bigcap_ ( _ <- _ | _ ) _ (set_scope) [in
mathcomp.ssreflect.finset]
+
\bigcup_ ( _ in _ ) _ (set_scope) [in
mathcomp.ssreflect.finset]
+
\bigcup_ ( _ in _ | _ ) _ (set_scope) [in
mathcomp.ssreflect.finset]
+
\bigcup_ ( _ < _ ) _ (set_scope) [in
mathcomp.ssreflect.finset]
+
\bigcup_ ( _ < _ | _ ) _ (set_scope) [in
mathcomp.ssreflect.finset]
+
\bigcup_ ( _ : _ ) _ (set_scope) [in
mathcomp.ssreflect.finset]
+
\bigcup_ ( _ : _ | _ ) _ (set_scope) [in
mathcomp.ssreflect.finset]
+
\bigcup_ _ _ (set_scope) [in
mathcomp.ssreflect.finset]
+
\bigcup_ ( _ | _ ) _ (set_scope) [in
mathcomp.ssreflect.finset]
+
\bigcup_ ( _ <= _ < _ ) _ (set_scope) [in
mathcomp.ssreflect.finset]
+
\bigcup_ ( _ <= _ < _ | _ ) _ (set_scope) [in
mathcomp.ssreflect.finset]
+
\bigcup_ ( _ <- _ ) _ (set_scope) [in
mathcomp.ssreflect.finset]
+
\bigcup_ ( _ <- _ | _ ) _ (set_scope) [in
mathcomp.ssreflect.finset]
+
[ se t _ | _ : _ , _ : _ & _ ] (set_scope) [in
mathcomp.ssreflect.finset]
+
[ se t _ | _ : _ , _ : _ ] (set_scope) [in
mathcomp.ssreflect.finset]
+
[ se t _ | _ : _ in _ , _ : _ & _ ] (set_scope) [in
mathcomp.ssreflect.finset]
+
[ se t _ | _ : _ in _ , _ : _ ] (set_scope) [in
mathcomp.ssreflect.finset]
+
[ se t _ | _ : _ , _ : _ in _ & _ ] (set_scope) [in
mathcomp.ssreflect.finset]
+
[ se t _ | _ : _ , _ : _ in _ ] (set_scope) [in
mathcomp.ssreflect.finset]
+
[ se t _ | _ in _ , _ in _ & _ ] (set_scope) [in
mathcomp.ssreflect.finset]
+
[ se t _ | _ in _ , _ in _ ] (set_scope) [in
mathcomp.ssreflect.finset]
+
[ set _ | _ , _ & _ ] (set_scope) [in
mathcomp.ssreflect.finset]
+
[ set _ | _ , _ ] (set_scope) [in
mathcomp.ssreflect.finset]
+
[ set _ | _ in _ , _ & _ ] (set_scope) [in
mathcomp.ssreflect.finset]
+
[ set _ | _ in _ , _ ] (set_scope) [in
mathcomp.ssreflect.finset]
+
[ set _ | _ , _ in _ & _ ] (set_scope) [in
mathcomp.ssreflect.finset]
+
[ set _ | _ , _ in _ ] (set_scope) [in
mathcomp.ssreflect.finset]
+
[ set _ | _ : _ , _ : _ & _ ] (set_scope) [in
mathcomp.ssreflect.finset]
+
[ set _ | _ : _ , _ : _ ] (set_scope) [in
mathcomp.ssreflect.finset]
+
[ set _ | _ : _ in _ , _ : _ & _ ] (set_scope) [in
mathcomp.ssreflect.finset]
+
[ set _ | _ : _ in _ , _ : _ ] (set_scope) [in
mathcomp.ssreflect.finset]
+
[ set _ | _ : _ , _ : _ in _ & _ ] (set_scope) [in
mathcomp.ssreflect.finset]
+
[ set _ | _ : _ , _ : _ in _ ] (set_scope) [in
mathcomp.ssreflect.finset]
+
[ set _ | _ : _ & _ ] (set_scope) [in
mathcomp.ssreflect.finset]
+
[ set _ | _ : _ ] (set_scope) [in
mathcomp.ssreflect.finset]
+
[ set _ | _ : _ in _ , _ : _ in _ & _ ] (set_scope) [in
mathcomp.ssreflect.finset]
+
[ set _ | _ : _ in _ , _ : _ in _ ] (set_scope) [in
mathcomp.ssreflect.finset]
+
[ set _ | _ : _ in _ & _ ] (set_scope) [in
mathcomp.ssreflect.finset]
+
[ set _ | _ : _ in _ ] (set_scope) [in
mathcomp.ssreflect.finset]
+
[ set _ | _ in _ , _ in _ & _ ] (set_scope) [in
mathcomp.ssreflect.finset]
+
[ set _ | _ in _ , _ in _ ] (set_scope) [in
mathcomp.ssreflect.finset]
+
[ set _ | _ in _ & _ ] (set_scope) [in
mathcomp.ssreflect.finset]
+
[ set _ | _ in _ ] (set_scope) [in
mathcomp.ssreflect.finset]
+
_ @2: ( _ , _ ) (set_scope) [in
mathcomp.ssreflect.finset]
+
_ @: _ (set_scope) [in
mathcomp.ssreflect.finset]
+
_ @^-1: _ (set_scope) [in
mathcomp.ssreflect.finset]
+
_ ::&: _ (set_scope) [in
mathcomp.ssreflect.finset]
+
_ :\ _ (set_scope) [in
mathcomp.ssreflect.finset]
+
_ :\: _ (set_scope) [in
mathcomp.ssreflect.finset]
+
[ set ~ _ ] (set_scope) [in
mathcomp.ssreflect.finset]
+
~: _ (set_scope) [in
mathcomp.ssreflect.finset]
+
_ :&: _ (set_scope) [in
mathcomp.ssreflect.finset]
+
[ set _ ; _ ; .. ; _ ] (set_scope) [in
mathcomp.ssreflect.finset]
+
_ |: _ (set_scope) [in
mathcomp.ssreflect.finset]
+
_ :|: _ (set_scope) [in
mathcomp.ssreflect.finset]
+
[ set _ : _ ] (set_scope) [in
mathcomp.ssreflect.finset]
+
[ set _ ] (set_scope) [in
mathcomp.ssreflect.finset]
+
[ set : _ ] (set_scope) [in
mathcomp.ssreflect.finset]
+
[ set _ : _ in _ | _ & _ ] (set_scope) [in
mathcomp.ssreflect.finset]
+
[ set _ in _ | _ & _ ] (set_scope) [in
mathcomp.ssreflect.finset]
+
[ set _ in _ | _ ] (set_scope) [in
mathcomp.ssreflect.finset]
+
[ set _ : _ in _ | _ ] (set_scope) [in
mathcomp.ssreflect.finset]
+
[ set _ | _ & _ ] (set_scope) [in
mathcomp.ssreflect.finset]
+
[ set _ : _ | _ & _ ] (set_scope) [in
mathcomp.ssreflect.finset]
+
[ set _ : _ in _ ] (set_scope) [in
mathcomp.ssreflect.finset]
+
[ set _ in _ ] (set_scope) [in
mathcomp.ssreflect.finset]
+
[ set _ | _ ] (set_scope) [in
mathcomp.ssreflect.finset]
+
[ set _ : _ | _ ] (set_scope) [in
mathcomp.ssreflect.finset]
+
_ :=P: _ (set_scope) [in
mathcomp.ssreflect.finset]
+
_ :!=: _ (set_scope) [in
mathcomp.ssreflect.finset]
+
_ :==: _ (set_scope) [in
mathcomp.ssreflect.finset]
+
_ :<>: _ (set_scope) [in
mathcomp.ssreflect.finset]
+
_ :=: _ (set_scope) [in
mathcomp.ssreflect.finset]
+
'forall 'X_ _ , _ (term_scope) [in
mathcomp.algebra.ssralg]
+
'exists 'X_ _ , _ (term_scope) [in
mathcomp.algebra.ssralg]
+
~ _ (term_scope) [in
mathcomp.algebra.ssralg]
+
_ ==> _ (term_scope) [in
mathcomp.algebra.ssralg]
+
_ \/ _ (term_scope) [in
mathcomp.algebra.ssralg]
+
_ /\ _ (term_scope) [in
mathcomp.algebra.ssralg]
+
_ != _ (term_scope) [in
mathcomp.algebra.ssralg]
+
_ == _ (term_scope) [in
mathcomp.algebra.ssralg]
+
_ ^+ _ (term_scope) [in
mathcomp.algebra.ssralg]
+
_ / _ (term_scope) [in
mathcomp.algebra.ssralg]
+
_ ^-1 (term_scope) [in
mathcomp.algebra.ssralg]
+
_ *+ _ (term_scope) [in
mathcomp.algebra.ssralg]
+
_ * _ (term_scope) [in
mathcomp.algebra.ssralg]
+
_ - _ (term_scope) [in
mathcomp.algebra.ssralg]
+
- _ (term_scope) [in
mathcomp.algebra.ssralg]
+
_ + _ (term_scope) [in
mathcomp.algebra.ssralg]
+
_ %:T (term_scope) [in
mathcomp.algebra.ssralg]
+
1 (term_scope) [in
mathcomp.algebra.ssralg]
+
0 (term_scope) [in
mathcomp.algebra.ssralg]
+
_ %:R (term_scope) [in
mathcomp.algebra.ssralg]
+
'X_ _ (term_scope) [in
mathcomp.algebra.ssralg]
+
_ ^o (type_scope) [in
mathcomp.algebra.ssralg]
+
_ ^c (type_scope) [in
mathcomp.algebra.ssralg]
+
{ perm _ } (type_scope) [in
mathcomp.fingroup.perm]
+
'D^ _ * Q (type_scope) [in
mathcomp.solvable.extraspecial]
+
'D^ _ (type_scope) [in
mathcomp.solvable.extraspecial]
+
_ ^{1+2* _ } (type_scope) [in
mathcomp.solvable.extraspecial]
+
_ ^{1+2} (type_scope) [in
mathcomp.solvable.extraspecial]
+
_ .-tuple (type_scope) [in
mathcomp.ssreflect.tuple]
+
{ 'GL_ _ ( _ ) } (type_scope) [in
mathcomp.algebra.matrix]
+
{ 'GL_ _ [ _ ] } (type_scope) [in
mathcomp.algebra.matrix]
+
'M_ ( _ ) (type_scope) [in
mathcomp.algebra.matrix]
+
'M_ _ (type_scope) [in
mathcomp.algebra.matrix]
+
'cV_ _ (type_scope) [in
mathcomp.algebra.matrix]
+
'rV_ _ (type_scope) [in
mathcomp.algebra.matrix]
+
'M_ ( _ , _ ) (type_scope) [in
mathcomp.algebra.matrix]
+
'M[ _ ]_ ( _ ) (type_scope) [in
mathcomp.algebra.matrix]
+
'M[ _ ]_ _ (type_scope) [in
mathcomp.algebra.matrix]
+
'cV[ _ ]_ _ (type_scope) [in
mathcomp.algebra.matrix]
+
'rV[ _ ]_ _ (type_scope) [in
mathcomp.algebra.matrix]
+
'M[ _ ]_ ( _ , _ ) (type_scope) [in
mathcomp.algebra.matrix]
+
'Q_ _ (type_scope) [in
mathcomp.solvable.extremal]
+
'SD_ _ (type_scope) [in
mathcomp.solvable.extremal]
+
'D_ _ (type_scope) [in
mathcomp.solvable.extremal]
+
'Mod_ _ (type_scope) [in
mathcomp.solvable.extremal]
+
{ unit _ } (type_scope) [in
mathcomp.algebra.finalg]
+
{ action _ &-> _ } (type_scope) [in
mathcomp.fingroup.action]
+
{ in _ , isometry _ , to _ } (type_scope) [in
mathcomp.character.classfun]
+
'CF ( _ ) (type_scope) [in
mathcomp.character.classfun]
+
_ ^ _ (type_scope) [in
mathcomp.ssreflect.finfun]
+
{ ffun _ } (type_scope) [in
mathcomp.ssreflect.finfun]
+
{ ? _ in _ | _ } (type_scope) [in
mathcomp.ssreflect.eqtype]
+
{ ? _ in _ } (type_scope) [in
mathcomp.ssreflect.eqtype]
+
{ ? _ | _ } (type_scope) [in
mathcomp.ssreflect.eqtype]
+
{ ? _ : _ | _ } (type_scope) [in
mathcomp.ssreflect.eqtype]
+
{ _ in _ | _ } (type_scope) [in
mathcomp.ssreflect.eqtype]
+
{ _ in _ } (type_scope) [in
mathcomp.ssreflect.eqtype]
+
[ subg _ ] (type_scope) [in
mathcomp.fingroup.fingroup]
+
{ group _ } (type_scope) [in
mathcomp.fingroup.fingroup]
+
@ fun_adjunction _ _ _ _ _ _ (type_scope) [in
mathcomp.ssreflect.fingraph]
+
@ rel_adjunction _ _ _ _ _ _ (type_scope) [in
mathcomp.ssreflect.fingraph]
+
'F_ _ (type_scope) [in
mathcomp.algebra.zmodp]
+
'Z_ _ (type_scope) [in
mathcomp.algebra.zmodp]
+
'AEnd ( _ ) (type_scope) [in
mathcomp.field.falgebra]
+
'AHom ( _ , _ ) (type_scope) [in
mathcomp.field.falgebra]
+
{ aspace _ } (type_scope) [in
mathcomp.field.falgebra]
+
'A [ _ ]_ _ (type_scope) [in
mathcomp.algebra.mxalgebra]
+
'A [ _ ]_ ( _ ) (type_scope) [in
mathcomp.algebra.mxalgebra]
+
'A [ _ ]_ ( _ , _ ) (type_scope) [in
mathcomp.algebra.mxalgebra]
+
'A_ _ (type_scope) [in
mathcomp.algebra.mxalgebra]
+
'A_ ( _ ) (type_scope) [in
mathcomp.algebra.mxalgebra]
+
'A_ ( _ , _ ) (type_scope) [in
mathcomp.algebra.mxalgebra]
+
{ set _ } (type_scope) [in
mathcomp.ssreflect.finset]
+
_ @^-1: _ (vspace_scope) [in
mathcomp.algebra.vector]
+
_ @: _ (vspace_scope) [in
mathcomp.algebra.vector]
+
\bigcap_ ( _ in _ ) _ (vspace_scope) [in
mathcomp.algebra.vector]
+
\bigcap_ ( _ in _ | _ ) _ (vspace_scope) [in
mathcomp.algebra.vector]
+
\bigcap_ ( _ < _ ) _ (vspace_scope) [in
mathcomp.algebra.vector]
+
\bigcap_ ( _ < _ | _ ) _ (vspace_scope) [in
mathcomp.algebra.vector]
+
\bigcap_ ( _ : _ ) _ (vspace_scope) [in
mathcomp.algebra.vector]
+
\bigcap_ ( _ : _ | _ ) _ (vspace_scope) [in
mathcomp.algebra.vector]
+
\bigcap_ _ _ (vspace_scope) [in
mathcomp.algebra.vector]
+
\bigcap_ ( _ | _ ) _ (vspace_scope) [in
mathcomp.algebra.vector]
+
\bigcap_ ( _ <= _ < _ ) _ (vspace_scope) [in
mathcomp.algebra.vector]
+
\bigcap_ ( _ <= _ < _ | _ ) _ (vspace_scope) [in
mathcomp.algebra.vector]
+
\bigcap_ ( _ <- _ ) _ (vspace_scope) [in
mathcomp.algebra.vector]
+
\bigcap_ ( _ <- _ | _ ) _ (vspace_scope) [in
mathcomp.algebra.vector]
+
\sum_ ( _ in _ ) _ (vspace_scope) [in
mathcomp.algebra.vector]
+
\sum_ ( _ in _ | _ ) _ (vspace_scope) [in
mathcomp.algebra.vector]
+
\sum_ ( _ < _ ) _ (vspace_scope) [in
mathcomp.algebra.vector]
+
\sum_ ( _ < _ | _ ) _ (vspace_scope) [in
mathcomp.algebra.vector]
+
\sum_ ( _ : _ ) _ (vspace_scope) [in
mathcomp.algebra.vector]
+
\sum_ ( _ : _ | _ ) _ (vspace_scope) [in
mathcomp.algebra.vector]
+
\sum_ _ _ (vspace_scope) [in
mathcomp.algebra.vector]
+
\sum_ ( _ | _ ) _ (vspace_scope) [in
mathcomp.algebra.vector]
+
\sum_ ( _ <= _ < _ ) _ (vspace_scope) [in
mathcomp.algebra.vector]
+
\sum_ ( _ <= _ < _ | _ ) _ (vspace_scope) [in
mathcomp.algebra.vector]
+
\sum_ ( _ <- _ ) _ (vspace_scope) [in
mathcomp.algebra.vector]
+
\sum_ ( _ <- _ | _ ) _ (vspace_scope) [in
mathcomp.algebra.vector]
+
{ : _ } (vspace_scope) [in
mathcomp.algebra.vector]
+
_ :\: _ (vspace_scope) [in
mathcomp.algebra.vector]
+
_ ^C (vspace_scope) [in
mathcomp.algebra.vector]
+
_ :&: _ (vspace_scope) [in
mathcomp.algebra.vector]
+
_ + _ (vspace_scope) [in
mathcomp.algebra.vector]
+
0 (vspace_scope) [in
mathcomp.algebra.vector]
+
<< _ >> (vspace_scope) [in
mathcomp.algebra.vector]
+
<[ _ ] > (vspace_scope) [in
mathcomp.algebra.vector]
+
_ <= _ <= _ (vspace_scope) [in
mathcomp.algebra.vector]
+
_ <= _ (vspace_scope) [in
mathcomp.algebra.vector]
+
'CF ( _ ) (vspace_scope) [in
mathcomp.character.classfun]
+
<< _ ; _ >> (vspace_scope) [in
mathcomp.field.falgebra]
+
<< _ & _ >> (vspace_scope) [in
mathcomp.field.falgebra]
+
'Z ( _ ) (vspace_scope) [in
mathcomp.field.falgebra]
+
'C_ ( _ ) ( _ ) (vspace_scope) [in
mathcomp.field.falgebra]
+
'C_ _ ( _ ) (vspace_scope) [in
mathcomp.field.falgebra]
+
'C ( _ ) (vspace_scope) [in
mathcomp.field.falgebra]
+
'C_ ( _ ) [ _ ] (vspace_scope) [in
mathcomp.field.falgebra]
+
'C_ _ [ _ ] (vspace_scope) [in
mathcomp.field.falgebra]
+
'C [ _ ] (vspace_scope) [in
mathcomp.field.falgebra]
+
_ ^+ _ (vspace_scope) [in
mathcomp.field.falgebra]
+
_ * _ (vspace_scope) [in
mathcomp.field.falgebra]
+
1 (vspace_scope) [in
mathcomp.field.falgebra]
+
_ \x _ [in
mathcomp.fingroup.gproduct]
+
_ \* _ [in
mathcomp.fingroup.gproduct]
+
_ ><| _ [in
mathcomp.fingroup.gproduct]
+
_ \isog _ [in
mathcomp.fingroup.morphism]
+
'Chi_ _ [in
mathcomp.character.character]
+
'exists_ _ [in
mathcomp.ssreflect.fintype]
+
'forall_ _ [in
mathcomp.ssreflect.fintype]
+
'I_ _ [in
mathcomp.ssreflect.fintype]
+
'Phi_ _ [in
mathcomp.field.cyclotomic]
+
'S_ _ [in
mathcomp.fingroup.perm]
+
*%N [in
mathcomp.ssreflect.bigop]
+
*%R [in
mathcomp.algebra.ssralg]
+
*:%R [in
mathcomp.algebra.ssralg]
+
+%N [in
mathcomp.ssreflect.bigop]
+
+%R [in
mathcomp.algebra.ssralg]
+
<< _ ; _ >> [in
mathcomp.field.algebraics_fundamentals]
+
@ perm [in
mathcomp.fingroup.perm]
+
@ sval [in
mathcomp.ssreflect.eqtype]
+
[ seq _ : _ <- _ | _ & _ ] [in
mathcomp.ssreflect.seq]
+
[ seq _ : _ <- _ | _ ] [in
mathcomp.ssreflect.seq]
+
[ pick _ : _ ] [in
mathcomp.ssreflect.fintype]
+
\d_ _ [in
mathcomp.algebra.fraction]
+
\mpi [in
mathcomp.ssreflect.generic_quotient]
+
\n_ _ [in
mathcomp.algebra.fraction]
+
{ideal_quot _ } [in
mathcomp.algebra.ring_quotient]
+
{ fraction _ } [in
mathcomp.algebra.fraction]
+
{ ratio _ } [in
mathcomp.algebra.fraction]
+
{ poly _ } [in
mathcomp.algebra.poly]
+
+
+| 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) |
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+| 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) |
+
+
+
A (notation)
+
<[nRA]> (action_scope) [in
mathcomp.fingroup.action]
+
_ != _ %[mod _ ] (C_scope) [in
mathcomp.field.algC]
+
_ == _ %[mod _ ] (C_scope) [in
mathcomp.field.algC]
+
_ %| _ (C_scope) [in
mathcomp.field.algC]
+
_ %| _ (C_expanded_scope) [in
mathcomp.field.algC]
+
_ ^* (ring_scope) [in
mathcomp.field.algC]
+
_ ^u [in
mathcomp.character.vcharacter]
+
+
+
+
+
+
+
+
+
+
+
+
+| 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) |
+
+
+
B (notation)
+
_ *F0: _ [in
mathcomp.field.fieldext]
+
+
+
+
+
+
+
+
+
+
+
+
+| 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) |
+
+
+
C (notation)
+
_ ^f (ring_scope) [in
mathcomp.character.mxrepresentation]
+
_ ^f (ring_scope) [in
mathcomp.character.mxrepresentation]
+
_ \char _ [in
mathcomp.fingroup.automorphism]
+
[ choiceType of _ ] (form_scope) [in
mathcomp.ssreflect.choice]
+
[ choiceType of _ for _ ] (form_scope) [in
mathcomp.ssreflect.choice]
+
'1_ _ [in
mathcomp.character.classfun]
+
<< _ ; _ >> (vspace_scope) [in
mathcomp.field.falgebra]
+
<< _ & _ >> (vspace_scope) [in
mathcomp.field.falgebra]
+
[ rec _ , _ , _ ] [in
mathcomp.ssreflect.choice]
+
` T (group_scope) [in
mathcomp.character.inertia]
+
_ / _ (Group_scope) [in
mathcomp.fingroup.quotient]
+
_ %% B (cfun_scope) [in
mathcomp.character.classfun]
+
_ / B (cfun_scope) [in
mathcomp.character.classfun]
+
[ countType of _ ] (form_scope) [in
mathcomp.ssreflect.choice]
+
[ countType of _ for _ ] (form_scope) [in
mathcomp.ssreflect.choice]
+
[ countClosedFieldType of _ ] (form_scope) [in
mathcomp.field.countalg]
+
[ countComRingType of _ ] (form_scope) [in
mathcomp.field.countalg]
+
[ countComUnitRingType of _ ] (form_scope) [in
mathcomp.field.countalg]
+
[ countDecFieldType of _ ] (form_scope) [in
mathcomp.field.countalg]
+
[ countFieldType of _ ] (form_scope) [in
mathcomp.field.countalg]
+
[ countIdomainType of _ ] (form_scope) [in
mathcomp.field.countalg]
+
[ countRingType of _ ] (form_scope) [in
mathcomp.field.countalg]
+
[ countUnitRingType of _ ] (form_scope) [in
mathcomp.field.countalg]
+
[ countZmodType of _ ] (form_scope) [in
mathcomp.field.countalg]
+
+
+
+
+
+
+
+
+
+
+
+
+| 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) |
+
+
+
D (notation)
+
'1_ _ (ring_scope) [in
mathcomp.character.classfun]
+
_ + _ [in
mathcomp.ssreflect.bigop]
+
_ * _ [in
mathcomp.ssreflect.bigop]
+
*%M [in
mathcomp.ssreflect.bigop]
+
+%M [in
mathcomp.ssreflect.bigop]
+
0 [in
mathcomp.ssreflect.bigop]
+
1 [in
mathcomp.ssreflect.bigop]
+
+
+
+
+
+
+
+
+
+
+
+
+| 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) |
+
+
+
E (notation)
+
[ eqType of _ ] (form_scope) [in
mathcomp.ssreflect.eqtype]
+
[ eqType of _ for _ ] (form_scope) [in
mathcomp.ssreflect.eqtype]
+
[ eqMixin of _ ] (form_scope) [in
mathcomp.ssreflect.eqtype]
+
+
+
+
+
+
+
+
+
+
+
+
+| 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) |
+
+
+
F (notation)
+
{ aspace _ } (type_scope) [in
mathcomp.field.falgebra]
+
'Z ( _ ) (vspace_scope) [in
mathcomp.field.falgebra]
+
'C ( _ ) (vspace_scope) [in
mathcomp.field.falgebra]
+
'C [ _ ] (vspace_scope) [in
mathcomp.field.falgebra]
+
_ ^+ _ (vspace_scope) [in
mathcomp.field.falgebra]
+
_ * _ (vspace_scope) [in
mathcomp.field.falgebra]
+
[ FalgType _ of _ for _ ] (form_scope) [in
mathcomp.field.falgebra]
+
[ FalgType _ of _ ] (form_scope) [in
mathcomp.field.falgebra]
+
_ ^u [in
mathcomp.character.classfun]
+
[ fieldExtType _ of _ for _ ] (form_scope) [in
mathcomp.field.fieldext]
+
[ fieldExtType _ of _ ] (form_scope) [in
mathcomp.field.fieldext]
+
{ subfield _ } (type_scope) [in
mathcomp.field.fieldext]
+
_ *F: _ [in
mathcomp.field.fieldext]
+
'Cl (action_scope) [in
mathcomp.character.mxrepresentation]
+
'e_ _ (group_ring_scope) [in
mathcomp.character.mxrepresentation]
+
'R_ _ (group_ring_scope) [in
mathcomp.character.mxrepresentation]
+
'n_ _ (group_ring_scope) [in
mathcomp.character.mxrepresentation]
+
1 (irrType_scope) [in
mathcomp.character.mxrepresentation]
+
[ 1 _ ] (irrType_scope) [in
mathcomp.character.mxrepresentation]
+
_ %| _ [in
mathcomp.field.finfield]
+
_ ^%:A (ring_scope) [in
mathcomp.field.finfield]
+
'Zm (action_scope) [in
mathcomp.character.mxabelem]
+
[ finGroupType of _ ] (form_scope) [in
mathcomp.fingroup.fingroup]
+
[ baseFinGroupType of _ ] (form_scope) [in
mathcomp.fingroup.fingroup]
+
_ ^-1 [in
mathcomp.fingroup.fingroup]
+
_ * _ [in
mathcomp.fingroup.fingroup]
+
1 [in
mathcomp.fingroup.fingroup]
+
'M (action_scope) [in
mathcomp.solvable.finmodule]
+
'M (groupAction_scope) [in
mathcomp.solvable.finmodule]
+
_ ^@ _ (ring_scope) [in
mathcomp.solvable.finmodule]
+
'M (action_scope) [in
mathcomp.solvable.finmodule]
+
'M (groupAction_scope) [in
mathcomp.solvable.finmodule]
+
_ ^@ _ (ring_scope) [in
mathcomp.solvable.finmodule]
+
, exists _ : _ in _ _ (bool_scope) [in
mathcomp.ssreflect.fintype]
+
, exists _ in _ _ (bool_scope) [in
mathcomp.ssreflect.fintype]
+
[ exists _ : _ in _ _ ] (bool_scope) [in
mathcomp.ssreflect.fintype]
+
[ exists _ in _ _ ] (bool_scope) [in
mathcomp.ssreflect.fintype]
+
[ exists ( _ : _ | _ ) _ ] (bool_scope) [in
mathcomp.ssreflect.fintype]
+
[ exists ( _ | _ ) _ ] (bool_scope) [in
mathcomp.ssreflect.fintype]
+
[ exists _ : _ _ ] (bool_scope) [in
mathcomp.ssreflect.fintype]
+
[ exists _ _ ] (bool_scope) [in
mathcomp.ssreflect.fintype]
+
, forall _ : _ in _ _ (bool_scope) [in
mathcomp.ssreflect.fintype]
+
, forall _ in _ _ (bool_scope) [in
mathcomp.ssreflect.fintype]
+
[ forall _ : _ in _ _ ] (bool_scope) [in
mathcomp.ssreflect.fintype]
+
[ forall _ in _ _ ] (bool_scope) [in
mathcomp.ssreflect.fintype]
+
[ forall ( _ : _ | _ ) _ ] (bool_scope) [in
mathcomp.ssreflect.fintype]
+
[ forall ( _ | _ ) _ ] (bool_scope) [in
mathcomp.ssreflect.fintype]
+
[ forall _ : _ _ ] (bool_scope) [in
mathcomp.ssreflect.fintype]
+
[ forall _ _ ] (bool_scope) [in
mathcomp.ssreflect.fintype]
+
, exists ( _ : _ | _ ) _ (fin_quant_scope) [in
mathcomp.ssreflect.fintype]
+
, exists ( _ | _ ) _ (fin_quant_scope) [in
mathcomp.ssreflect.fintype]
+
, exists _ : _ _ (fin_quant_scope) [in
mathcomp.ssreflect.fintype]
+
, exists _ _ (fin_quant_scope) [in
mathcomp.ssreflect.fintype]
+
, forall ( _ : _ | _ ) _ (fin_quant_scope) [in
mathcomp.ssreflect.fintype]
+
, forall ( _ | _ ) _ (fin_quant_scope) [in
mathcomp.ssreflect.fintype]
+
, forall _ : _ _ (fin_quant_scope) [in
mathcomp.ssreflect.fintype]
+
, forall _ _ (fin_quant_scope) [in
mathcomp.ssreflect.fintype]
+
, _ (fin_quant_scope) [in
mathcomp.ssreflect.fintype]
+
_ ^~ [in
mathcomp.ssreflect.fintype]
+
_ ^* [in
mathcomp.ssreflect.fintype]
+
[ _ : _ | _ ] [in
mathcomp.ssreflect.fintype]
+
[ _ | _ ] [in
mathcomp.ssreflect.fintype]
+
[ finType of _ ] (form_scope) [in
mathcomp.ssreflect.fintype]
+
[ finType of _ for _ ] (form_scope) [in
mathcomp.ssreflect.fintype]
+
[ finAlgType _ of _ ] (form_scope) [in
mathcomp.algebra.finalg]
+
[ finComRingType of _ ] (form_scope) [in
mathcomp.algebra.finalg]
+
[ finComUnitRingType of _ ] (form_scope) [in
mathcomp.algebra.finalg]
+
[ finFieldType of _ ] (form_scope) [in
mathcomp.algebra.finalg]
+
[ finIdomainType of _ ] (form_scope) [in
mathcomp.algebra.finalg]
+
[ finLalgType _ of _ ] (form_scope) [in
mathcomp.algebra.finalg]
+
[ finLmodType _ of _ ] (form_scope) [in
mathcomp.algebra.finalg]
+
[ finRingType of _ ] (form_scope) [in
mathcomp.algebra.finalg]
+
[ finUnitAlgType _ of _ ] (form_scope) [in
mathcomp.algebra.finalg]
+
[ finUnitRingType of _ ] (form_scope) [in
mathcomp.algebra.finalg]
+
[ finGroupType of _ for +%R ] (form_scope) [in
mathcomp.algebra.finalg]
+
[ baseFinGroupType of _ for +%R ] (form_scope) [in
mathcomp.algebra.finalg]
+
[ finZmodType of _ ] (form_scope) [in
mathcomp.algebra.finalg]
+
{ ratio _ } [in
mathcomp.algebra.fraction]
+
_ %:F [in
mathcomp.algebra.fraction]
+
_ %:F [in
mathcomp.algebra.fraction]
+
{ fraction _ } [in
mathcomp.algebra.fraction]
+
+
+| 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) |
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+| 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) |
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+| 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) |
+
+
+
I (notation)
+
'Ind[ _ ] (ring_scope) [in
mathcomp.character.classfun]
+
'Ind[ _ , _ ] (ring_scope) [in
mathcomp.character.classfun]
+
_ ^: _ (cfun_scope) [in
mathcomp.character.inertia]
+
'I_ _ [ _ ] (Group_scope) [in
mathcomp.character.inertia]
+
'I[ _ ] (Group_scope) [in
mathcomp.character.inertia]
+
'I_ _ [ _ ] (group_scope) [in
mathcomp.character.inertia]
+
'I[ _ ] (group_scope) [in
mathcomp.character.inertia]
+
_ ^ _ (ring_scope) [in
mathcomp.field.separable]
+
_ - _ (distn_scope) [in
mathcomp.algebra.ssrint]
+
`| _ | (nat_scope) [in
mathcomp.algebra.ssrint]
+
_ <= _ ?< if _ (ring_scope) [in
mathcomp.algebra.interval]
+
`] -oo , +oo [ (ring_scope) [in
mathcomp.algebra.interval]
+
`] _ , +oo [ (ring_scope) [in
mathcomp.algebra.interval]
+
`[ _ , +oo [ (ring_scope) [in
mathcomp.algebra.interval]
+
`] -oo , _ [ (ring_scope) [in
mathcomp.algebra.interval]
+
`] -oo , _ ] (ring_scope) [in
mathcomp.algebra.interval]
+
`] _ , _ [ (ring_scope) [in
mathcomp.algebra.interval]
+
`[ _ , _ [ (ring_scope) [in
mathcomp.algebra.interval]
+
`] _ , _ ] (ring_scope) [in
mathcomp.algebra.interval]
+
`[ _ , _ ] (ring_scope) [in
mathcomp.algebra.interval]
+
_ * _ (int_scope) [in
mathcomp.algebra.ssrint]
+
*%Z (int_scope) [in
mathcomp.algebra.ssrint]
+
1 (int_scope) [in
mathcomp.algebra.ssrint]
+
_ - _ (int_scope) [in
mathcomp.algebra.ssrint]
+
_ + _ (int_scope) [in
mathcomp.algebra.ssrint]
+
+%Z (int_scope) [in
mathcomp.algebra.ssrint]
+
- _ (int_scope) [in
mathcomp.algebra.ssrint]
+
-%Z (int_scope) [in
mathcomp.algebra.ssrint]
+
0 (int_scope) [in
mathcomp.algebra.ssrint]
+
'e_ _ [in
mathcomp.character.character]
+
'n_ _ [in
mathcomp.character.character]
+
'R_ _ [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) |
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+| 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) |
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+| 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 (notation)
+
_ ^-1 (lrfun_scope) [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) |
+
+
+
L (notation)
+
_ *:l _ [in
mathcomp.algebra.vector]
+
+
+
+
+
+
+
+
+
+
+
+
+| 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) |
+
+
+
M (notation)
+
_ ^f (ring_scope) [in
mathcomp.algebra.mxpoly]
+
_ ^f (ring_scope) [in
mathcomp.algebra.matrix]
+
_ ^f (ring_scope) [in
mathcomp.algebra.poly]
+
_ ^f (ring_scope) [in
mathcomp.algebra.mxpoly]
+
_ ^f (ring_scope) [in
mathcomp.algebra.mxalgebra]
+
_ ^f (ring_scope) [in
mathcomp.algebra.matrix]
+
_ ^f (ring_scope) [in
mathcomp.algebra.poly]
+
_ ^f (ring_scope) [in
mathcomp.algebra.poly]
+
_ ^f (ring_scope) [in
mathcomp.algebra.poly]
+
_ ^f (ring_scope) [in
mathcomp.algebra.matrix]
+
_ ^f (ring_scope) [in
mathcomp.algebra.mxpoly]
+
_ ^f (ring_scope) [in
mathcomp.algebra.matrix]
+
_ *m: _ (ring_scope) [in
mathcomp.algebra.matrix]
+
_ %:M (ring_scope) [in
mathcomp.algebra.matrix]
+
\tr _ (ring_scope) [in
mathcomp.algebra.matrix]
+
'Z ( _ ) (matrix_set_scope) [in
mathcomp.algebra.mxalgebra]
+
'C ( _ ) (matrix_set_scope) [in
mathcomp.algebra.mxalgebra]
+
_ * _ (matrix_set_scope) [in
mathcomp.algebra.mxalgebra]
+
\tr _ (ring_scope) [in
mathcomp.algebra.matrix]
+
_ *m _ (ring_scope) [in
mathcomp.algebra.matrix]
+
_ %:M (ring_scope) [in
mathcomp.algebra.matrix]
+
_ \in _ [in
mathcomp.algebra.mxalgebra]
+
_ ^T (ring_scope) [in
mathcomp.algebra.matrix]
+
_ * _ [in
mathcomp.ssreflect.bigop]
+
*%M [in
mathcomp.ssreflect.bigop]
+
_ * _ [in
mathcomp.ssreflect.bigop]
+
*%M [in
mathcomp.ssreflect.bigop]
+
1 [in
mathcomp.ssreflect.bigop]
+
[ add_law _ of _ ] (form_scope) [in
mathcomp.ssreflect.bigop]
+
[ mul_law of _ ] (form_scope) [in
mathcomp.ssreflect.bigop]
+
[ com_law of _ ] (form_scope) [in
mathcomp.ssreflect.bigop]
+
[ law of _ ] (form_scope) [in
mathcomp.ssreflect.bigop]
+
_ ^f [in
mathcomp.algebra.ssrint]
+
+
+| 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) |
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+| 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) |
+
+
+
N (notation)
+
_ .*2 (nat_scope) [in
mathcomp.ssreflect.ssrnat]
+
_ ^ _ (nat_scope) [in
mathcomp.ssreflect.ssrnat]
+
_ * _ (nat_scope) [in
mathcomp.ssreflect.ssrnat]
+
_ + _ (nat_scope) [in
mathcomp.ssreflect.ssrnat]
+
[ archiFieldType of _ ] (form_scope) [in
mathcomp.algebra.ssrnum]
+
[ archiFieldType of _ for _ ] (form_scope) [in
mathcomp.algebra.ssrnum]
+
[ numClosedFieldType of _ ] (form_scope) [in
mathcomp.algebra.ssrnum]
+
[ numClosedFieldType of _ for _ ] (form_scope) [in
mathcomp.algebra.ssrnum]
+
_ < _ (ring_scope) [in
mathcomp.algebra.ssrnum]
+
_ <= _ (ring_scope) [in
mathcomp.algebra.ssrnum]
+
[ numDomainType of _ ] (form_scope) [in
mathcomp.algebra.ssrnum]
+
[ numDomainType of _ for _ ] (form_scope) [in
mathcomp.algebra.ssrnum]
+
[ numFieldType of _ ] (form_scope) [in
mathcomp.algebra.ssrnum]
+
[ rcfType of _ ] (form_scope) [in
mathcomp.algebra.ssrnum]
+
[ rcfType of _ for _ ] (form_scope) [in
mathcomp.algebra.ssrnum]
+
[ realDomainType of _ ] (form_scope) [in
mathcomp.algebra.ssrnum]
+
[ realDomainType of _ for _ ] (form_scope) [in
mathcomp.algebra.ssrnum]
+
[ realFieldType of _ ] (form_scope) [in
mathcomp.algebra.ssrnum]
+
`| _ | (ring_scope) [in
mathcomp.algebra.ssrnum]
+
_ < _ [in
mathcomp.algebra.ssrnum]
+
_ <= _ [in
mathcomp.algebra.ssrnum]
+
_ <= _ ?= iff _ :> _ (ring_scope) [in
mathcomp.algebra.ssrnum]
+
_ <= _ ?= iff _ (ring_scope) [in
mathcomp.algebra.ssrnum]
+
_ < _ < _ (ring_scope) [in
mathcomp.algebra.ssrnum]
+
_ <= _ < _ (ring_scope) [in
mathcomp.algebra.ssrnum]
+
_ < _ <= _ (ring_scope) [in
mathcomp.algebra.ssrnum]
+
_ <= _ <= _ (ring_scope) [in
mathcomp.algebra.ssrnum]
+
_ >= _ :> _ (ring_scope) [in
mathcomp.algebra.ssrnum]
+
_ >= _ (ring_scope) [in
mathcomp.algebra.ssrnum]
+
_ <= _ :> _ (ring_scope) [in
mathcomp.algebra.ssrnum]
+
_ <= _ (ring_scope) [in
mathcomp.algebra.ssrnum]
+
_ > _ :> _ (ring_scope) [in
mathcomp.algebra.ssrnum]
+
_ > _ (ring_scope) [in
mathcomp.algebra.ssrnum]
+
_ < _ :> _ (ring_scope) [in
mathcomp.algebra.ssrnum]
+
_ < _ (ring_scope) [in
mathcomp.algebra.ssrnum]
+
>= _ :> _ (ring_scope) [in
mathcomp.algebra.ssrnum]
+
>= _ (ring_scope) [in
mathcomp.algebra.ssrnum]
+
<= _ :> _ (ring_scope) [in
mathcomp.algebra.ssrnum]
+
<= _ (ring_scope) [in
mathcomp.algebra.ssrnum]
+
> _ :> _ (ring_scope) [in
mathcomp.algebra.ssrnum]
+
> _ (ring_scope) [in
mathcomp.algebra.ssrnum]
+
< _ :> _ (ring_scope) [in
mathcomp.algebra.ssrnum]
+
< _ (ring_scope) [in
mathcomp.algebra.ssrnum]
+
[in mathcomp.algebra.ssrnum]
+
>=%R (ring_scope) [in
mathcomp.algebra.ssrnum]
+
<=%R (ring_scope) [in
mathcomp.algebra.ssrnum]
+
>%R (ring_scope) [in
mathcomp.algebra.ssrnum]
+
<%R (ring_scope) [in
mathcomp.algebra.ssrnum]
+
`| _ | (ring_scope) [in
mathcomp.algebra.ssrnum]
+
'Im _ (ring_scope) [in
mathcomp.algebra.ssrnum]
+
'Re _ (ring_scope) [in
mathcomp.algebra.ssrnum]
+
_ .-root (ring_scope) [in
mathcomp.algebra.ssrnum]
+
_ .-root (ring_core_scope) [in
mathcomp.algebra.ssrnum]
+
'Im _ (ring_scope) [in
mathcomp.algebra.ssrnum]
+
'Re _ (ring_scope) [in
mathcomp.algebra.ssrnum]
+
'i (ring_scope) [in
mathcomp.algebra.ssrnum]
+
_ .-root (ring_scope) [in
mathcomp.algebra.ssrnum]
+
'i (ring_scope) [in
mathcomp.algebra.ssrnum]
+
_ ^* (ring_scope) [in
mathcomp.algebra.ssrnum]
+
+
+| 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) |
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+| 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) |
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+| 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) |
+
+
+
P (notation)
+
_ ^f (ring_scope) [in
mathcomp.algebra.polydiv]
+
_ ^f (ring_scope) [in
mathcomp.algebra.polydiv]
+
_ %= _ (ring_scope) [in
mathcomp.algebra.polydiv]
+
_ %| _ (ring_scope) [in
mathcomp.algebra.polydiv]
+
_ %% _ (ring_scope) [in
mathcomp.algebra.polydiv]
+
_ %/ _ (ring_scope) [in
mathcomp.algebra.polydiv]
+
_ \Po _ (ring_scope) [in
mathcomp.algebra.poly]
+
_ ^`N ( _ ) (ring_scope) [in
mathcomp.algebra.poly]
+
_ ^` ( _ ) (ring_scope) [in
mathcomp.algebra.poly]
+
_ .-primitive_root (ring_scope) [in
mathcomp.algebra.poly]
+
_ .-unity_root (ring_scope) [in
mathcomp.algebra.poly]
+
_ .[ _ ] (ring_scope) [in
mathcomp.algebra.poly]
+
_ ^` [in
mathcomp.algebra.poly]
+
_ %:P [in
mathcomp.algebra.poly]
+
'X [in
mathcomp.algebra.poly]
+
'X^ _ [in
mathcomp.algebra.poly]
+
\poly_ ( _ < _ ) _ [in
mathcomp.algebra.poly]
+
_ *p: _ [in
mathcomp.field.finfield]
+
[ rec _ , _ , _ , _ , _ , _ ] [in
mathcomp.ssreflect.prime]
+
+
+
+
+
+
+
+
+
+
+
+
+| 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) |
+
+
+
Q (notation)
+
\pi [in
mathcomp.ssreflect.generic_quotient]
+
{quot _ } [in
mathcomp.algebra.ring_quotient]
+
+
+
+
+
+
+
+
+
+
+
+
+| 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) |
+
+
+
R (notation)
+
_ \isog _ [in
mathcomp.fingroup.morphism]
+
_ :\: _ (matrix_set_scope) [in
mathcomp.algebra.mxalgebra]
+
\bigcap_ ( _ | _ ) _ (matrix_set_scope) [in
mathcomp.algebra.mxalgebra]
+
_ :&: _ (matrix_set_scope) [in
mathcomp.algebra.mxalgebra]
+
\sum_ ( _ <- _ | _ ) _ (matrix_set_scope) [in
mathcomp.algebra.mxalgebra]
+
\sum_ ( _ | _ ) _ (matrix_set_scope) [in
mathcomp.algebra.mxalgebra]
+
_ + _ (matrix_set_scope) [in
mathcomp.algebra.mxalgebra]
+
<< _ >> (matrix_set_scope) [in
mathcomp.algebra.mxalgebra]
+
_ :=: _ (matrix_set_scope) [in
mathcomp.algebra.mxalgebra]
+
_ < _ (matrix_set_scope) [in
mathcomp.algebra.mxalgebra]
+
_ == _ (matrix_set_scope) [in
mathcomp.algebra.mxalgebra]
+
_ <= _ <= _ (matrix_set_scope) [in
mathcomp.algebra.mxalgebra]
+
_ <= _ (matrix_set_scope) [in
mathcomp.algebra.mxalgebra]
+
_ ^C (matrix_set_scope) [in
mathcomp.algebra.mxalgebra]
+
\rank _ (nat_scope) [in
mathcomp.algebra.mxalgebra]
+
'M_ _ (type_scope) [in
mathcomp.algebra.mxalgebra]
+
'M_ ( _ , _ ) (type_scope) [in
mathcomp.algebra.mxalgebra]
+
+
+
+
+
+
+
+
+
+
+
+
+| 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) |
+
+
+
S (notation)
+
_ ++ _ (seq_scope) [in
mathcomp.ssreflect.seq]
+
[ splittingFieldType _ of _ ] (form_scope) [in
mathcomp.field.galois]
+
[ splittingFieldType _ of _ for _ ] (form_scope) [in
mathcomp.field.galois]
+
_ ^iota (ring_scope) [in
mathcomp.field.fieldext]
+
'Alt_T [in
mathcomp.solvable.alt]
+
'Sym_T [in
mathcomp.solvable.alt]
+
+
+
+
+
+
+
+
+
+
+
+
+| 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) |
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+| 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 (notation)
+
_ .-primitive_root (unity_root_scope) [in
mathcomp.algebra.poly]
+
_ .-unity_root (unity_root_scope) [in
mathcomp.algebra.poly]
+
+
+
+
+
+
+
+
+
+
+
+
+| 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) |
+
+
+
V (notation)
+
[ vectType _ of _ ] (form_scope) [in
mathcomp.algebra.vector]
+
[ vectType _ of _ for _ ] (form_scope) [in
mathcomp.algebra.vector]
+
'End ( _ ) (type_scope) [in
mathcomp.algebra.vector]
+
'Hom ( _ , _ ) (type_scope) [in
mathcomp.algebra.vector]
+
{ vspace _ } (type_scope) [in
mathcomp.algebra.vector]
+
+
+
+
+
+
+
+
+
+
+
+
+| 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) |
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+| 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) |
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+| 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) |
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+| 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 (notation)
+
_ ^z (type_scope) [in
mathcomp.algebra.ssrint]
+
+
+
+
+
+
+
+
+
+
+
+
+| 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) |
+
+
+
+
+
+
+