From 748d716efb2f2f75946c8386e441ce1789806a39 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 22 May 2019 13:43:08 +0200
Subject: htmldoc regenerated
---
docs/htmldoc/index_notation_*.html | 1994 ++++++++++++++++++------------------
docs/htmldoc/index_notation_A.html | 50 +-
docs/htmldoc/index_notation_B.html | 38 +-
docs/htmldoc/index_notation_C.html | 87 +-
docs/htmldoc/index_notation_D.html | 50 +-
docs/htmldoc/index_notation_E.html | 47 +-
docs/htmldoc/index_notation_F.html | 232 ++---
docs/htmldoc/index_notation_G.html | 320 +++---
docs/htmldoc/index_notation_H.html | 36 +-
docs/htmldoc/index_notation_I.html | 542 +---------
docs/htmldoc/index_notation_J.html | 36 +-
docs/htmldoc/index_notation_K.html | 38 +-
docs/htmldoc/index_notation_L.html | 39 +-
docs/htmldoc/index_notation_M.html | 136 +--
docs/htmldoc/index_notation_N.html | 194 ++--
docs/htmldoc/index_notation_O.html | 36 +-
docs/htmldoc/index_notation_P.html | 75 +-
docs/htmldoc/index_notation_Q.html | 40 +-
docs/htmldoc/index_notation_R.html | 70 +-
docs/htmldoc/index_notation_S.html | 48 +-
docs/htmldoc/index_notation_T.html | 36 +-
docs/htmldoc/index_notation_U.html | 40 +-
docs/htmldoc/index_notation_V.html | 46 +-
docs/htmldoc/index_notation_W.html | 36 +-
docs/htmldoc/index_notation_X.html | 36 +-
docs/htmldoc/index_notation_Y.html | 36 +-
docs/htmldoc/index_notation_Z.html | 38 +-
docs/htmldoc/index_notation__.html | 36 +-
28 files changed, 1999 insertions(+), 2413 deletions(-)
(limited to 'docs/htmldoc/index_notation_*.html')
diff --git a/docs/htmldoc/index_notation_*.html b/docs/htmldoc/index_notation_*.html
index b464b44..4ceb661 100644
--- a/docs/htmldoc/index_notation_*.html
+++ b/docs/htmldoc/index_notation_*.html
@@ -4,7 +4,7 @@
-mathcomp.ssreflect.tuple
+mathcomp.test_suite.hierarchy_test
@@ -47,7 +47,7 @@
| Z |
_ |
other |
-(23233 entries) |
+(23836 entries) |
| Notation Index |
@@ -79,14 +79,14 @@
Z |
_ |
other |
-(1373 entries) |
+(1409 entries) |
| Module Index |
A |
B |
C |
-D |
+D |
E |
F |
G |
@@ -111,7 +111,7 @@
Z |
_ |
other |
-(213 entries) |
+(221 entries) |
| Variable Index |
@@ -143,7 +143,7 @@
Z |
_ |
other |
-(3475 entries) |
+(3574 entries) |
| Library Index |
@@ -175,7 +175,7 @@
Z |
_ |
other |
-(89 entries) |
+(90 entries) |
| Lemma Index |
@@ -207,7 +207,7 @@
Z |
_ |
other |
-(11853 entries) |
+(12096 entries) |
| Constructor Index |
@@ -239,7 +239,7 @@
Z |
_ |
other |
-(359 entries) |
+(368 entries) |
| Axiom Index |
@@ -271,7 +271,7 @@
Z |
_ |
other |
-(47 entries) |
+(45 entries) |
| Inductive Index |
@@ -303,14 +303,14 @@
Z |
_ |
other |
-(103 entries) |
+(107 entries) |
| Projection Index |
A |
B |
C |
-D |
+D |
E |
F |
G |
@@ -335,7 +335,7 @@
Z |
_ |
other |
-(266 entries) |
+(273 entries) |
| Section Index |
@@ -367,7 +367,7 @@
Z |
_ |
other |
-(1118 entries) |
+(1140 entries) |
| Abbreviation Index |
@@ -399,7 +399,7 @@
Z |
_ |
other |
-(691 entries) |
+(728 entries) |
| Definition Index |
@@ -431,14 +431,14 @@
Z |
_ |
other |
-(3461 entries) |
+(3596 entries) |
| Record Index |
A |
B |
C |
-D |
+D |
E |
F |
G |
@@ -463,957 +463,987 @@
Z |
_ |
other |
-(185 entries) |
+(189 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]
+'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]
+[ <-> _ ; _ ; .. ; _ ] (form_scope) [in mathcomp.ssreflect.seq]
+[ 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]
+[ rel _ _ in _ ] (fun_scope) [in mathcomp.ssreflect.ssrbool]
+[ rel _ _ in _ | _ ] (fun_scope) [in mathcomp.ssreflect.ssrbool]
+[ rel _ _ in _ & _ ] (fun_scope) [in mathcomp.ssreflect.ssrbool]
+[ rel _ _ in _ & _ | _ ] (fun_scope) [in mathcomp.ssreflect.ssrbool]
+[ rel _ _ : _ | _ ] (fun_scope) [in mathcomp.ssreflect.ssrbool]
+[ rel _ _ | _ ] (fun_scope) [in mathcomp.ssreflect.ssrbool]
+_ .-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]
+[ 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.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]
+`] -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]
+_ <= _ ?< if _ (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 _ | _ : _ <- _ & _ ] (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]
+{ pred _ } (type_scope) [in mathcomp.ssreflect.ssrbool]
+_ ^ _ (type_scope) [in mathcomp.ssreflect.finfun]
+{ dffun _ } (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]
+Falgebra.type [in mathcomp.test_suite.hierarchy_test]
+FieldExt.type [in mathcomp.test_suite.hierarchy_test]
+FinRing.Algebra.type [in mathcomp.test_suite.hierarchy_test]
+FinRing.Lalgebra.type [in mathcomp.test_suite.hierarchy_test]
+FinRing.Lmodule.type [in mathcomp.test_suite.hierarchy_test]
+FinRing.UnitAlgebra.type [in mathcomp.test_suite.hierarchy_test]
+GRing.Algebra.type [in mathcomp.test_suite.hierarchy_test]
+GRing.Lalgebra.type [in mathcomp.test_suite.hierarchy_test]
+GRing.Lmodule.type [in mathcomp.test_suite.hierarchy_test]
+GRing.UnitAlgebra.type [in mathcomp.test_suite.hierarchy_test]
+SplittingField.type [in mathcomp.test_suite.hierarchy_test]
+Vector.type [in mathcomp.test_suite.hierarchy_test]
+'Chi_ _ [in mathcomp.character.character]
+'exists_in_ _ [in mathcomp.ssreflect.fintype]
+'exists_ _ [in mathcomp.ssreflect.fintype]
+'forall_in_ _ [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]
+@ perm_eq_trans [in mathcomp.ssreflect.seq]
+@ eq_big_perm [in mathcomp.ssreflect.bigop]
+@ ffun_on _ _ [in mathcomp.ssreflect.finfun]
+@ 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 |
@@ -1445,7 +1475,7 @@
Z |
_ |
other |
-(23233 entries) |
+(23836 entries) |
| Notation Index |
@@ -1477,14 +1507,14 @@
Z |
_ |
other |
-(1373 entries) |
+(1409 entries) |
| Module Index |
A |
B |
C |
-D |
+D |
E |
F |
G |
@@ -1509,7 +1539,7 @@
Z |
_ |
other |
-(213 entries) |
+(221 entries) |
| Variable Index |
@@ -1541,7 +1571,7 @@
Z |
_ |
other |
-(3475 entries) |
+(3574 entries) |
| Library Index |
@@ -1573,7 +1603,7 @@
Z |
_ |
other |
-(89 entries) |
+(90 entries) |
| Lemma Index |
@@ -1605,7 +1635,7 @@
Z |
_ |
other |
-(11853 entries) |
+(12096 entries) |
| Constructor Index |
@@ -1637,7 +1667,7 @@
Z |
_ |
other |
-(359 entries) |
+(368 entries) |
| Axiom Index |
@@ -1669,7 +1699,7 @@
Z |
_ |
other |
-(47 entries) |
+(45 entries) |
| Inductive Index |
@@ -1701,14 +1731,14 @@
Z |
_ |
other |
-(103 entries) |
+(107 entries) |
| Projection Index |
A |
B |
C |
-D |
+D |
E |
F |
G |
@@ -1733,7 +1763,7 @@
Z |
_ |
other |
-(266 entries) |
+(273 entries) |
| Section Index |
@@ -1765,7 +1795,7 @@
Z |
_ |
other |
-(1118 entries) |
+(1140 entries) |
| Abbreviation Index |
@@ -1797,7 +1827,7 @@
Z |
_ |
other |
-(691 entries) |
+(728 entries) |
| Definition Index |
@@ -1829,14 +1859,14 @@
Z |
_ |
other |
-(3461 entries) |
+(3596 entries) |
| Record Index |
A |
B |
C |
-D |
+D |
E |
F |
G |
@@ -1861,7 +1891,7 @@
Z |
_ |
other |
-(185 entries) |
+(189 entries) |
diff --git a/docs/htmldoc/index_notation_A.html b/docs/htmldoc/index_notation_A.html
index bdf10c3..288d94f 100644
--- a/docs/htmldoc/index_notation_A.html
+++ b/docs/htmldoc/index_notation_A.html
@@ -4,7 +4,7 @@
-mathcomp.ssreflect.tuple
+mathcomp.test_suite.hierarchy_test
@@ -47,7 +47,7 @@
Z |
_ |
other |
-(23233 entries) |
+(23836 entries) |
| Notation Index |
@@ -79,14 +79,14 @@
Z |
_ |
other |
-(1373 entries) |
+(1409 entries) |
| Module Index |
A |
B |
C |
-D |
+D |
E |
F |
G |
@@ -111,7 +111,7 @@
Z |
_ |
other |
-(213 entries) |
+(221 entries) |
| Variable Index |
@@ -143,7 +143,7 @@
Z |
_ |
other |
-(3475 entries) |
+(3574 entries) |
| Library Index |
@@ -175,7 +175,7 @@
Z |
_ |
other |
-(89 entries) |
+(90 entries) |
| Lemma Index |
@@ -207,7 +207,7 @@
Z |
_ |
other |
-(11853 entries) |
+(12096 entries) |
| Constructor Index |
@@ -239,7 +239,7 @@
Z |
_ |
other |
-(359 entries) |
+(368 entries) |
| Axiom Index |
@@ -271,7 +271,7 @@
Z |
_ |
other |
-(47 entries) |
+(45 entries) |
| Inductive Index |
@@ -303,14 +303,14 @@
Z |
_ |
other |
-(103 entries) |
+(107 entries) |
| Projection Index |
A |
B |
C |
-D |
+D |
E |
F |
G |
@@ -335,7 +335,7 @@
Z |
_ |
other |
-(266 entries) |
+(273 entries) |
| Section Index |
@@ -367,7 +367,7 @@
Z |
_ |
other |
-(1118 entries) |
+(1140 entries) |
| Abbreviation Index |
@@ -399,7 +399,7 @@
Z |
_ |
other |
-(691 entries) |
+(728 entries) |
| Definition Index |
@@ -431,14 +431,14 @@
Z |
_ |
other |
-(3461 entries) |
+(3596 entries) |
| Record Index |
A |
B |
C |
-D |
+D |
E |
F |
G |
@@ -463,17 +463,17 @@
Z |
_ |
other |
-(185 entries) |
+(189 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]
+<[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]
diff --git a/docs/htmldoc/index_notation_G.html b/docs/htmldoc/index_notation_G.html
index 0600a7c..9287491 100644
--- a/docs/htmldoc/index_notation_G.html
+++ b/docs/htmldoc/index_notation_G.html
@@ -4,7 +4,7 @@
-mathcomp.ssreflect.tuple
+mathcomp.test_suite.hierarchy_test
@@ -47,7 +47,7 @@
Z |
_ |
other |
-(23233 entries) |
+(23836 entries) |
| Notation Index |
@@ -79,14 +79,14 @@
Z |
_ |
other |
-(1373 entries) |
+(1409 entries) |
| Module Index |
A |
B |
C |
-D |
+D |
E |
F |
G |
@@ -111,7 +111,7 @@
Z |
_ |
other |
-(213 entries) |
+(221 entries) |
| Variable Index |
@@ -143,7 +143,7 @@
Z |
_ |
other |
-(3475 entries) |
+(3574 entries) |
| Library Index |
@@ -175,7 +175,7 @@
Z |
_ |
other |
-(89 entries) |
+(90 entries) |
| Lemma Index |
@@ -207,7 +207,7 @@
Z |
_ |
other |
-(11853 entries) |
+(12096 entries) |
| Constructor Index |
@@ -239,7 +239,7 @@
Z |
_ |
other |
-(359 entries) |
+(368 entries) |
| Axiom Index |
@@ -271,7 +271,7 @@
Z |
_ |
other |
-(47 entries) |
+(45 entries) |
| Inductive Index |
@@ -303,14 +303,14 @@
Z |
_ |
other |
-(103 entries) |
+(107 entries) |
| Projection Index |
A |
B |
C |
-D |
+D |
E |
F |
G |
@@ -335,7 +335,7 @@
Z |
_ |
other |
-(266 entries) |
+(273 entries) |
| Section Index |
@@ -367,7 +367,7 @@
Z |
_ |
other |
-(1118 entries) |
+(1140 entries) |
| Abbreviation Index |
@@ -399,7 +399,7 @@
Z |
_ |
other |
-(691 entries) |
+(728 entries) |
| Definition Index |
@@ -431,14 +431,14 @@
Z |
_ |
other |
-(3461 entries) |
+(3596 entries) |
| Record Index |
A |
B |
C |
-D |
+D |
E |
F |
G |
@@ -463,135 +463,135 @@
Z |
_ |
other |
-(185 entries) |
+(189 entries) |
G (notation)
-'Gal ( _ / _ ) (Group_scope) [in mathcomp.field.galois]
-'Gal ( _ / _ ) (group_scope) [in mathcomp.field.galois]
-'K_ _ (ring_scope) [in mathcomp.character.integral_char]
-[ mgFun of _ ] (form_scope) [in mathcomp.solvable.gfunctor]
-[ mgFun by _ ] (form_scope) [in mathcomp.solvable.gfunctor]
-[ pgFun of _ ] (form_scope) [in mathcomp.solvable.gfunctor]
-[ pgFun by _ ] (form_scope) [in mathcomp.solvable.gfunctor]
-[ gFun of _ ] (form_scope) [in mathcomp.solvable.gfunctor]
-[ gFun by _ ] (form_scope) [in mathcomp.solvable.gfunctor]
-[ igFun of _ ] (form_scope) [in mathcomp.solvable.gfunctor]
-[ igFun by _ & ! _ ] (form_scope) [in mathcomp.solvable.gfunctor]
-[ igFun by _ & _ ] (form_scope) [in mathcomp.solvable.gfunctor]
-[ additive of _ ] (form_scope) [in mathcomp.algebra.ssralg]
-[ additive of _ as _ ] (form_scope) [in mathcomp.algebra.ssralg]
-{ additive _ } (ring_scope) [in mathcomp.algebra.ssralg]
-[ algType _ of _ ] (form_scope) [in mathcomp.algebra.ssralg]
-[ algType _ of _ for _ ] (form_scope) [in mathcomp.algebra.ssralg]
-[ closedFieldType of _ ] (form_scope) [in mathcomp.algebra.ssralg]
-[ closedFieldType of _ for _ ] (form_scope) [in mathcomp.algebra.ssralg]
-[ comRingType of _ ] (form_scope) [in mathcomp.algebra.ssralg]
-[ comRingType of _ for _ ] (form_scope) [in mathcomp.algebra.ssralg]
-[ comUnitRingType of _ ] (form_scope) [in mathcomp.algebra.ssralg]
-[ decFieldType of _ ] (form_scope) [in mathcomp.algebra.ssralg]
-[ decFieldType of _ for _ ] (form_scope) [in mathcomp.algebra.ssralg]
-[ rec _ , _ ] [in mathcomp.algebra.ssralg]
-[ fieldType of _ ] (form_scope) [in mathcomp.algebra.ssralg]
-[ fieldType of _ for _ ] (form_scope) [in mathcomp.algebra.ssralg]
-[ idomainType of _ ] (form_scope) [in mathcomp.algebra.ssralg]
-[ idomainType of _ for _ ] (form_scope) [in mathcomp.algebra.ssralg]
-[ lalgType _ of _ ] (form_scope) [in mathcomp.algebra.ssralg]
-[ lalgType _ of _ for _ ] (form_scope) [in mathcomp.algebra.ssralg]
-[ linear of _ ] (form_scope) [in mathcomp.algebra.ssralg]
-[ linear of _ as _ ] (form_scope) [in mathcomp.algebra.ssralg]
-_ *^ _ _ (linear_ring_scope) [in mathcomp.algebra.ssralg]
-_ *:^ _ _ (linear_ring_scope) [in mathcomp.algebra.ssralg]
-_ * _ (linear_ring_scope) [in mathcomp.algebra.ssralg]
-_ *: _ (linear_ring_scope) [in mathcomp.algebra.ssralg]
-{ scalar _ } (ring_scope) [in mathcomp.algebra.ssralg]
-{ linear _ } (ring_scope) [in mathcomp.algebra.ssralg]
-{ linear _ | _ } (ring_scope) [in mathcomp.algebra.ssralg]
-*:%R [in mathcomp.algebra.ssralg]
-[ lmodType _ of _ ] (form_scope) [in mathcomp.algebra.ssralg]
-[ lmodType _ of _ for _ ] (form_scope) [in mathcomp.algebra.ssralg]
-[ lrmorphism of _ ] (form_scope) [in mathcomp.algebra.ssralg]
-{ lrmorphism _ } (ring_scope) [in mathcomp.algebra.ssralg]
-{ lrmorphism _ | _ } (ring_scope) [in mathcomp.algebra.ssralg]
-_ ^f [in mathcomp.algebra.ssralg]
-[ ringType of _ ] (form_scope) [in mathcomp.algebra.ssralg]
-[ ringType of _ for _ ] (form_scope) [in mathcomp.algebra.ssralg]
-[ rmorphism of _ ] (form_scope) [in mathcomp.algebra.ssralg]
-[ rmorphism of _ as _ ] (form_scope) [in mathcomp.algebra.ssralg]
-{ rmorphism _ } (ring_scope) [in mathcomp.algebra.ssralg]
-[ fieldMixin of _ by <: ] (form_scope) [in mathcomp.algebra.ssralg]
-[ idomainMixin of _ by <: ] (form_scope) [in mathcomp.algebra.ssralg]
-[ unitRingMixin of _ by <: ] (form_scope) [in mathcomp.algebra.ssralg]
-[ algMixin of _ by <: ] (form_scope) [in mathcomp.algebra.ssralg]
-[ comRingMixin of _ by <: ] (form_scope) [in mathcomp.algebra.ssralg]
-[ lalgMixin of _ by <: ] (form_scope) [in mathcomp.algebra.ssralg]
-[ lmodMixin of _ by <: ] (form_scope) [in mathcomp.algebra.ssralg]
-[ ringMixin of _ by <: ] (form_scope) [in mathcomp.algebra.ssralg]
-[ zmodMixin of _ by <: ] (form_scope) [in mathcomp.algebra.ssralg]
-[ unitAlgType _ of _ ] (form_scope) [in mathcomp.algebra.ssralg]
-[ unitRingType of _ ] (form_scope) [in mathcomp.algebra.ssralg]
-[ unitRingType of _ for _ ] (form_scope) [in mathcomp.algebra.ssralg]
-[ zmodType of _ ] (form_scope) [in mathcomp.algebra.ssralg]
-[ zmodType of _ for _ ] (form_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]
-[ char _ ] (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]
-- 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]
-+%R (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]
-'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]
-1 (term_scope) [in mathcomp.algebra.ssralg]
-0 (term_scope) [in mathcomp.algebra.ssralg]
-_ %:T (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]
-_ ^- _ [in mathcomp.algebra.ssralg]
-_ / _ [in mathcomp.algebra.ssralg]
-_ ^-1 [in mathcomp.algebra.ssralg]
-*%R [in mathcomp.algebra.ssralg]
-*:%R [in mathcomp.algebra.ssralg]
-\prod_ ( _ <= _ < _ ) _ [in mathcomp.algebra.ssralg]
-\prod_ ( _ in _ ) _ [in mathcomp.algebra.ssralg]
-\prod_ ( _ | _ ) _ [in mathcomp.algebra.ssralg]
-\prod_ ( _ <- _ | _ ) _ [in mathcomp.algebra.ssralg]
-\sum_ ( _ in _ ) _ [in mathcomp.algebra.ssralg]
-\sum_ ( _ < _ ) _ [in mathcomp.algebra.ssralg]
-\sum_ ( _ <= _ < _ ) _ [in mathcomp.algebra.ssralg]
-\sum_ ( _ <- _ | _ ) _ [in mathcomp.algebra.ssralg]
+'Gal ( _ / _ ) (Group_scope) [in mathcomp.field.galois]
+'Gal ( _ / _ ) (group_scope) [in mathcomp.field.galois]
+'K_ _ (ring_scope) [in mathcomp.character.integral_char]
+[ mgFun of _ ] (form_scope) [in mathcomp.solvable.gfunctor]
+[ mgFun by _ ] (form_scope) [in mathcomp.solvable.gfunctor]
+[ pgFun of _ ] (form_scope) [in mathcomp.solvable.gfunctor]
+[ pgFun by _ ] (form_scope) [in mathcomp.solvable.gfunctor]
+[ gFun of _ ] (form_scope) [in mathcomp.solvable.gfunctor]
+[ gFun by _ ] (form_scope) [in mathcomp.solvable.gfunctor]
+[ igFun of _ ] (form_scope) [in mathcomp.solvable.gfunctor]
+[ igFun by _ & ! _ ] (form_scope) [in mathcomp.solvable.gfunctor]
+[ igFun by _ & _ ] (form_scope) [in mathcomp.solvable.gfunctor]
+[ additive of _ ] (form_scope) [in mathcomp.algebra.ssralg]
+[ additive of _ as _ ] (form_scope) [in mathcomp.algebra.ssralg]
+{ additive _ } (ring_scope) [in mathcomp.algebra.ssralg]
+[ algType _ of _ ] (form_scope) [in mathcomp.algebra.ssralg]
+[ algType _ of _ for _ ] (form_scope) [in mathcomp.algebra.ssralg]
+[ closedFieldType of _ ] (form_scope) [in mathcomp.algebra.ssralg]
+[ closedFieldType of _ for _ ] (form_scope) [in mathcomp.algebra.ssralg]
+[ comRingType of _ ] (form_scope) [in mathcomp.algebra.ssralg]
+[ comRingType of _ for _ ] (form_scope) [in mathcomp.algebra.ssralg]
+[ comUnitRingType of _ ] (form_scope) [in mathcomp.algebra.ssralg]
+[ decFieldType of _ ] (form_scope) [in mathcomp.algebra.ssralg]
+[ decFieldType of _ for _ ] (form_scope) [in mathcomp.algebra.ssralg]
+[ rec _ , _ ] [in mathcomp.algebra.ssralg]
+[ fieldType of _ ] (form_scope) [in mathcomp.algebra.ssralg]
+[ fieldType of _ for _ ] (form_scope) [in mathcomp.algebra.ssralg]
+[ idomainType of _ ] (form_scope) [in mathcomp.algebra.ssralg]
+[ idomainType of _ for _ ] (form_scope) [in mathcomp.algebra.ssralg]
+[ lalgType _ of _ ] (form_scope) [in mathcomp.algebra.ssralg]
+[ lalgType _ of _ for _ ] (form_scope) [in mathcomp.algebra.ssralg]
+[ linear of _ ] (form_scope) [in mathcomp.algebra.ssralg]
+[ linear of _ as _ ] (form_scope) [in mathcomp.algebra.ssralg]
+_ *^ _ _ (linear_ring_scope) [in mathcomp.algebra.ssralg]
+_ *:^ _ _ (linear_ring_scope) [in mathcomp.algebra.ssralg]
+_ * _ (linear_ring_scope) [in mathcomp.algebra.ssralg]
+_ *: _ (linear_ring_scope) [in mathcomp.algebra.ssralg]
+{ scalar _ } (ring_scope) [in mathcomp.algebra.ssralg]
+{ linear _ } (ring_scope) [in mathcomp.algebra.ssralg]
+{ linear _ | _ } (ring_scope) [in mathcomp.algebra.ssralg]
+*:%R [in mathcomp.algebra.ssralg]
+[ lmodType _ of _ ] (form_scope) [in mathcomp.algebra.ssralg]
+[ lmodType _ of _ for _ ] (form_scope) [in mathcomp.algebra.ssralg]
+[ lrmorphism of _ ] (form_scope) [in mathcomp.algebra.ssralg]
+{ lrmorphism _ } (ring_scope) [in mathcomp.algebra.ssralg]
+{ lrmorphism _ | _ } (ring_scope) [in mathcomp.algebra.ssralg]
+_ ^f [in mathcomp.algebra.ssralg]
+[ ringType of _ ] (form_scope) [in mathcomp.algebra.ssralg]
+[ ringType of _ for _ ] (form_scope) [in mathcomp.algebra.ssralg]
+[ rmorphism of _ ] (form_scope) [in mathcomp.algebra.ssralg]
+[ rmorphism of _ as _ ] (form_scope) [in mathcomp.algebra.ssralg]
+{ rmorphism _ } (ring_scope) [in mathcomp.algebra.ssralg]
+[ fieldMixin of _ by <: ] (form_scope) [in mathcomp.algebra.ssralg]
+[ idomainMixin of _ by <: ] (form_scope) [in mathcomp.algebra.ssralg]
+[ unitRingMixin of _ by <: ] (form_scope) [in mathcomp.algebra.ssralg]
+[ algMixin of _ by <: ] (form_scope) [in mathcomp.algebra.ssralg]
+[ comRingMixin of _ by <: ] (form_scope) [in mathcomp.algebra.ssralg]
+[ lalgMixin of _ by <: ] (form_scope) [in mathcomp.algebra.ssralg]
+[ lmodMixin of _ by <: ] (form_scope) [in mathcomp.algebra.ssralg]
+[ ringMixin of _ by <: ] (form_scope) [in mathcomp.algebra.ssralg]
+[ zmodMixin of _ by <: ] (form_scope) [in mathcomp.algebra.ssralg]
+[ unitAlgType _ of _ ] (form_scope) [in mathcomp.algebra.ssralg]
+[ unitRingType of _ ] (form_scope) [in mathcomp.algebra.ssralg]
+[ unitRingType of _ for _ ] (form_scope) [in mathcomp.algebra.ssralg]
+[ zmodType of _ ] (form_scope) [in mathcomp.algebra.ssralg]
+[ zmodType of _ for _ ] (form_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]
+[ char _ ] (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]
+- 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]
++%R (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]
+'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]
+1 (term_scope) [in mathcomp.algebra.ssralg]
+0 (term_scope) [in mathcomp.algebra.ssralg]
+_ %:T (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]
+_ ^- _ [in mathcomp.algebra.ssralg]
+_ / _ [in mathcomp.algebra.ssralg]
+_ ^-1 [in mathcomp.algebra.ssralg]
+*%R [in mathcomp.algebra.ssralg]
+*:%R [in mathcomp.algebra.ssralg]
+\prod_ ( _ <= _ < _ ) _ [in mathcomp.algebra.ssralg]
+\prod_ ( _ in _ ) _ [in mathcomp.algebra.ssralg]
+\prod_ ( _ | _ ) _ [in mathcomp.algebra.ssralg]
+\prod_ ( _ <- _ | _ ) _ [in mathcomp.algebra.ssralg]
+\sum_ ( _ in _ ) _ [in mathcomp.algebra.ssralg]
+\sum_ ( _ < _ ) _ [in mathcomp.algebra.ssralg]
+\sum_ ( _ <= _ < _ ) _ [in mathcomp.algebra.ssralg]
+\sum_ ( _ <- _ | _ ) _ [in mathcomp.algebra.ssralg]
| Global Index |
@@ -623,7 +623,7 @@
Z |
_ |
other |
-(23233 entries) |
+(23836 entries) |
| Notation Index |
@@ -655,14 +655,14 @@
Z |
_ |
other |
-(1373 entries) |
+(1409 entries) |
| Module Index |
A |
B |
C |
-D |
+D |
E |
F |
G |
@@ -687,7 +687,7 @@
Z |
_ |
other |
-(213 entries) |
+(221 entries) |
| Variable Index |
@@ -719,7 +719,7 @@
Z |
_ |
other |
-(3475 entries) |
+(3574 entries) |
| Library Index |
@@ -751,7 +751,7 @@
Z |
_ |
other |
-(89 entries) |
+(90 entries) |
| Lemma Index |
@@ -783,7 +783,7 @@
Z |
_ |
other |
-(11853 entries) |
+(12096 entries) |
| Constructor Index |
@@ -815,7 +815,7 @@
Z |
_ |
other |
-(359 entries) |
+(368 entries) |
| Axiom Index |
@@ -847,7 +847,7 @@
Z |
_ |
other |
-(47 entries) |
+(45 entries) |
| Inductive Index |
@@ -879,14 +879,14 @@
Z |
_ |
other |
-(103 entries) |
+(107 entries) |
| Projection Index |
A |
B |
C |
-D |
+D |
E |
F |
G |
@@ -911,7 +911,7 @@
Z |
_ |
other |
-(266 entries) |
+(273 entries) |
| Section Index |
@@ -943,7 +943,7 @@
Z |
_ |
other |
-(1118 entries) |
+(1140 entries) |
| Abbreviation Index |
@@ -975,7 +975,7 @@
Z |
_ |
other |
-(691 entries) |
+(728 entries) |
| Definition Index |
@@ -1007,14 +1007,14 @@
Z |
_ |
other |
-(3461 entries) |
+(3596 entries) |
| Record Index |
A |
B |
C |
-D |
+D |
E |
F |
G |
@@ -1039,7 +1039,7 @@
Z |
_ |
other |
-(185 entries) |
+(189 entries) |
diff --git a/docs/htmldoc/index_notation_H.html b/docs/htmldoc/index_notation_H.html
index c9bd28e..ecb788b 100644
--- a/docs/htmldoc/index_notation_H.html
+++ b/docs/htmldoc/index_notation_H.html
@@ -4,7 +4,7 @@
-mathcomp.ssreflect.tuple
+mathcomp.test_suite.hierarchy_test
@@ -47,7 +47,7 @@
Z |
_ |
other |
-(23233 entries) |
+(23836 entries) |
| Notation Index |
@@ -79,14 +79,14 @@
Z |
_ |
other |
-(1373 entries) |
+(1409 entries) |
| Module Index |
A |
B |
C |
-D |
+D |
E |
F |
G |
@@ -111,7 +111,7 @@
Z |
_ |
other |
-(213 entries) |
+(221 entries) |
| Variable Index |
@@ -143,7 +143,7 @@
Z |
_ |
other |
-(3475 entries) |
+(3574 entries) |
| Library Index |
@@ -175,7 +175,7 @@
Z |
_ |
other |
-(89 entries) |
+(90 entries) |
| Lemma Index |
@@ -207,7 +207,7 @@
Z |
_ |
other |
-(11853 entries) |
+(12096 entries) |
| Constructor Index |
@@ -239,7 +239,7 @@
Z |
_ |
other |
-(359 entries) |
+(368 entries) |
| Axiom Index |
@@ -271,7 +271,7 @@
Z |
_ |
other |
-(47 entries) |
+(45 entries) |
| Inductive Index |
@@ -303,14 +303,14 @@
Z |
_ |
other |
-(103 entries) |
+(107 entries) |
| Projection Index |
A |
B |
C |
-D |
+D |
E |
F |
G |
@@ -335,7 +335,7 @@
Z |
_ |
other |
-(266 entries) |
+(273 entries) |
| Section Index |
@@ -367,7 +367,7 @@
Z |
_ |
other |
-(1118 entries) |
+(1140 entries) |
| Abbreviation Index |
@@ -399,7 +399,7 @@
Z |
_ |
other |
-(691 entries) |
+(728 entries) |
| Definition Index |
@@ -431,14 +431,14 @@
Z |
_ |
other |
-(3461 entries) |
+(3596 entries) |
| Record Index |
A |
B |
C |
-D |
+D |
E |
F |
G |
@@ -463,7 +463,7 @@
Z |
_ |
other |
-(185 entries) |
+(189 entries) |
diff --git a/docs/htmldoc/index_notation_I.html b/docs/htmldoc/index_notation_I.html
index 68a2b58..c884f10 100644
--- a/docs/htmldoc/index_notation_I.html
+++ b/docs/htmldoc/index_notation_I.html
@@ -4,7 +4,7 @@
-mathcomp.ssreflect.tuple
+mathcomp.test_suite.hierarchy_test
@@ -47,7 +47,7 @@
Z |
_ |
other |
-(23233 entries) |
+(23836 entries) |
| Notation Index |
@@ -79,14 +79,14 @@
Z |
_ |
other |
-(1373 entries) |
+(1409 entries) |
| Module Index |
A |
B |
C |
-D |
+D |
E |
F |
G |
@@ -111,7 +111,7 @@
Z |
_ |
other |
-(213 entries) |
+(221 entries) |
| Variable Index |
@@ -143,7 +143,7 @@
Z |
_ |
other |
-(3475 entries) |
+(3574 entries) |
| Library Index |
@@ -175,7 +175,7 @@
Z |
_ |
other |
-(89 entries) |
+(90 entries) |
| Lemma Index |
@@ -207,7 +207,7 @@
Z |
_ |
other |
-(11853 entries) |
+(12096 entries) |
| Constructor Index |
@@ -239,7 +239,7 @@
Z |
_ |
other |
-(359 entries) |
+(368 entries) |
| Axiom Index |
@@ -271,7 +271,7 @@
Z |
_ |
other |
-(47 entries) |
+(45 entries) |
| Inductive Index |
@@ -303,14 +303,14 @@
Z |
_ |
other |
-(103 entries) |
+(107 entries) |
| Projection Index |
A |
B |
C |
-D |
+D |
E |
F |
G |
@@ -335,7 +335,7 @@
Z |
_ |
other |
-(266 entries) |
+(273 entries) |
| Section Index |
@@ -367,7 +367,7 @@
Z |
_ |
other |
-(1118 entries) |
+(1140 entries) |
| Abbreviation Index |
@@ -399,7 +399,7 @@
Z |
_ |
other |
-(691 entries) |
+(728 entries) |
| Definition Index |
@@ -431,14 +431,14 @@
Z |
_ |
other |
-(3461 entries) |
+(3596 entries) |
| Record Index |
A |
B |
C |
-D |
+D |
E |
F |
G |
@@ -463,493 +463,33 @@
Z |
_ |
other |
-(185 entries) |
+(189 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) |
-
-
-
+'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]
+_ * _ (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]
+
diff --git a/docs/htmldoc/index_notation_K.html b/docs/htmldoc/index_notation_K.html
index 527b237..799115a 100644
--- a/docs/htmldoc/index_notation_K.html
+++ b/docs/htmldoc/index_notation_K.html
@@ -4,7 +4,7 @@
-mathcomp.ssreflect.tuple
+mathcomp.test_suite.hierarchy_test
@@ -47,7 +47,7 @@
Z |
_ |
other |
-(23233 entries) |
+(23836 entries) |
| Notation Index |
@@ -79,14 +79,14 @@
Z |
_ |
other |
-(1373 entries) |
+(1409 entries) |
| Module Index |
A |
B |
C |
-D |
+D |
E |
F |
G |
@@ -111,7 +111,7 @@
Z |
_ |
other |
-(213 entries) |
+(221 entries) |
| Variable Index |
@@ -143,7 +143,7 @@
Z |
_ |
other |
-(3475 entries) |
+(3574 entries) |
| Library Index |
@@ -175,7 +175,7 @@
Z |
_ |
other |
-(89 entries) |
+(90 entries) |
| Lemma Index |
@@ -207,7 +207,7 @@
Z |
_ |
other |
-(11853 entries) |
+(12096 entries) |
| Constructor Index |
@@ -239,7 +239,7 @@
Z |
_ |
other |
-(359 entries) |
+(368 entries) |
| Axiom Index |
@@ -271,7 +271,7 @@
Z |
_ |
other |
-(47 entries) |
+(45 entries) |
| Inductive Index |
@@ -303,14 +303,14 @@
Z |
_ |
other |
-(103 entries) |
+(107 entries) |
| Projection Index |
A |
B |
C |
-D |
+D |
E |
F |
G |
@@ -335,7 +335,7 @@
Z |
_ |
other |
-(266 entries) |
+(273 entries) |
| Section Index |
@@ -367,7 +367,7 @@
Z |
_ |
other |
-(1118 entries) |
+(1140 entries) |
| Abbreviation Index |
@@ -399,7 +399,7 @@
Z |
_ |
other |
-(691 entries) |
+(728 entries) |
| Definition Index |
@@ -431,14 +431,14 @@
Z |
_ |
other |
-(3461 entries) |
+(3596 entries) |
| Record Index |
A |
B |
C |
-D |
+D |
E |
F |
G |
@@ -463,11 +463,11 @@
Z |
_ |
other |
-(185 entries) |
+(189 entries) |
K (notation)
-_ ^-1 (lrfun_scope) [in mathcomp.field.galois]
+_ ^-1 (lrfun_scope) [in mathcomp.field.galois]
diff --git a/docs/htmldoc/index_notation_N.html b/docs/htmldoc/index_notation_N.html
index c0cb513..45c9bab 100644
--- a/docs/htmldoc/index_notation_N.html
+++ b/docs/htmldoc/index_notation_N.html
@@ -4,7 +4,7 @@
-mathcomp.ssreflect.tuple
+mathcomp.test_suite.hierarchy_test
@@ -47,7 +47,7 @@
Z |
_ |
other |
-(23233 entries) |
+(23836 entries) |
| Notation Index |
@@ -79,14 +79,14 @@
Z |
_ |
other |
-(1373 entries) |
+(1409 entries) |
| Module Index |
A |
B |
C |
-D |
+D |
E |
F |
G |
@@ -111,7 +111,7 @@
Z |
_ |
other |
-(213 entries) |
+(221 entries) |
| Variable Index |
@@ -143,7 +143,7 @@
Z |
_ |
other |
-(3475 entries) |
+(3574 entries) |
| Library Index |
@@ -175,7 +175,7 @@
Z |
_ |
other |
-(89 entries) |
+(90 entries) |
| Lemma Index |
@@ -207,7 +207,7 @@
Z |
_ |
other |
-(11853 entries) |
+(12096 entries) |
| Constructor Index |
@@ -239,7 +239,7 @@
Z |
_ |
other |
-(359 entries) |
+(368 entries) |
| Axiom Index |
@@ -271,7 +271,7 @@
Z |
_ |
other |
-(47 entries) |
+(45 entries) |
| Inductive Index |
@@ -303,14 +303,14 @@
Z |
_ |
other |
-(103 entries) |
+(107 entries) |
| Projection Index |
A |
B |
C |
-D |
+D |
E |
F |
G |
@@ -335,7 +335,7 @@
Z |
_ |
other |
-(266 entries) |
+(273 entries) |
| Section Index |
@@ -367,7 +367,7 @@
Z |
_ |
other |
-(1118 entries) |
+(1140 entries) |
| Abbreviation Index |
@@ -399,7 +399,7 @@
Z |
_ |
other |
-(691 entries) |
+(728 entries) |
| Definition Index |
@@ -431,14 +431,14 @@
Z |
_ |
other |
-(3461 entries) |
+(3596 entries) |
| Record Index |
A |
B |
C |
-D |
+D |
E |
F |
G |
@@ -463,69 +463,75 @@
Z |
_ |
other |
-(185 entries) |
+(189 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]
+_ .*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]
+[ arg maxr_ ( _ > _ ) _ ] (form_scope) [in mathcomp.algebra.ssrnum]
+[ arg maxr_ ( _ > _ in _ ) _ ] (form_scope) [in mathcomp.algebra.ssrnum]
+[ arg maxr_ ( _ > _ | _ ) _ ] (form_scope) [in mathcomp.algebra.ssrnum]
+[ arg minr_ ( _ < _ ) _ ] (form_scope) [in mathcomp.algebra.ssrnum]
+[ arg minr_ ( _ < _ in _ ) _ ] (form_scope) [in mathcomp.algebra.ssrnum]
+[ arg minr_ ( _ < _ | _ ) _ ] (form_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 |
@@ -557,7 +563,7 @@
Z |
_ |
other |
-(23233 entries) |
+(23836 entries) |
| Notation Index |
@@ -589,14 +595,14 @@
Z |
_ |
other |
-(1373 entries) |
+(1409 entries) |
| Module Index |
A |
B |
C |
-D |
+D |
E |
F |
G |
@@ -621,7 +627,7 @@
Z |
_ |
other |
-(213 entries) |
+(221 entries) |
| Variable Index |
@@ -653,7 +659,7 @@
Z |
_ |
other |
-(3475 entries) |
+(3574 entries) |
| Library Index |
@@ -685,7 +691,7 @@
Z |
_ |
other |
-(89 entries) |
+(90 entries) |
| Lemma Index |
@@ -717,7 +723,7 @@
Z |
_ |
other |
-(11853 entries) |
+(12096 entries) |
| Constructor Index |
@@ -749,7 +755,7 @@
Z |
_ |
other |
-(359 entries) |
+(368 entries) |
| Axiom Index |
@@ -781,7 +787,7 @@
Z |
_ |
other |
-(47 entries) |
+(45 entries) |
| Inductive Index |
@@ -813,14 +819,14 @@
Z |
_ |
other |
-(103 entries) |
+(107 entries) |
| Projection Index |
A |
B |
C |
-D |
+D |
E |
F |
G |
@@ -845,7 +851,7 @@
Z |
_ |
other |
-(266 entries) |
+(273 entries) |
| Section Index |
@@ -877,7 +883,7 @@
Z |
_ |
other |
-(1118 entries) |
+(1140 entries) |
| Abbreviation Index |
@@ -909,7 +915,7 @@
Z |
_ |
other |
-(691 entries) |
+(728 entries) |
| Definition Index |
@@ -941,14 +947,14 @@
Z |
_ |
other |
-(3461 entries) |
+(3596 entries) |
| Record Index |
A |
B |
C |
-D |
+D |
E |
F |
G |
@@ -973,7 +979,7 @@
Z |
_ |
other |
-(185 entries) |
+(189 entries) |
diff --git a/docs/htmldoc/index_notation_O.html b/docs/htmldoc/index_notation_O.html
index c9bd28e..ecb788b 100644
--- a/docs/htmldoc/index_notation_O.html
+++ b/docs/htmldoc/index_notation_O.html
@@ -4,7 +4,7 @@
-mathcomp.ssreflect.tuple
+mathcomp.test_suite.hierarchy_test
@@ -47,7 +47,7 @@
Z |
_ |
other |
-(23233 entries) |
+(23836 entries) |
| Notation Index |
@@ -79,14 +79,14 @@
Z |
_ |
other |
-(1373 entries) |
+(1409 entries) |
| Module Index |
A |
B |
C |
-D |
+D |
E |
F |
G |
@@ -111,7 +111,7 @@
Z |
_ |
other |
-(213 entries) |
+(221 entries) |
| Variable Index |
@@ -143,7 +143,7 @@
Z |
_ |
other |
-(3475 entries) |
+(3574 entries) |
| Library Index |
@@ -175,7 +175,7 @@
Z |
_ |
other |
-(89 entries) |
+(90 entries) |
| Lemma Index |
@@ -207,7 +207,7 @@
Z |
_ |
other |
-(11853 entries) |
+(12096 entries) |
| Constructor Index |
@@ -239,7 +239,7 @@
Z |
_ |
other |
-(359 entries) |
+(368 entries) |
| Axiom Index |
@@ -271,7 +271,7 @@
Z |
_ |
other |
-(47 entries) |
+(45 entries) |
| Inductive Index |
@@ -303,14 +303,14 @@
Z |
_ |
other |
-(103 entries) |
+(107 entries) |
| Projection Index |
A |
B |
C |
-D |
+D |
E |
F |
G |
@@ -335,7 +335,7 @@
Z |
_ |
other |
-(266 entries) |
+(273 entries) |
| Section Index |
@@ -367,7 +367,7 @@
Z |
_ |
other |
-(1118 entries) |
+(1140 entries) |
| Abbreviation Index |
@@ -399,7 +399,7 @@
Z |
_ |
other |
-(691 entries) |
+(728 entries) |
| Definition Index |
@@ -431,14 +431,14 @@
Z |
_ |
other |
-(3461 entries) |
+(3596 entries) |
| Record Index |
A |
B |
C |
-D |
+D |
E |
F |
G |
@@ -463,7 +463,7 @@
Z |
_ |
other |
-(185 entries) |
+(189 entries) |
diff --git a/docs/htmldoc/index_notation_P.html b/docs/htmldoc/index_notation_P.html
index 1152843..3e21d07 100644
--- a/docs/htmldoc/index_notation_P.html
+++ b/docs/htmldoc/index_notation_P.html
@@ -4,7 +4,7 @@
-mathcomp.ssreflect.tuple
+mathcomp.test_suite.hierarchy_test
@@ -47,7 +47,7 @@
Z |
_ |
other |
-(23233 entries) |
+(23836 entries) |
| Notation Index |
@@ -79,14 +79,14 @@
Z |
_ |
other |
-(1373 entries) |
+(1409 entries) |
| Module Index |
A |
B |
C |
-D |
+D |
E |
F |
G |
@@ -111,7 +111,7 @@
Z |
_ |
other |
-(213 entries) |
+(221 entries) |
| Variable Index |
@@ -143,7 +143,7 @@
Z |
_ |
other |
-(3475 entries) |
+(3574 entries) |
| Library Index |
@@ -175,7 +175,7 @@
Z |
_ |
other |
-(89 entries) |
+(90 entries) |
| Lemma Index |
@@ -207,7 +207,7 @@
Z |
_ |
other |
-(11853 entries) |
+(12096 entries) |
| Constructor Index |
@@ -239,7 +239,7 @@
Z |
_ |
other |
-(359 entries) |
+(368 entries) |
| Axiom Index |
@@ -271,7 +271,7 @@
Z |
_ |
other |
-(47 entries) |
+(45 entries) |
| Inductive Index |
@@ -303,14 +303,14 @@
Z |
_ |
other |
-(103 entries) |
+(107 entries) |
| Projection Index |
A |
B |
C |
-D |
+D |
E |
F |
G |
@@ -335,7 +335,7 @@
Z |
_ |
other |
-(266 entries) |
+(273 entries) |
| Section Index |
@@ -367,7 +367,7 @@
Z |
_ |
other |
-(1118 entries) |
+(1140 entries) |
| Abbreviation Index |
@@ -399,7 +399,7 @@
Z |
_ |
other |
-(691 entries) |
+(728 entries) |
| Definition Index |
@@ -431,14 +431,14 @@
Z |
_ |
other |
-(3461 entries) |
+(3596 entries) |
| Record Index |
A |
B |
C |
-D |
+D |
E |
F |
G |
@@ -463,29 +463,30 @@
Z |
_ |
other |
-(185 entries) |
+(189 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]
+_ ^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]
+_ ^? _ :: _ (nat_scope) [in mathcomp.ssreflect.prime]
+[ rec _ , _ , _ , _ , _ , _ ] [in mathcomp.ssreflect.prime]
diff --git a/docs/htmldoc/index_notation_U.html b/docs/htmldoc/index_notation_U.html
index 5db79b0..28fe348 100644
--- a/docs/htmldoc/index_notation_U.html
+++ b/docs/htmldoc/index_notation_U.html
@@ -4,7 +4,7 @@
-mathcomp.ssreflect.tuple
+mathcomp.test_suite.hierarchy_test
@@ -47,7 +47,7 @@
Z |
_ |
other |
-(23233 entries) |
+(23836 entries) |
| Notation Index |
@@ -79,14 +79,14 @@
Z |
_ |
other |
-(1373 entries) |
+(1409 entries) |
| Module Index |
A |
B |
C |
-D |
+D |
E |
F |
G |
@@ -111,7 +111,7 @@
Z |
_ |
other |
-(213 entries) |
+(221 entries) |
| Variable Index |
@@ -143,7 +143,7 @@
Z |
_ |
other |
-(3475 entries) |
+(3574 entries) |
| Library Index |
@@ -175,7 +175,7 @@
Z |
_ |
other |
-(89 entries) |
+(90 entries) |
| Lemma Index |
@@ -207,7 +207,7 @@
Z |
_ |
other |
-(11853 entries) |
+(12096 entries) |
| Constructor Index |
@@ -239,7 +239,7 @@
Z |
_ |
other |
-(359 entries) |
+(368 entries) |
| Axiom Index |
@@ -271,7 +271,7 @@
Z |
_ |
other |
-(47 entries) |
+(45 entries) |
| Inductive Index |
@@ -303,14 +303,14 @@
Z |
_ |
other |
-(103 entries) |
+(107 entries) |
| Projection Index |
A |
B |
C |
-D |
+D |
E |
F |
G |
@@ -335,7 +335,7 @@
Z |
_ |
other |
-(266 entries) |
+(273 entries) |
| Section Index |
@@ -367,7 +367,7 @@
Z |
_ |
other |
-(1118 entries) |
+(1140 entries) |
| Abbreviation Index |
@@ -399,7 +399,7 @@
Z |
_ |
other |
-(691 entries) |
+(728 entries) |
| Definition Index |
@@ -431,14 +431,14 @@
Z |
_ |
other |
-(3461 entries) |
+(3596 entries) |
| Record Index |
A |
B |
C |
-D |
+D |
E |
F |
G |
@@ -463,12 +463,12 @@
Z |
_ |
other |
-(185 entries) |
+(189 entries) |
U (notation)
-_ .-primitive_root (unity_root_scope) [in mathcomp.algebra.poly]
-_ .-unity_root (unity_root_scope) [in mathcomp.algebra.poly]
+_ .-primitive_root (unity_root_scope) [in mathcomp.algebra.poly]
+_ .-unity_root (unity_root_scope) [in mathcomp.algebra.poly]
diff --git a/docs/htmldoc/index_notation_X.html b/docs/htmldoc/index_notation_X.html
index c9bd28e..ecb788b 100644
--- a/docs/htmldoc/index_notation_X.html
+++ b/docs/htmldoc/index_notation_X.html
@@ -4,7 +4,7 @@
-mathcomp.ssreflect.tuple
+mathcomp.test_suite.hierarchy_test
@@ -47,7 +47,7 @@
Z |
_ |
other |
-(23233 entries) |
+(23836 entries) |
| Notation Index |
@@ -79,14 +79,14 @@
Z |
_ |
other |
-(1373 entries) |
+(1409 entries) |
| Module Index |
A |
B |
C |
-D |
+D |
E |
F |
G |
@@ -111,7 +111,7 @@
Z |
_ |
other |
-(213 entries) |
+(221 entries) |
| Variable Index |
@@ -143,7 +143,7 @@
Z |
_ |
other |
-(3475 entries) |
+(3574 entries) |
| Library Index |
@@ -175,7 +175,7 @@
Z |
_ |
other |
-(89 entries) |
+(90 entries) |
| Lemma Index |
@@ -207,7 +207,7 @@
Z |
_ |
other |
-(11853 entries) |
+(12096 entries) |
| Constructor Index |
@@ -239,7 +239,7 @@
Z |
_ |
other |
-(359 entries) |
+(368 entries) |
| Axiom Index |
@@ -271,7 +271,7 @@
Z |
_ |
other |
-(47 entries) |
+(45 entries) |
| Inductive Index |
@@ -303,14 +303,14 @@
Z |
_ |
other |
-(103 entries) |
+(107 entries) |
| Projection Index |
A |
B |
C |
-D |
+D |
E |
F |
G |
@@ -335,7 +335,7 @@
Z |
_ |
other |
-(266 entries) |
+(273 entries) |
| Section Index |
@@ -367,7 +367,7 @@
Z |
_ |
other |
-(1118 entries) |
+(1140 entries) |
| Abbreviation Index |
@@ -399,7 +399,7 @@
Z |
_ |
other |
-(691 entries) |
+(728 entries) |
| Definition Index |
@@ -431,14 +431,14 @@
Z |
_ |
other |
-(3461 entries) |
+(3596 entries) |
| Record Index |
A |
B |
C |
-D |
+D |
E |
F |
G |
@@ -463,7 +463,7 @@
Z |
_ |
other |
-(185 entries) |
+(189 entries) |
diff --git a/docs/htmldoc/index_notation_Y.html b/docs/htmldoc/index_notation_Y.html
index c9bd28e..ecb788b 100644
--- a/docs/htmldoc/index_notation_Y.html
+++ b/docs/htmldoc/index_notation_Y.html
@@ -4,7 +4,7 @@
-mathcomp.ssreflect.tuple
+mathcomp.test_suite.hierarchy_test
@@ -47,7 +47,7 @@
Z |
_ |
other |
-(23233 entries) |
+(23836 entries) |
| Notation Index |
@@ -79,14 +79,14 @@
Z |
_ |
other |
-(1373 entries) |
+(1409 entries) |
| Module Index |
A |
B |
C |
-D |
+D |
E |
F |
G |
@@ -111,7 +111,7 @@
Z |
_ |
other |
-(213 entries) |
+(221 entries) |
| Variable Index |
@@ -143,7 +143,7 @@
Z |
_ |
other |
-(3475 entries) |
+(3574 entries) |
| Library Index |
@@ -175,7 +175,7 @@
Z |
_ |
other |
-(89 entries) |
+(90 entries) |
| Lemma Index |
@@ -207,7 +207,7 @@
Z |
_ |
other |
-(11853 entries) |
+(12096 entries) |
| Constructor Index |
@@ -239,7 +239,7 @@
Z |
_ |
other |
-(359 entries) |
+(368 entries) |
| Axiom Index |
@@ -271,7 +271,7 @@
Z |
_ |
other |
-(47 entries) |
+(45 entries) |
| Inductive Index |
@@ -303,14 +303,14 @@
Z |
_ |
other |
-(103 entries) |
+(107 entries) |
| Projection Index |
A |
B |
C |
-D |
+D |
E |
F |
G |
@@ -335,7 +335,7 @@
Z |
_ |
other |
-(266 entries) |
+(273 entries) |
| Section Index |
@@ -367,7 +367,7 @@
Z |
_ |
other |
-(1118 entries) |
+(1140 entries) |
| Abbreviation Index |
@@ -399,7 +399,7 @@
Z |
_ |
other |
-(691 entries) |
+(728 entries) |
| Definition Index |
@@ -431,14 +431,14 @@
Z |
_ |
other |
-(3461 entries) |
+(3596 entries) |
| Record Index |
A |
B |
C |
-D |
+D |
E |
F |
G |
@@ -463,7 +463,7 @@
Z |
_ |
other |
-(185 entries) |
+(189 entries) |
diff --git a/docs/htmldoc/index_notation_Z.html b/docs/htmldoc/index_notation_Z.html
index cee9742..a82cb63 100644
--- a/docs/htmldoc/index_notation_Z.html
+++ b/docs/htmldoc/index_notation_Z.html
@@ -4,7 +4,7 @@
-mathcomp.ssreflect.tuple
+mathcomp.test_suite.hierarchy_test
@@ -47,7 +47,7 @@
Z |
_ |
other |
-(23233 entries) |
+(23836 entries) |
| Notation Index |
@@ -79,14 +79,14 @@
Z |
_ |
other |
-(1373 entries) |
+(1409 entries) |
| Module Index |
A |
B |
C |
-D |
+D |
E |
F |
G |
@@ -111,7 +111,7 @@
Z |
_ |
other |
-(213 entries) |
+(221 entries) |
| Variable Index |
@@ -143,7 +143,7 @@
Z |
_ |
other |
-(3475 entries) |
+(3574 entries) |
| Library Index |
@@ -175,7 +175,7 @@
Z |
_ |
other |
-(89 entries) |
+(90 entries) |
| Lemma Index |
@@ -207,7 +207,7 @@
Z |
_ |
other |
-(11853 entries) |
+(12096 entries) |
| Constructor Index |
@@ -239,7 +239,7 @@
Z |
_ |
other |
-(359 entries) |
+(368 entries) |
| Axiom Index |
@@ -271,7 +271,7 @@
Z |
_ |
other |
-(47 entries) |
+(45 entries) |
| Inductive Index |
@@ -303,14 +303,14 @@
Z |
_ |
other |
-(103 entries) |
+(107 entries) |
| Projection Index |
A |
B |
C |
-D |
+D |
E |
F |
G |
@@ -335,7 +335,7 @@
Z |
_ |
other |
-(266 entries) |
+(273 entries) |
| Section Index |
@@ -367,7 +367,7 @@
Z |
_ |
other |
-(1118 entries) |
+(1140 entries) |
| Abbreviation Index |
@@ -399,7 +399,7 @@
Z |
_ |
other |
-(691 entries) |
+(728 entries) |
| Definition Index |
@@ -431,14 +431,14 @@
Z |
_ |
other |
-(3461 entries) |
+(3596 entries) |
| Record Index |
A |
B |
C |
-D |
+D |
E |
F |
G |
@@ -463,11 +463,11 @@
Z |
_ |
other |
-(185 entries) |
+(189 entries) |
Z (notation)
-_ ^z (type_scope) [in mathcomp.algebra.ssrint]
+_ ^z (type_scope) [in mathcomp.algebra.ssrint]
--
cgit v1.2.3