Top

Notations

Files

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

Definitions

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

Lemmas

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

Abbreviations

A

B

C

D

E

F

G

H

I

J

K

L

M

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

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

_

Notations

no scope

'1_ [not, in mathcomp.group_representation.classfun] (no scope)
'Alt_T [not, in mathcomp.solvable.alt] (no scope)
'Chi_ [not, in mathcomp.group_representation.character] (no scope)
'I_ [not, in mathcomp.boot.fintype] (no scope)
'Phi_ [not, in mathcomp.field.cyclotomic] (no scope)
'R_ [not, in mathcomp.group_representation.character] (no scope)
'S_ [not, in mathcomp.finite_group.perm] (no scope)
'Sym_T [not, in mathcomp.solvable.alt] (no scope)
'T[ ] [not, in mathcomp.algebra.tensor] (no scope)
'T[ ] [not, in mathcomp.algebra.tensor] (no scope)
'X [not, in mathcomp.algebra.poly] (no scope)
'X^ [not, in mathcomp.algebra.poly] (no scope)
'all_ [not, in mathcomp.boot.seq] (no scope)
'e_ [not, in mathcomp.group_representation.character] (no scope)
'exists_ [not, in mathcomp.boot.fintype] (no scope)
'exists_in_ [not, in mathcomp.boot.fintype] (no scope)
'forall_ [not, in mathcomp.boot.fintype] (no scope)
'forall_in_ [not, in mathcomp.boot.fintype] (no scope)
'has_ [not, in mathcomp.boot.seq] (no scope)
'if then else [not, in mathcomp.field.closed_field] (no scope)
'let <- ; [not, in mathcomp.field.closed_field] (no scope)
'nX^ [not, in mathcomp.algebra.qpoly] (no scope)
'n_ [not, in mathcomp.group_representation.character] (no scope)
'qX [not, in mathcomp.algebra.qpoly] (no scope)
( ) [not, in mathcomp.finite_group.presentation] (no scope)
*%M [not, in mathcomp.boot.bigop] (no scope)
*%M [not, in mathcomp.boot.bigop] (no scope)
*%M [not, in mathcomp.boot.bigop] (no scope)
*%N [not, in mathcomp.boot.bigop] (no scope)
+%M [not, in mathcomp.boot.bigop] (no scope)
+%N [not, in mathcomp.boot.bigop] (no scope)
0 [not, in mathcomp.boot.bigop] (no scope)
1 [not, in mathcomp.finite_group.presentation] (no scope)
1 [not, in mathcomp.finite_group.fingroup] (no scope)
1 [not, in mathcomp.boot.bigop] (no scope)
1 [not, in mathcomp.boot.bigop] (no scope)
1 [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (no scope)
<< ; >> [not, in mathcomp.field.algebraics_fundamentals] (no scope)
@ ffun_on [not, in mathcomp.boot.finfun] (no scope)
[ cmp0 of ] [not, in mathcomp.algebra.interval_inference] (no scope)
[ ge0 of ] [not, in mathcomp.algebra.interval_inference] (no scope)
[ gt0 of ] [not, in mathcomp.algebra.interval_inference] (no scope)
[ le0 of ] [not, in mathcomp.algebra.interval_inference] (no scope)
[ lt0 of ] [not, in mathcomp.algebra.interval_inference] (no scope)
[ neq0 of ] [not, in mathcomp.algebra.interval_inference] (no scope)
[ rec , , , , , ] [not, in mathcomp.boot.prime] (no scope)
[ rec , , ] [not, in mathcomp.boot.choice] (no scope)
[ rec , ] [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (no scope)
[ seq : <- | & ] [not, in mathcomp.boot.seq] (no scope)
[ seq : <- | ] [not, in mathcomp.boot.seq] (no scope)
[ ~ , , .. , ] [not, in mathcomp.finite_group.presentation] (no scope)
[ : | ] [not, in mathcomp.boot.fintype] (no scope)
[ | ] [not, in mathcomp.boot.fintype] (no scope)
\bot [not, in mathcomp.order.order] (no scope)
\bot [not, in mathcomp.order.order] (no scope)
\bot [not, in mathcomp.order.order] (no scope)
\bot [not, in mathcomp.order.order] (no scope)
\bot [not, in mathcomp.order.order] (no scope)
\d_ [not, in mathcomp.algebra.fraction] (no scope)
\mpi [not, in mathcomp.boot.generic_quotient] (no scope)
\n_ [not, in mathcomp.algebra.fraction] (no scope)
\pi [not, in mathcomp.boot.generic_quotient] (no scope)
\poly_ ( < ) [not, in mathcomp.algebra.poly] (no scope)
\prod_ ( <- | ) [not, in mathcomp.boot.monoid] (no scope)
\prod_ ( <- | ) [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (no scope)
\prod_ ( <= < ) [not, in mathcomp.boot.monoid] (no scope)
\prod_ ( <= < ) [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (no scope)
\prod_ ( in ) [not, in mathcomp.boot.monoid] (no scope)
\prod_ ( in ) [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (no scope)
\prod_ ( | ) [not, in mathcomp.boot.monoid] (no scope)
\prod_ ( | ) [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (no scope)
\sum_ ( < ) [not, in mathcomp.boot.nmodule] (no scope)
\sum_ ( <- | ) [not, in mathcomp.boot.nmodule] (no scope)
\sum_ ( <= < ) [not, in mathcomp.boot.nmodule] (no scope)
\sum_ ( in ) [not, in mathcomp.boot.nmodule] (no scope)
\top [not, in mathcomp.order.order] (no scope)
\top [not, in mathcomp.order.order] (no scope)
\top [not, in mathcomp.order.order] (no scope)
\top [not, in mathcomp.order.order] (no scope)
\top [not, in mathcomp.order.order] (no scope)
\val [not, in mathcomp.boot.eqtype] (no scope)
\val [not, in mathcomp.boot.eqtype] (no scope)
{ fraction } [not, in mathcomp.algebra.fraction] (no scope)
{ poly %/ with } [not, in mathcomp.field.qfpoly] (no scope)
{ subset } [not, in mathcomp.order.preorder] (no scope)
{ subset } [not, in mathcomp.order.order] (no scope)
{subset <= } [not, in mathcomp.order.order] (no scope)
[not, in mathcomp.finite_group.presentation] (no scope)
%:F [not, in mathcomp.algebra.fraction] (no scope)
%:F [not, in mathcomp.algebra.fraction] (no scope)
%:P [not, in mathcomp.algebra.poly] (no scope)
%:R [not, in mathcomp.solvable.extremal] (no scope)
%:R [not, in mathcomp.solvable.extraspecial] (no scope)
%| [not, in mathcomp.field.finfield] (no scope)
* [not, in mathcomp.finite_group.presentation] (no scope)
* [not, in mathcomp.finite_group.fingroup] (no scope)
* [not, in mathcomp.boot.bigop] (no scope)
* [not, in mathcomp.boot.bigop] (no scope)
* [not, in mathcomp.boot.bigop] (no scope)
* [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (no scope)
*:l [not, in mathcomp.algebra.vector] (no scope)
*F0: [not, in mathcomp.field.fieldext] (no scope)
*F: [not, in mathcomp.field.fieldext] (no scope)
*p': [not, in mathcomp.field.finfield] (no scope)
+ [not, in mathcomp.boot.bigop] (no scope)
, , .. , [not, in mathcomp.finite_group.presentation] (no scope)
->_ [not, in mathcomp.field.closed_field] (no scope)
.-root [not, in mathcomp.algebra.numeric_hierarchy.numfield] (no scope)
.-sesqui [not, in mathcomp.algebra.sesquilinear] (no scope)
.-tuplelexi [not, in mathcomp.order.preorder] (no scope)
.-tupleprod [not, in mathcomp.order.preorder] (no scope)
.[ AC ] [not, in mathcomp.boot.ssrAC] (no scope)
.[ ACl ] [not, in mathcomp.boot.ssrAC] (no scope)
.[ ACof ] [not, in mathcomp.boot.ssrAC] (no scope)
/ [not, in mathcomp.algebra.algebraic_hierarchy.divalg] (no scope)
: [not, in mathcomp.finite_group.presentation] (no scope)
= [not, in mathcomp.finite_group.presentation] (no scope)
= = [not, in mathcomp.finite_group.presentation] (no scope)
\char [not, in mathcomp.finite_group.automorphism] (no scope)
\in [not, in mathcomp.algebra.mxalgebra] (no scope)
\isog [not, in mathcomp.finite_group.morphism] (no scope)
\isog [not, in mathcomp.finite_group.morphism] (no scope)
^ [not, in mathcomp.finite_group.presentation] (no scope)
^ [not, in mathcomp.algebra.matrix] (no scope)
^* [not, in mathcomp.boot.fintype] (no scope)
^+ [not, in mathcomp.finite_group.presentation] (no scope)
^- [not, in mathcomp.finite_group.presentation] (no scope)
^- [not, in mathcomp.algebra.algebraic_hierarchy.divalg] (no scope)
^-1 [not, in mathcomp.finite_group.presentation] (no scope)
^-1 [not, in mathcomp.finite_group.fingroup] (no scope)
^-1 [not, in mathcomp.algebra.algebraic_hierarchy.divalg] (no scope)
^^ [not, in mathcomp.field.algC] (no scope)
^` () [not, in mathcomp.algebra.poly] (no scope)
^f [not, in mathcomp.algebra.ssrint] (no scope)
^f [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (no scope)
^f [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (no scope)
^u [not, in mathcomp.group_representation.vcharacter] (no scope)
^u [not, in mathcomp.group_representation.classfun] (no scope)
~_ [not, in mathcomp.algebra.mxpoly] (no scope)
~_{in } { in } [not, in mathcomp.algebra.mxpoly] (no scope)
~_{in } [not, in mathcomp.algebra.mxpoly] (no scope)

AC_scope

* [not, in mathcomp.boot.ssrAC] (in AC_scope)

C_expanded_scope

%| [not, in mathcomp.field.algC] (in C_expanded_scope)

C_scope

#[ ] [not, in mathcomp.field.algnum] (in C_scope)
!= %[mod ] [not, in mathcomp.field.algC] (in C_scope)
%| [not, in mathcomp.field.algC] (in C_scope)
== %[mod ] [not, in mathcomp.field.algC] (in C_scope)

Group_scope

'Alt_ [not, in mathcomp.solvable.alt] (in Group_scope)
'C ( ) [not, in mathcomp.finite_group.fingroup] (in Group_scope)
'C ( | ) [not, in mathcomp.finite_group.action] (in Group_scope)
'C [ ] [not, in mathcomp.finite_group.fingroup] (in Group_scope)
'C [ | ] [not, in mathcomp.finite_group.action] (in Group_scope)
'C_ ( | ) ( ) [not, in mathcomp.finite_group.action] (in Group_scope)
'C_ ( | ) [ ] [not, in mathcomp.finite_group.action] (in Group_scope)
'C_ ( ) ( ) [not, in mathcomp.finite_group.fingroup] (in Group_scope)
'C_ ( ) ( | ) [not, in mathcomp.finite_group.action] (in Group_scope)
'C_ ( ) [ ] [not, in mathcomp.finite_group.fingroup] (in Group_scope)
'C_ ( ) [ | ] [not, in mathcomp.finite_group.action] (in Group_scope)
'C_ ( | ) ( ) [not, in mathcomp.finite_group.action] (in Group_scope)
'C_ ( | ) [ ] [not, in mathcomp.finite_group.action] (in Group_scope)
'C_ ( ) [not, in mathcomp.finite_group.fingroup] (in Group_scope)
'C_ ( | ) [not, in mathcomp.finite_group.action] (in Group_scope)
'C_ [ ] [not, in mathcomp.finite_group.fingroup] (in Group_scope)
'C_ [ | ] [not, in mathcomp.finite_group.action] (in Group_scope)
'D^ [not, in mathcomp.solvable.extraspecial] (in Group_scope)
'D^ * Q [not, in mathcomp.solvable.extraspecial] (in Group_scope)
'D_ [not, in mathcomp.solvable.extremal] (in Group_scope)
'F ( ) [not, in mathcomp.solvable.maximal] (in Group_scope)
'GL_ ( ) [not, in mathcomp.algebra.matrix] (in Group_scope)
'GL_ [ ] [not, in mathcomp.algebra.matrix] (in Group_scope)
'Gal ( / ) [not, in mathcomp.field.galois] (in Group_scope)
'Gal ( / ) [not, in mathcomp.field.galois] (in Group_scope)
'I[ ] [not, in mathcomp.group_representation.inertia] (in Group_scope)
'I[ ] [not, in mathcomp.group_representation.inertia] (in Group_scope)
'I_ [ ] [not, in mathcomp.group_representation.inertia] (in Group_scope)
'I_ [ ] [not, in mathcomp.group_representation.inertia] (in Group_scope)
'L_ ( ) [not, in mathcomp.solvable.nilpotent] (in Group_scope)
'Mho^ ( ) [not, in mathcomp.solvable.abelian] (in Group_scope)
'Mod_ [not, in mathcomp.solvable.extremal] (in Group_scope)
'N ( ) [not, in mathcomp.finite_group.fingroup] (in Group_scope)
'N ( | ) [not, in mathcomp.finite_group.action] (in Group_scope)
'N_ ( ) [not, in mathcomp.finite_group.fingroup] (in Group_scope)
'N_ ( | ) [not, in mathcomp.finite_group.action] (in Group_scope)
'O_ ( ) [not, in mathcomp.solvable.pgroup] (in Group_scope)
'O_{ , .. , } ( ) [not, in mathcomp.solvable.pgroup] (in Group_scope)
'Ohm_ ( ) [not, in mathcomp.solvable.abelian] (in Group_scope)
'Phi ( ) [not, in mathcomp.solvable.maximal] (in Group_scope)
'Q_ [not, in mathcomp.solvable.extremal] (in Group_scope)
'SD_ [not, in mathcomp.solvable.extremal] (in Group_scope)
'Sym_ [not, in mathcomp.solvable.alt] (in Group_scope)
'Z ( ) [not, in mathcomp.solvable.center] (in Group_scope)
'Z_ ( ) [not, in mathcomp.solvable.nilpotent] (in Group_scope)
'ker [not, in mathcomp.finite_group.morphism] (in Group_scope)
'ker_ [not, in mathcomp.finite_group.morphism] (in Group_scope)
1 [not, in mathcomp.finite_group.fingroup] (in Group_scope)
<< >> [not, in mathcomp.finite_group.fingroup] (in Group_scope)
<[ ] > [not, in mathcomp.finite_group.fingroup] (in Group_scope)
[ 1 ] [not, in mathcomp.finite_group.fingroup] (in Group_scope)
[ Aut ] [not, in mathcomp.finite_group.automorphism] (in Group_scope)
[ set : ] [not, in mathcomp.finite_group.fingroup] (in Group_scope)
[ subg ] [not, in mathcomp.finite_group.fingroup] (in Group_scope)
[ ~: , , .. , ] [not, in mathcomp.finite_group.fingroup] (in Group_scope)
\prod_ ( : ) [not, in mathcomp.finite_group.fingroup] (in Group_scope)
\prod_ ( : | ) [not, in mathcomp.finite_group.fingroup] (in Group_scope)
\prod_ ( < ) [not, in mathcomp.finite_group.fingroup] (in Group_scope)
\prod_ ( < | ) [not, in mathcomp.finite_group.fingroup] (in Group_scope)
\prod_ ( <- ) [not, in mathcomp.finite_group.fingroup] (in Group_scope)
\prod_ ( <- | ) [not, in mathcomp.finite_group.fingroup] (in Group_scope)
\prod_ ( <= < ) [not, in mathcomp.finite_group.fingroup] (in Group_scope)
\prod_ ( <= < | ) [not, in mathcomp.finite_group.fingroup] (in Group_scope)
\prod_ ( in ) [not, in mathcomp.finite_group.fingroup] (in Group_scope)
\prod_ ( in | ) [not, in mathcomp.finite_group.fingroup] (in Group_scope)
\prod_ ( | ) [not, in mathcomp.finite_group.fingroup] (in Group_scope)
\prod_ [not, in mathcomp.finite_group.fingroup] (in Group_scope)
* [not, in mathcomp.finite_group.fingroup] (in Group_scope)
/ [not, in mathcomp.finite_group.quotient] (in Group_scope)
/ [not, in mathcomp.finite_group.quotient] (in Group_scope)
:&: [not, in mathcomp.finite_group.fingroup] (in Group_scope)
:^ [not, in mathcomp.finite_group.fingroup] (in Group_scope)
<*> [not, in mathcomp.finite_group.fingroup] (in Group_scope)
@* [not, in mathcomp.finite_group.morphism] (in Group_scope)
@*^-1 [not, in mathcomp.finite_group.morphism] (in Group_scope)
@: [not, in mathcomp.finite_group.morphism] (in Group_scope)
^` ( ) [not, in mathcomp.solvable.commutator] (in Group_scope)
^{1+2* } [not, in mathcomp.solvable.extraspecial] (in Group_scope)
^{1+2} [not, in mathcomp.solvable.extraspecial] (in Group_scope)

abelem_scope

'M ( ) [not, in mathcomp.group_representation.mxabelem] (in abelem_scope)
'M[ ] ( ) [not, in mathcomp.group_representation.mxabelem] (in abelem_scope)
'dim [not, in mathcomp.group_representation.mxabelem] (in abelem_scope)
'rV ( ) [not, in mathcomp.group_representation.mxabelem] (in abelem_scope)
'rV[ ] ( ) [not, in mathcomp.group_representation.mxabelem] (in abelem_scope)

action_scope

'Cl [not, in mathcomp.group_representation.mxrepresentation] (in action_scope)
'Cl [not, in mathcomp.group_representation.mxrepresentation] (in action_scope)
'J [not, in mathcomp.finite_group.action] (in action_scope)
'JG [not, in mathcomp.finite_group.action] (in action_scope)
'Js [not, in mathcomp.finite_group.action] (in action_scope)
'M [not, in mathcomp.solvable.finmodule] (in action_scope)
'M [not, in mathcomp.solvable.finmodule] (in action_scope)
'MR [not, in mathcomp.group_representation.mxabelem] (in action_scope)
'P [not, in mathcomp.finite_group.action] (in action_scope)
'Q [not, in mathcomp.finite_group.action] (in action_scope)
'R [not, in mathcomp.finite_group.action] (in action_scope)
'Rs [not, in mathcomp.finite_group.action] (in action_scope)
'U [not, in mathcomp.algebra.finalg] (in action_scope)
'Zm [not, in mathcomp.group_representation.mxabelem] (in action_scope)
'Zm [not, in mathcomp.group_representation.mxabelem] (in action_scope)
<< >> [not, in mathcomp.finite_group.action] (in action_scope)
<[ ] > [not, in mathcomp.finite_group.action] (in action_scope)
<[nRA]> [not, in mathcomp.finite_group.action] (in action_scope)
[ Aut ] [not, in mathcomp.finite_group.action] (in action_scope)
%% [not, in mathcomp.finite_group.action] (in action_scope)
* [not, in mathcomp.solvable.primitive_action] (in action_scope)
/ [not, in mathcomp.finite_group.action] (in action_scope)
\ [not, in mathcomp.finite_group.action] (in action_scope)
\o [not, in mathcomp.finite_group.action] (in action_scope)
^* [not, in mathcomp.finite_group.action] (in action_scope)
^? [not, in mathcomp.finite_group.action] (in action_scope)

algC_expanded_scope

%| [not, in mathcomp.field.algnum] (in algC_expanded_scope)

algC_scope

!= %[mod ] [not, in mathcomp.field.algnum] (in algC_scope)
%| [not, in mathcomp.field.algnum] (in algC_scope)
== %[mod ] [not, in mathcomp.field.algnum] (in algC_scope)

aspace_scope

'C ( ) [not, in mathcomp.field.falgebra] (in aspace_scope)
'C [ ] [not, in mathcomp.field.falgebra] (in aspace_scope)
'C_ ( ) ( ) [not, in mathcomp.field.fieldext] (in aspace_scope)
'C_ ( ) [ ] [not, in mathcomp.field.fieldext] (in aspace_scope)
'C_ ( ) [not, in mathcomp.field.fieldext] (in aspace_scope)
'C_ [ ] [not, in mathcomp.field.fieldext] (in aspace_scope)
'Z ( ) [not, in mathcomp.field.falgebra] (in aspace_scope)
1 [not, in mathcomp.field.falgebra] (in aspace_scope)
<< & >> [not, in mathcomp.field.falgebra] (in aspace_scope)
<< ; >> [not, in mathcomp.field.falgebra] (in aspace_scope)
<< >> [not, in mathcomp.field.falgebra] (in aspace_scope)
{ : } [not, in mathcomp.field.falgebra] (in aspace_scope)
* [not, in mathcomp.field.fieldext] (in aspace_scope)
:&: [not, in mathcomp.field.fieldext] (in aspace_scope)
@: [not, in mathcomp.field.fieldext] (in aspace_scope)

big_scope

\big [ / ]_ ( : ) [not, in mathcomp.boot.bigop] (in big_scope)
\big [ / ]_ ( : | ) [not, in mathcomp.boot.bigop] (in big_scope)
\big [ / ]_ ( < ) [not, in mathcomp.boot.bigop] (in big_scope)
\big [ / ]_ ( < | ) [not, in mathcomp.boot.bigop] (in big_scope)
\big [ / ]_ ( <- ) [not, in mathcomp.boot.bigop] (in big_scope)
\big [ / ]_ ( <- | ) [not, in mathcomp.boot.bigop] (in big_scope)
\big [ / ]_ ( <= < ) [not, in mathcomp.boot.bigop] (in big_scope)
\big [ / ]_ ( <= < | ) [not, in mathcomp.boot.bigop] (in big_scope)
\big [ / ]_ ( in ) [not, in mathcomp.boot.bigop] (in big_scope)
\big [ / ]_ ( in | ) [not, in mathcomp.boot.bigop] (in big_scope)
\big [ / ]_ ( | ) [not, in mathcomp.boot.bigop] (in big_scope)
\big [ / ]_ [not, in mathcomp.boot.bigop] (in big_scope)

bool_scope

, exists : in [not, in mathcomp.boot.fintype] (in bool_scope)
, exists in [not, in mathcomp.boot.fintype] (in bool_scope)
, forall : in [not, in mathcomp.boot.fintype] (in bool_scope)
, forall in [not, in mathcomp.boot.fintype] (in bool_scope)
[ disjoint & ] [not, in mathcomp.boot.fintype] (in bool_scope)
[ exists ( : | ) ] [not, in mathcomp.boot.fintype] (in bool_scope)
[ exists ( | ) ] [not, in mathcomp.boot.fintype] (in bool_scope)
[ exists : in ] [not, in mathcomp.boot.fintype] (in bool_scope)
[ exists : ] [not, in mathcomp.boot.fintype] (in bool_scope)
[ exists in ] [not, in mathcomp.boot.fintype] (in bool_scope)
[ exists ] [not, in mathcomp.boot.fintype] (in bool_scope)
[ forall ( : | ) ] [not, in mathcomp.boot.fintype] (in bool_scope)
[ forall ( | ) ] [not, in mathcomp.boot.fintype] (in bool_scope)
[ forall : in ] [not, in mathcomp.boot.fintype] (in bool_scope)
[ forall : ] [not, in mathcomp.boot.fintype] (in bool_scope)
[ forall in ] [not, in mathcomp.boot.fintype] (in bool_scope)
[ forall ] [not, in mathcomp.boot.fintype] (in bool_scope)
!= [not, in mathcomp.boot.eqtype] (in bool_scope)
!= :> [not, in mathcomp.boot.eqtype] (in bool_scope)
'_|_ [not, in mathcomp.algebra.spectral] (in bool_scope)
== [not, in mathcomp.boot.eqtype] (in bool_scope)
== :> [not, in mathcomp.boot.eqtype] (in bool_scope)
\proper [not, in mathcomp.boot.fintype] (in bool_scope)
\subset [not, in mathcomp.boot.fintype] (in bool_scope)

cfun_scope

#[ ] [not, in mathcomp.group_representation.classfun] (in cfun_scope)
'Z ( ) [not, in mathcomp.group_representation.character] (in cfun_scope)
'o ( ) [not, in mathcomp.group_representation.character] (in cfun_scope)
1 [not, in mathcomp.group_representation.classfun] (in cfun_scope)
%% B [not, in mathcomp.group_representation.classfun] (in cfun_scope)
%% [not, in mathcomp.group_representation.classfun] (in cfun_scope)
.[ ] [not, in mathcomp.group_representation.character] (in cfun_scope)
/ B [not, in mathcomp.group_representation.classfun] (in cfun_scope)
/ [not, in mathcomp.group_representation.classfun] (in cfun_scope)
^ [not, in mathcomp.group_representation.inertia] (in cfun_scope)
^* [not, in mathcomp.group_representation.classfun] (in cfun_scope)
^: [not, in mathcomp.group_representation.inertia] (in cfun_scope)
^: [not, in mathcomp.group_representation.inertia] (in cfun_scope)

coq_nat_scope

* [not, in mathcomp.boot.ssrnat] (in coq_nat_scope)
+ [not, in mathcomp.boot.ssrnat] (in coq_nat_scope)
- [not, in mathcomp.boot.ssrnat] (in coq_nat_scope)
< [not, in mathcomp.boot.ssrnat] (in coq_nat_scope)
<= [not, in mathcomp.boot.ssrnat] (in coq_nat_scope)
> [not, in mathcomp.boot.ssrnat] (in coq_nat_scope)
>= [not, in mathcomp.boot.ssrnat] (in coq_nat_scope)

distn_scope

- [not, in mathcomp.algebra.ssrint] (in distn_scope)
- [not, in mathcomp.algebra.ssrint] (in distn_scope)

eq_scope

=P [not, in mathcomp.boot.eqtype] (in eq_scope)
=P :> [not, in mathcomp.boot.eqtype] (in eq_scope)

fin_quant_scope

, exists ( : | ) [not, in mathcomp.boot.fintype] (in fin_quant_scope)
, exists ( | ) [not, in mathcomp.boot.fintype] (in fin_quant_scope)
, exists : [not, in mathcomp.boot.fintype] (in fin_quant_scope)
, exists [not, in mathcomp.boot.fintype] (in fin_quant_scope)
, forall ( : | ) [not, in mathcomp.boot.fintype] (in fin_quant_scope)
, forall ( | ) [not, in mathcomp.boot.fintype] (in fin_quant_scope)
, forall : [not, in mathcomp.boot.fintype] (in fin_quant_scope)
, forall [not, in mathcomp.boot.fintype] (in fin_quant_scope)
, [not, in mathcomp.boot.fintype] (in fin_quant_scope)

form_scope

[ <-> ; ; .. ; ] [not, in mathcomp.boot.seq] (in form_scope)
[ Choice of by <:%/ ] [not, in mathcomp.boot.generic_quotient] (in form_scope)
[ Choice of by <: ] [not, in mathcomp.boot.choice] (in form_scope)
[ Countable of by <:%/ ] [not, in mathcomp.boot.generic_quotient] (in form_scope)
[ Countable of by <: ] [not, in mathcomp.boot.choice] (in form_scope)
[ Equality of by <:%/ ] [not, in mathcomp.boot.generic_quotient] (in form_scope)
[ Equality of by <: ] [not, in mathcomp.boot.eqtype] (in form_scope)
[ Finite of by <:%/ ] [not, in mathcomp.boot.generic_quotient] (in form_scope)
[ Finite of by <: ] [not, in mathcomp.boot.fintype] (in form_scope)
[ Order of by <: ] [not, in mathcomp.order.order] (in form_scope)
[ POrder of by <: ] [not, in mathcomp.order.order] (in form_scope)
[ Sub by %/ ] [not, in mathcomp.boot.generic_quotient] (in form_scope)
[ Sub of by %/ ] [not, in mathcomp.boot.generic_quotient] (in form_scope)
[ SubChoice_isBSubLattice of by <: ] [not, in mathcomp.order.order] (in form_scope)
[ SubChoice_isBSubLattice of by <: with ] [not, in mathcomp.order.order] (in form_scope)
[ SubChoice_isSubAlgebra of by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.ssralg] (in form_scope)
[ SubChoice_isSubComNzRing of by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in form_scope)
[ SubChoice_isSubComNzSemiRing of by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in form_scope)
[ SubChoice_isSubComPzRing of by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in form_scope)
[ SubChoice_isSubComPzSemiRing of by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in form_scope)
[ SubChoice_isSubComRing of by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.ssralg] (in form_scope)
[ SubChoice_isSubComSemiRing of by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.ssralg] (in form_scope)
[ SubChoice_isSubComUnitRing of by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.divalg] (in form_scope)
[ SubChoice_isSubIntegralDomain of by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.divalg] (in form_scope)
[ SubChoice_isSubLSemiAlgebra of by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.ssralg] (in form_scope)
[ SubChoice_isSubLSemiModule of by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in form_scope)
[ SubChoice_isSubLalgebra of by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.ssralg] (in form_scope)
[ SubChoice_isSubLattice of by <: ] [not, in mathcomp.order.order] (in form_scope)
[ SubChoice_isSubLattice of by <: with ] [not, in mathcomp.order.order] (in form_scope)
[ SubChoice_isSubLmodule of by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in form_scope)
[ SubChoice_isSubNmodule of by <: ] [not, in mathcomp.boot.nmodule] (in form_scope)
[ SubChoice_isSubNzAlgebra of by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in form_scope)
[ SubChoice_isSubNzLSemiAlgebra of by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in form_scope)
[ SubChoice_isSubNzLalgebra of by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in form_scope)
[ SubChoice_isSubNzRing of by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in form_scope)
[ SubChoice_isSubNzSemiAlgebra of by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in form_scope)
[ SubChoice_isSubNzSemiRing of by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in form_scope)
[ SubChoice_isSubOrder of by <: ] [not, in mathcomp.order.order] (in form_scope)
[ SubChoice_isSubOrder of by <: with ] [not, in mathcomp.order.order] (in form_scope)
[ SubChoice_isSubPOrder of by <: ] [not, in mathcomp.order.order] (in form_scope)
[ SubChoice_isSubPOrder of by <: with ] [not, in mathcomp.order.order] (in form_scope)
[ SubChoice_isSubPreorder of by <: ] [not, in mathcomp.order.preorder] (in form_scope)
[ SubChoice_isSubPreorder of by <: with ] [not, in mathcomp.order.preorder] (in form_scope)
[ SubChoice_isSubPzAlgebra of by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in form_scope)
[ SubChoice_isSubPzLSemiAlgebra of by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in form_scope)
[ SubChoice_isSubPzLalgebra of by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in form_scope)
[ SubChoice_isSubPzRing of by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in form_scope)
[ SubChoice_isSubPzSemiAlgebra of by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in form_scope)
[ SubChoice_isSubPzSemiRing of by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in form_scope)
[ SubChoice_isSubRing of by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.ssralg] (in form_scope)
[ SubChoice_isSubSemiAlgebra of by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.ssralg] (in form_scope)
[ SubChoice_isSubSemiRing of by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.ssralg] (in form_scope)
[ SubChoice_isSubUnitRing of by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.divalg] (in form_scope)
[ SubChoice_isSubZmodule of by <: ] [not, in mathcomp.boot.nmodule] (in form_scope)
[ SubChoice_isTBSubLattice of by <: ] [not, in mathcomp.order.order] (in form_scope)
[ SubChoice_isTBSubLattice of by <: with ] [not, in mathcomp.order.order] (in form_scope)
[ SubChoice_isTSubLattice of by <: ] [not, in mathcomp.order.order] (in form_scope)
[ SubChoice_isTSubLattice of by <: with ] [not, in mathcomp.order.order] (in form_scope)
[ SubComUnitRing_isSubIntegralDomain of by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.divalg] (in form_scope)
[ SubIntegralDomain_isSubField of by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.divalg] (in form_scope)
[ SubLSemiAlgebra_isSubSemiAlgebra of by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in form_scope)
[ SubLalgebra_isSubAlgebra of by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.ssralg] (in form_scope)
[ SubLattice_isSubOrder of by <: ] [not, in mathcomp.order.order] (in form_scope)
[ SubLattice_isSubOrder of by <: with ] [not, in mathcomp.order.order] (in form_scope)
[ SubNmodule_isSubLSemiModule of by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in form_scope)
[ SubNmodule_isSubNzSemiRing of by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in form_scope)
[ SubNmodule_isSubPzSemiRing of by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in form_scope)
[ SubNmodule_isSubSemiRing of by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.ssralg] (in form_scope)
[ SubNmodule_isSubZmodule of by <: ] [not, in mathcomp.boot.nmodule] (in form_scope)
[ SubNzRing_SubLmodule_isSubLalgebra of by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.ssralg] (in form_scope)
[ SubNzRing_isSubComNzRing of by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.ssralg] (in form_scope)
[ SubNzRing_isSubUnitRing of by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.divalg] (in form_scope)
[ SubNzSemiRing_SubLSemiModule_isSubLSemiAlgebra of by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.ssralg] (in form_scope)
[ SubNzSemiRing_isSubComNzSemiRing of by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.ssralg] (in form_scope)
[ SubPOrder_isBSubLattice of by <: ] [not, in mathcomp.order.order] (in form_scope)
[ SubPOrder_isBSubLattice of by <: with ] [not, in mathcomp.order.order] (in form_scope)
[ SubPOrder_isSubLattice of by <: ] [not, in mathcomp.order.order] (in form_scope)
[ SubPOrder_isSubLattice of by <: with ] [not, in mathcomp.order.order] (in form_scope)
[ SubPOrder_isSubOrder of by <: ] [not, in mathcomp.order.order] (in form_scope)
[ SubPOrder_isSubOrder of by <: with ] [not, in mathcomp.order.order] (in form_scope)
[ SubPOrder_isTBSubLattice of by <: ] [not, in mathcomp.order.order] (in form_scope)
[ SubPOrder_isTBSubLattice of by <: with ] [not, in mathcomp.order.order] (in form_scope)
[ SubPOrder_isTSubLattice of by <: ] [not, in mathcomp.order.order] (in form_scope)
[ SubPOrder_isTSubLattice of by <: with ] [not, in mathcomp.order.order] (in form_scope)
[ SubPzRing_isSubComPzRing of by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.ssralg] (in form_scope)
[ SubPzSemiRing_isSubComPzSemiRing of by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.ssralg] (in form_scope)
[ SubRing_SubLmodule_isSubLalgebra of by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in form_scope)
[ SubRing_isSubComRing of by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.ssralg] (in form_scope)
[ SubRing_isSubUnitRing of by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.ssralg] (in form_scope)
[ SubSemiRing_SubLSemiModule_isSubLSemiAlgebra of by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in form_scope)
[ SubSemiRing_isSubComSemiRing of by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in form_scope)
[ SubZmodule_isSubLmodule of by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.ssralg] (in form_scope)
[ SubZmodule_isSubNzRing of by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.ssralg] (in form_scope)
[ SubZmodule_isSubRing of by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.ssralg] (in form_scope)
[ action of ] [not, in mathcomp.finite_group.action] (in form_scope)
[ acts , on | ] [not, in mathcomp.finite_group.action] (in form_scope)
[ aspace of ] [not, in mathcomp.field.falgebra] (in form_scope)
[ aspace of for ] [not, in mathcomp.field.falgebra] (in form_scope)
[ bseq ] [not, in mathcomp.boot.tuple] (in form_scope)
[ bseq of ] [not, in mathcomp.boot.tuple] (in form_scope)
[ bseq ; .. ; ] [not, in mathcomp.boot.tuple] (in form_scope)
[ equiv_rel of ] [not, in mathcomp.boot.generic_quotient] (in form_scope)
[ faithful , on | ] [not, in mathcomp.finite_group.action] (in form_scope)
[ finGroupMixin of for +%R ] [not, in mathcomp.algebra.finalg] (in form_scope)
[ gFun by ] [not, in mathcomp.solvable.gfunctor] (in form_scope)
[ gFun of ] [not, in mathcomp.solvable.gfunctor] (in form_scope)
[ group of ] [not, in mathcomp.finite_group.fingroup] (in form_scope)
[ groupAction of ] [not, in mathcomp.finite_group.action] (in form_scope)
[ igFun by & ! ] [not, in mathcomp.solvable.gfunctor] (in form_scope)
[ igFun by & ] [not, in mathcomp.solvable.gfunctor] (in form_scope)
[ igFun of ] [not, in mathcomp.solvable.gfunctor] (in form_scope)
[ isNew for ] [not, in mathcomp.boot.eqtype] (in form_scope)
[ isNew for ] [not, in mathcomp.boot.eqtype] (in form_scope)
[ isNew of for ] [not, in mathcomp.boot.eqtype] (in form_scope)
[ isSub for ] [not, in mathcomp.boot.eqtype] (in form_scope)
[ isSub for ] [not, in mathcomp.boot.eqtype] (in form_scope)
[ isSub for by ] [not, in mathcomp.boot.eqtype] (in form_scope)
[ isSub of for ] [not, in mathcomp.boot.eqtype] (in form_scope)
[ jlmorphism of ] [not, in mathcomp.order.order] (in form_scope)
[ jlmorphism of as ] [not, in mathcomp.order.order] (in form_scope)
[ lmorphism of ] [not, in mathcomp.order.order] (in form_scope)
[ lmorphism of as ] [not, in mathcomp.order.order] (in form_scope)
[ mgFun by ] [not, in mathcomp.solvable.gfunctor] (in form_scope)
[ mgFun of ] [not, in mathcomp.solvable.gfunctor] (in form_scope)
[ mlmorphism of ] [not, in mathcomp.order.order] (in form_scope)
[ mlmorphism of as ] [not, in mathcomp.order.order] (in form_scope)
[ morphism of ] [not, in mathcomp.finite_group.morphism] (in form_scope)
[ morphism of ] [not, in mathcomp.finite_group.morphism] (in form_scope)
[ pgFun by ] [not, in mathcomp.solvable.gfunctor] (in form_scope)
[ pgFun of ] [not, in mathcomp.solvable.gfunctor] (in form_scope)
[ pick : ] [not, in mathcomp.boot.fintype] (in form_scope)
[ pick : ] [not, in mathcomp.boot.fintype] (in form_scope)
[ pick : in ] [not, in mathcomp.boot.fintype] (in form_scope)
[ pick : in | & ] [not, in mathcomp.boot.fintype] (in form_scope)
[ pick : in | ] [not, in mathcomp.boot.fintype] (in form_scope)
[ pick : | & ] [not, in mathcomp.boot.fintype] (in form_scope)
[ pick : | ] [not, in mathcomp.boot.fintype] (in form_scope)
[ pick ] [not, in mathcomp.boot.fintype] (in form_scope)
[ pick in ] [not, in mathcomp.boot.fintype] (in form_scope)
[ pick in | & ] [not, in mathcomp.boot.fintype] (in form_scope)
[ pick in | ] [not, in mathcomp.boot.fintype] (in form_scope)
[ pick | & ] [not, in mathcomp.boot.fintype] (in form_scope)
[ pick | ] [not, in mathcomp.boot.fintype] (in form_scope)
[ primitive , on | ] [not, in mathcomp.solvable.primitive_action] (in form_scope)
[ tnth ] [not, in mathcomp.boot.tuple] (in form_scope)
[ transitive ^ , on | ] [not, in mathcomp.solvable.primitive_action] (in form_scope)
[ transitive , on | ] [not, in mathcomp.finite_group.action] (in form_scope)
[ tuple ] [not, in mathcomp.boot.tuple] (in form_scope)
[ tuple of ] [not, in mathcomp.boot.tuple] (in form_scope)
[ tuple ; .. ; ] [not, in mathcomp.boot.tuple] (in form_scope)
[ tuple | < ] [not, in mathcomp.boot.tuple] (in form_scope)

fun_delta_scope

|-> [not, in mathcomp.boot.eqtype] (in fun_delta_scope)

function_scope

*%R [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in function_scope)
*%R [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in function_scope)
*%g [not, in mathcomp.boot.monoid] (in function_scope)
*%g [not, in mathcomp.boot.monoid] (in function_scope)
*:%R [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in function_scope)
*:%R [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in function_scope)
*t%R [not, in mathcomp.algebra.tensor] (in function_scope)
*~%R [not, in mathcomp.algebra.ssrint] (in function_scope)
+%R [not, in mathcomp.boot.nmodule] (in function_scope)
+%R [not, in mathcomp.boot.nmodule] (in function_scope)
+%R [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in function_scope)
<%O [not, in mathcomp.order.preorder] (in function_scope)
<%R [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in function_scope)
<=%O [not, in mathcomp.order.preorder] (in function_scope)
<=%R [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in function_scope)
<=^d%O [not, in mathcomp.order.preorder] (in function_scope)
<=^l%O [not, in mathcomp.order.preorder] (in function_scope)
<=^l%O [not, in mathcomp.order.preorder] (in function_scope)
<=^p%O [not, in mathcomp.order.preorder] (in function_scope)
<=^sp%O [not, in mathcomp.order.preorder] (in function_scope)
[not, in mathcomp.order.preorder] (in function_scope)
[not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in function_scope)
[not, in mathcomp.order.preorder] (in function_scope)
[not, in mathcomp.order.preorder] (in function_scope)
[not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in function_scope)
[not, in mathcomp.order.preorder] (in function_scope)
[not, in mathcomp.order.preorder] (in function_scope)
[not, in mathcomp.order.preorder] (in function_scope)
[not, in mathcomp.order.preorder] (in function_scope)
[not, in mathcomp.order.preorder] (in function_scope)
<^d%O [not, in mathcomp.order.preorder] (in function_scope)
<^l%O [not, in mathcomp.order.preorder] (in function_scope)
<^l%O [not, in mathcomp.order.preorder] (in function_scope)
<^p%O [not, in mathcomp.order.preorder] (in function_scope)
<^sp%O [not, in mathcomp.order.preorder] (in function_scope)
>%O [not, in mathcomp.order.preorder] (in function_scope)
>%R [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in function_scope)
><%O [not, in mathcomp.order.preorder] (in function_scope)
><%R [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in function_scope)
><^d%O [not, in mathcomp.order.preorder] (in function_scope)
><^l%O [not, in mathcomp.order.preorder] (in function_scope)
><^l%O [not, in mathcomp.order.preorder] (in function_scope)
><^p%O [not, in mathcomp.order.preorder] (in function_scope)
><^sp%O [not, in mathcomp.order.preorder] (in function_scope)
>=%O [not, in mathcomp.order.preorder] (in function_scope)
>=%R [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in function_scope)
>=<%O [not, in mathcomp.order.preorder] (in function_scope)
>=<%R [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in function_scope)
>=<^d%O [not, in mathcomp.order.preorder] (in function_scope)
>=<^l%O [not, in mathcomp.order.preorder] (in function_scope)
>=<^l%O [not, in mathcomp.order.preorder] (in function_scope)
>=<^p%O [not, in mathcomp.order.preorder] (in function_scope)
>=<^sp%O [not, in mathcomp.order.preorder] (in function_scope)
>=^d%O [not, in mathcomp.order.preorder] (in function_scope)
>=^l%O [not, in mathcomp.order.preorder] (in function_scope)
>=^l%O [not, in mathcomp.order.preorder] (in function_scope)
>=^l%O [not, in mathcomp.order.preorder] (in function_scope)
>=^l%O [not, in mathcomp.order.preorder] (in function_scope)
>=^p%O [not, in mathcomp.order.preorder] (in function_scope)
>=^p%O [not, in mathcomp.order.preorder] (in function_scope)
>=^sp%O [not, in mathcomp.order.preorder] (in function_scope)
>=^sp%O [not, in mathcomp.order.preorder] (in function_scope)
>^d%O [not, in mathcomp.order.preorder] (in function_scope)
>^l%O [not, in mathcomp.order.preorder] (in function_scope)
>^l%O [not, in mathcomp.order.preorder] (in function_scope)
>^p%O [not, in mathcomp.order.preorder] (in function_scope)
>^sp%O [not, in mathcomp.order.preorder] (in function_scope)
@ comparabler [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in function_scope)
@ dvd [not, in mathcomp.order.preorder] (in function_scope)
@ gcd [not, in mathcomp.order.order] (in function_scope)
@ ger [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in function_scope)
@ gtr [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in function_scope)
@ lcm [not, in mathcomp.order.order] (in function_scope)
@ ler [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in function_scope)
@ lerif [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in function_scope)
@ lteif [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in function_scope)
@ ltr [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in function_scope)
@ maxr [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in function_scope)
@ minr [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in function_scope)
@ sdvd [not, in mathcomp.order.preorder] (in function_scope)
[ eta with , .. , ] [not, in mathcomp.boot.eqtype] (in function_scope)
[ ffun => ] [not, in mathcomp.boot.finfun] (in function_scope)
[ ffun : => ] [not, in mathcomp.boot.finfun] (in function_scope)
[ ffun => ] [not, in mathcomp.boot.finfun] (in function_scope)
[ fprod : => ] [not, in mathcomp.boot.finfun] (in function_scope)
[ fprod => ] [not, in mathcomp.boot.finfun] (in function_scope)
[ fprod : => ] [not, in mathcomp.boot.finfun] (in function_scope)
[ fprod => ] [not, in mathcomp.boot.finfun] (in function_scope)
[ fun : => with , .. , ] [not, in mathcomp.boot.eqtype] (in function_scope)
[ fun => with , .. , ] [not, in mathcomp.boot.eqtype] (in function_scope)
[ predD1 & ] [not, in mathcomp.boot.eqtype] (in function_scope)
[ predU1 & ] [not, in mathcomp.boot.eqtype] (in function_scope)
[ predX & ] [not, in mathcomp.boot.eqtype] (in function_scope)
\- [not, in mathcomp.boot.nmodule] (in function_scope)
\- [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in function_scope)
\0 [not, in mathcomp.boot.nmodule] (in function_scope)
\0 [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in function_scope)
\1 [not, in mathcomp.boot.monoid] (in function_scope)
.-support [not, in mathcomp.boot.finfun] (in function_scope)
\* [not, in mathcomp.boot.monoid] (in function_scope)
\* [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in function_scope)
\*: [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in function_scope)
\*o [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in function_scope)
\+ [not, in mathcomp.boot.nmodule] (in function_scope)
\+ [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in function_scope)
\- [not, in mathcomp.boot.nmodule] (in function_scope)
\- [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in function_scope)
\max [not, in mathcomp.order.preorder] (in function_scope)
\min [not, in mathcomp.order.preorder] (in function_scope)
\o* [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in function_scope)
^* [not, in mathcomp.finite_group.action] (in function_scope)

gFun_scope

%% [not, in mathcomp.solvable.gfunctor] (in gFun_scope)
\o [not, in mathcomp.solvable.gfunctor] (in gFun_scope)

groupAction_scope

'J [not, in mathcomp.finite_group.action] (in groupAction_scope)
'M [not, in mathcomp.solvable.finmodule] (in groupAction_scope)
'M [not, in mathcomp.solvable.finmodule] (in groupAction_scope)
'MR [not, in mathcomp.group_representation.mxabelem] (in groupAction_scope)
'Q [not, in mathcomp.finite_group.action] (in groupAction_scope)
'U [not, in mathcomp.algebra.finalg] (in groupAction_scope)
'Zm [not, in mathcomp.group_representation.mxabelem] (in groupAction_scope)
<[ ] > [not, in mathcomp.finite_group.action] (in groupAction_scope)
[ Aut ] [not, in mathcomp.finite_group.action] (in groupAction_scope)
%% [not, in mathcomp.finite_group.action] (in groupAction_scope)
/ [not, in mathcomp.finite_group.action] (in groupAction_scope)
\ [not, in mathcomp.finite_group.action] (in groupAction_scope)
\o [not, in mathcomp.finite_group.action] (in groupAction_scope)

group_rel_scope

.-central [not, in mathcomp.solvable.gseries] (in group_rel_scope)
.-chief [not, in mathcomp.solvable.gseries] (in group_rel_scope)
.-invariant [not, in mathcomp.solvable.gseries] (in group_rel_scope)
.-stable [not, in mathcomp.solvable.gseries] (in group_rel_scope)

group_ring_scope

'R_ [not, in mathcomp.group_representation.mxrepresentation] (in group_ring_scope)
'R_ [not, in mathcomp.group_representation.mxrepresentation] (in group_ring_scope)
'e_ [not, in mathcomp.group_representation.mxrepresentation] (in group_ring_scope)
'e_ [not, in mathcomp.group_representation.mxrepresentation] (in group_ring_scope)
'n_ [not, in mathcomp.group_representation.mxrepresentation] (in group_ring_scope)
'n_ [not, in mathcomp.group_representation.mxrepresentation] (in group_ring_scope)

group_scope

#[ ] [not, in mathcomp.finite_group.fingroup] (in group_scope)
#| : | [not, in mathcomp.finite_group.fingroup] (in group_scope)
'Alt_ [not, in mathcomp.solvable.alt] (in group_scope)
'C ( ) [not, in mathcomp.finite_group.fingroup] (in group_scope)
'C ( | ) [not, in mathcomp.finite_group.action] (in group_scope)
'C [ ] [not, in mathcomp.finite_group.fingroup] (in group_scope)
'C [ | ] [not, in mathcomp.finite_group.action] (in group_scope)
'C_ ( | ) ( ) [not, in mathcomp.finite_group.action] (in group_scope)
'C_ ( | ) [ ] [not, in mathcomp.finite_group.action] (in group_scope)
'C_ ( ) ( ) [not, in mathcomp.finite_group.fingroup] (in group_scope)
'C_ ( ) ( | ) [not, in mathcomp.finite_group.action] (in group_scope)
'C_ ( ) [ ] [not, in mathcomp.finite_group.fingroup] (in group_scope)
'C_ ( ) [ | ] [not, in mathcomp.finite_group.action] (in group_scope)
'C_ ( | ) ( ) [not, in mathcomp.finite_group.action] (in group_scope)
'C_ ( | ) [ ] [not, in mathcomp.finite_group.action] (in group_scope)
'C_ ( ) [not, in mathcomp.finite_group.fingroup] (in group_scope)
'C_ ( | ) [not, in mathcomp.finite_group.action] (in group_scope)
'C_ [ ] [not, in mathcomp.finite_group.fingroup] (in group_scope)
'C_ [ | ] [not, in mathcomp.finite_group.action] (in group_scope)
'D^ [not, in mathcomp.solvable.extraspecial] (in group_scope)
'D^ * Q [not, in mathcomp.solvable.extraspecial] (in group_scope)
'D_ [not, in mathcomp.solvable.extremal] (in group_scope)
'E ^ ( ) [not, in mathcomp.solvable.abelian] (in group_scope)
'E*_ ( ) [not, in mathcomp.solvable.abelian] (in group_scope)
'E_ ( ) [not, in mathcomp.solvable.abelian] (in group_scope)
'E_ ^ ( ) [not, in mathcomp.solvable.abelian] (in group_scope)
'F ( ) [not, in mathcomp.solvable.maximal] (in group_scope)
'Fix_ ( ) ( ) [not, in mathcomp.finite_group.action] (in group_scope)
'Fix_ ( | ) ( ) [not, in mathcomp.finite_group.action] (in group_scope)
'Fix_ ( | ) [ ] [not, in mathcomp.finite_group.action] (in group_scope)
'Fix_ ( ) [not, in mathcomp.finite_group.action] (in group_scope)
'Fix_ [ ] [not, in mathcomp.finite_group.action] (in group_scope)
'GL_ ( ) [not, in mathcomp.algebra.matrix] (in group_scope)
'GL_ [ ] [not, in mathcomp.algebra.matrix] (in group_scope)
'Gal ( / ) [not, in mathcomp.field.galois] (in group_scope)
'Gal ( / ) [not, in mathcomp.field.galois] (in group_scope)
'I[ ] [not, in mathcomp.group_representation.inertia] (in group_scope)
'I[ ] [not, in mathcomp.group_representation.inertia] (in group_scope)
'I_ [ ] [not, in mathcomp.group_representation.inertia] (in group_scope)
'I_ [ ] [not, in mathcomp.group_representation.inertia] (in group_scope)
'L_ ( ) [not, in mathcomp.solvable.nilpotent] (in group_scope)
'Ldiv_ ( ) [not, in mathcomp.solvable.abelian] (in group_scope)
'Ldiv_ () [not, in mathcomp.solvable.abelian] (in group_scope)
'Mho^ ( ) [not, in mathcomp.solvable.abelian] (in group_scope)
'Mod_ [not, in mathcomp.solvable.extremal] (in group_scope)
'N ( ) [not, in mathcomp.finite_group.fingroup] (in group_scope)
'N ( | ) [not, in mathcomp.finite_group.action] (in group_scope)
'N_ ( ) [not, in mathcomp.finite_group.fingroup] (in group_scope)
'N_ ( | ) [not, in mathcomp.finite_group.action] (in group_scope)
'O_ ( ) [not, in mathcomp.solvable.pgroup] (in group_scope)
'O_{ , .. , } ( ) [not, in mathcomp.solvable.pgroup] (in group_scope)
'Ohm_ ( ) [not, in mathcomp.solvable.abelian] (in group_scope)
'Phi ( ) [not, in mathcomp.solvable.maximal] (in group_scope)
'Q_ [not, in mathcomp.solvable.extremal] (in group_scope)
'SCN ( ) [not, in mathcomp.solvable.maximal] (in group_scope)
'SCN_ ( ) [not, in mathcomp.solvable.maximal] (in group_scope)
'SD_ [not, in mathcomp.solvable.extremal] (in group_scope)
'Syl_ ( ) [not, in mathcomp.solvable.pgroup] (in group_scope)
'Sym_ [not, in mathcomp.solvable.alt] (in group_scope)
'Z ( ) [not, in mathcomp.solvable.center] (in group_scope)
'Z[ , ] [not, in mathcomp.group_representation.vcharacter] (in group_scope)
'Z[ ] [not, in mathcomp.group_representation.vcharacter] (in group_scope)
'Z_ ( ) [not, in mathcomp.solvable.nilpotent] (in group_scope)
'dom [not, in mathcomp.finite_group.morphism] (in group_scope)
'injm [not, in mathcomp.finite_group.morphism] (in group_scope)
'ker [not, in mathcomp.finite_group.morphism] (in group_scope)
'ker_ [not, in mathcomp.finite_group.morphism] (in group_scope)
'm ( ) [not, in mathcomp.solvable.abelian] (in group_scope)
'r ( ) [not, in mathcomp.solvable.abelian] (in group_scope)
'r_ ( ) [not, in mathcomp.solvable.abelian] (in group_scope)
1 [not, in mathcomp.boot.monoid] (in group_scope)
1 [not, in mathcomp.boot.monoid] (in group_scope)
<< >> [not, in mathcomp.finite_group.fingroup] (in group_scope)
<[ ] > [not, in mathcomp.finite_group.fingroup] (in group_scope)
[ 1 ] [not, in mathcomp.finite_group.fingroup] (in group_scope)
[ 1 ] [not, in mathcomp.finite_group.fingroup] (in group_scope)
[ Aut ] [not, in mathcomp.finite_group.automorphism] (in group_scope)
[ Frobenius = ><| ] [not, in mathcomp.solvable.frobenius] (in group_scope)
[ Frobenius ] [not, in mathcomp.solvable.frobenius] (in group_scope)
[ Frobenius with complement ] [not, in mathcomp.solvable.frobenius] (in group_scope)
[ Frobenius with kernel ] [not, in mathcomp.solvable.frobenius] (in group_scope)
[ complements to in ] [not, in mathcomp.finite_group.gproduct] (in group_scope)
[ max of | & ] [not, in mathcomp.finite_group.fingroup] (in group_scope)
[ max of | ] [not, in mathcomp.finite_group.fingroup] (in group_scope)
[ max | & ] [not, in mathcomp.finite_group.fingroup] (in group_scope)
[ max | ] [not, in mathcomp.finite_group.fingroup] (in group_scope)
[ min of | & ] [not, in mathcomp.finite_group.fingroup] (in group_scope)
[ min of | ] [not, in mathcomp.finite_group.fingroup] (in group_scope)
[ min | & ] [not, in mathcomp.finite_group.fingroup] (in group_scope)
[ min | ] [not, in mathcomp.finite_group.fingroup] (in group_scope)
[ splits , over ] [not, in mathcomp.finite_group.gproduct] (in group_scope)
[ subg ] [not, in mathcomp.finite_group.fingroup] (in group_scope)
[ ~ , , .. , ] [not, in mathcomp.boot.monoid] (in group_scope)
[ ~ , , .. , ] [not, in mathcomp.boot.monoid] (in group_scope)
[ ~: , , .. , ] [not, in mathcomp.finite_group.fingroup] (in group_scope)
\prod_ ( : ) [not, in mathcomp.boot.monoid] (in group_scope)
\prod_ ( : | ) [not, in mathcomp.boot.monoid] (in group_scope)
\prod_ ( < ) [not, in mathcomp.boot.monoid] (in group_scope)
\prod_ ( < | ) [not, in mathcomp.boot.monoid] (in group_scope)
\prod_ ( <- ) [not, in mathcomp.boot.monoid] (in group_scope)
\prod_ ( <- | ) [not, in mathcomp.boot.monoid] (in group_scope)
\prod_ ( <= < ) [not, in mathcomp.boot.monoid] (in group_scope)
\prod_ ( <= < | ) [not, in mathcomp.boot.monoid] (in group_scope)
\prod_ ( in ) [not, in mathcomp.boot.monoid] (in group_scope)
\prod_ ( in | ) [not, in mathcomp.boot.monoid] (in group_scope)
\prod_ ( | ) [not, in mathcomp.boot.monoid] (in group_scope)
\prod_ [not, in mathcomp.boot.monoid] (in group_scope)
` T [not, in mathcomp.group_representation.inertia] (in group_scope)
* [not, in mathcomp.boot.monoid] (in group_scope)
* [not, in mathcomp.boot.monoid] (in group_scope)
*: [not, in mathcomp.finite_group.fingroup] (in group_scope)
.-Hall ( ) [not, in mathcomp.solvable.pgroup] (in group_scope)
.-Sylow ( ) [not, in mathcomp.solvable.pgroup] (in group_scope)
.-abelem [not, in mathcomp.solvable.abelian] (in group_scope)
.-elt [not, in mathcomp.solvable.pgroup] (in group_scope)
.-group [not, in mathcomp.solvable.pgroup] (in group_scope)
.-series [not, in mathcomp.solvable.gseries] (in group_scope)
.-subgroup ( ) [not, in mathcomp.solvable.pgroup] (in group_scope)
.`_ [not, in mathcomp.solvable.pgroup] (in group_scope)
/ [not, in mathcomp.finite_group.quotient] (in group_scope)
/ [not, in mathcomp.boot.monoid] (in group_scope)
/ [not, in mathcomp.boot.monoid] (in group_scope)
:* [not, in mathcomp.finite_group.fingroup] (in group_scope)
:^ [not, in mathcomp.finite_group.fingroup] (in group_scope)
:^: [not, in mathcomp.finite_group.fingroup] (in group_scope)
<*> [not, in mathcomp.finite_group.fingroup] (in group_scope)
<| [not, in mathcomp.finite_group.fingroup] (in group_scope)
<|<| [not, in mathcomp.solvable.gseries] (in group_scope)
><| [not, in mathcomp.finite_group.gproduct] (in group_scope)
@* [not, in mathcomp.finite_group.morphism] (in group_scope)
@*^-1 [not, in mathcomp.finite_group.morphism] (in group_scope)
\* [not, in mathcomp.finite_group.gproduct] (in group_scope)
\char [not, in mathcomp.finite_group.automorphism] (in group_scope)
\homg Grp ( : ) [not, in mathcomp.finite_group.presentation] (in group_scope)
\homg Grp [not, in mathcomp.finite_group.presentation] (in group_scope)
\homg [not, in mathcomp.finite_group.morphism] (in group_scope)
\isog Grp ( : ) [not, in mathcomp.finite_group.presentation] (in group_scope)
\isog Grp [not, in mathcomp.finite_group.presentation] (in group_scope)
\x [not, in mathcomp.finite_group.gproduct] (in group_scope)
^# [not, in mathcomp.finite_group.fingroup] (in group_scope)
^ [not, in mathcomp.boot.monoid] (in group_scope)
^ [not, in mathcomp.boot.monoid] (in group_scope)
^+ [not, in mathcomp.boot.monoid] (in group_scope)
^+ [not, in mathcomp.boot.monoid] (in group_scope)
^- [not, in mathcomp.boot.monoid] (in group_scope)
^- [not, in mathcomp.boot.monoid] (in group_scope)
^-1 [not, in mathcomp.boot.monoid] (in group_scope)
^-1 [not, in mathcomp.boot.monoid] (in group_scope)
^: [not, in mathcomp.finite_group.fingroup] (in group_scope)
^` ( ) [not, in mathcomp.solvable.commutator] (in group_scope)
^{1+2* } [not, in mathcomp.solvable.extraspecial] (in group_scope)
^{1+2} [not, in mathcomp.solvable.extraspecial] (in group_scope)
`_ [not, in mathcomp.boot.monoid] (in group_scope)
`_ [not, in mathcomp.boot.monoid] (in group_scope)

int_scope

*%Z [not, in mathcomp.algebra.ssrint] (in int_scope)
+%Z [not, in mathcomp.algebra.ssrint] (in int_scope)
-%Z [not, in mathcomp.algebra.ssrint] (in int_scope)
- [not, in mathcomp.algebra.ssrint] (in int_scope)
!= %[mod ] [not, in mathcomp.algebra.intdiv] (in int_scope)
%% [not, in mathcomp.algebra.intdiv] (in int_scope)
%/ [not, in mathcomp.algebra.intdiv] (in int_scope)
%:Z [not, in mathcomp.algebra.ssrint] (in int_scope)
%| [not, in mathcomp.algebra.intdiv] (in int_scope)
* [not, in mathcomp.algebra.ssrint] (in int_scope)
+ [not, in mathcomp.algebra.ssrint] (in int_scope)
- [not, in mathcomp.algebra.ssrint] (in int_scope)
<> %[mod ] [not, in mathcomp.algebra.intdiv] (in int_scope)
= %[mod ] [not, in mathcomp.algebra.intdiv] (in int_scope)
== %[mod ] [not, in mathcomp.algebra.intdiv] (in int_scope)

irrType_scope

1 [not, in mathcomp.group_representation.mxrepresentation] (in irrType_scope)
[ 1 ] [not, in mathcomp.group_representation.mxrepresentation] (in irrType_scope)
[ 1 ] [not, in mathcomp.group_representation.mxrepresentation] (in irrType_scope)

lfun_scope

\1 [not, in mathcomp.algebra.vector] (in lfun_scope)
\o [not, in mathcomp.algebra.vector] (in lfun_scope)
^-1 [not, in mathcomp.algebra.vector] (in lfun_scope)

lrfun_scope

\1 [not, in mathcomp.field.falgebra] (in lrfun_scope)
\o [not, in mathcomp.field.falgebra] (in lrfun_scope)
^-1 [not, in mathcomp.field.galois] (in lrfun_scope)
^-1 [not, in mathcomp.field.galois] (in lrfun_scope)

matrix_set_scope

'C ( ) [not, in mathcomp.algebra.mxalgebra] (in matrix_set_scope)
'C ( ) [not, in mathcomp.algebra.mxalgebra] (in matrix_set_scope)
'C_ ( ) ( ) [not, in mathcomp.algebra.mxalgebra] (in matrix_set_scope)
'C_ ( ) [not, in mathcomp.algebra.mxalgebra] (in matrix_set_scope)
'Z ( ) [not, in mathcomp.algebra.mxalgebra] (in matrix_set_scope)
'Z ( ) [not, in mathcomp.algebra.mxalgebra] (in matrix_set_scope)
<< >> [not, in mathcomp.algebra.mxalgebra] (in matrix_set_scope)
<< >> [not, in mathcomp.algebra.mxalgebra] (in matrix_set_scope)
\bigcap_ ( : ) [not, in mathcomp.algebra.mxalgebra] (in matrix_set_scope)
\bigcap_ ( : | ) [not, in mathcomp.algebra.mxalgebra] (in matrix_set_scope)
\bigcap_ ( < ) [not, in mathcomp.algebra.mxalgebra] (in matrix_set_scope)
\bigcap_ ( < | ) [not, in mathcomp.algebra.mxalgebra] (in matrix_set_scope)
\bigcap_ ( <- ) [not, in mathcomp.algebra.mxalgebra] (in matrix_set_scope)
\bigcap_ ( <- | ) [not, in mathcomp.algebra.mxalgebra] (in matrix_set_scope)
\bigcap_ ( <= < ) [not, in mathcomp.algebra.mxalgebra] (in matrix_set_scope)
\bigcap_ ( <= < | ) [not, in mathcomp.algebra.mxalgebra] (in matrix_set_scope)
\bigcap_ ( in ) [not, in mathcomp.algebra.mxalgebra] (in matrix_set_scope)
\bigcap_ ( in | ) [not, in mathcomp.algebra.mxalgebra] (in matrix_set_scope)
\bigcap_ ( | ) [not, in mathcomp.algebra.mxalgebra] (in matrix_set_scope)
\bigcap_ ( | ) [not, in mathcomp.algebra.mxalgebra] (in matrix_set_scope)
\bigcap_ [not, in mathcomp.algebra.mxalgebra] (in matrix_set_scope)
\sum_ ( : ) [not, in mathcomp.algebra.mxalgebra] (in matrix_set_scope)
\sum_ ( : | ) [not, in mathcomp.algebra.mxalgebra] (in matrix_set_scope)
\sum_ ( < ) [not, in mathcomp.algebra.mxalgebra] (in matrix_set_scope)
\sum_ ( < | ) [not, in mathcomp.algebra.mxalgebra] (in matrix_set_scope)
\sum_ ( <- ) [not, in mathcomp.algebra.mxalgebra] (in matrix_set_scope)
\sum_ ( <- | ) [not, in mathcomp.algebra.mxalgebra] (in matrix_set_scope)
\sum_ ( <- | ) [not, in mathcomp.algebra.mxalgebra] (in matrix_set_scope)
\sum_ ( <= < ) [not, in mathcomp.algebra.mxalgebra] (in matrix_set_scope)
\sum_ ( <= < | ) [not, in mathcomp.algebra.mxalgebra] (in matrix_set_scope)
\sum_ ( in ) [not, in mathcomp.algebra.mxalgebra] (in matrix_set_scope)
\sum_ ( in | ) [not, in mathcomp.algebra.mxalgebra] (in matrix_set_scope)
\sum_ ( | ) [not, in mathcomp.algebra.mxalgebra] (in matrix_set_scope)
\sum_ ( | ) [not, in mathcomp.algebra.mxalgebra] (in matrix_set_scope)
\sum_ [not, in mathcomp.algebra.mxalgebra] (in matrix_set_scope)
'_|_ [not, in mathcomp.algebra.sesquilinear] (in matrix_set_scope)
* [not, in mathcomp.algebra.mxalgebra] (in matrix_set_scope)
* [not, in mathcomp.algebra.mxalgebra] (in matrix_set_scope)
+ [not, in mathcomp.algebra.mxalgebra] (in matrix_set_scope)
+ [not, in mathcomp.algebra.mxalgebra] (in matrix_set_scope)
:&: [not, in mathcomp.algebra.mxalgebra] (in matrix_set_scope)
:&: [not, in mathcomp.algebra.mxalgebra] (in matrix_set_scope)
:=: [not, in mathcomp.algebra.mxalgebra] (in matrix_set_scope)
:=: [not, in mathcomp.algebra.mxalgebra] (in matrix_set_scope)
:\: [not, in mathcomp.algebra.mxalgebra] (in matrix_set_scope)
:\: [not, in mathcomp.algebra.mxalgebra] (in matrix_set_scope)
< [not, in mathcomp.algebra.mxalgebra] (in matrix_set_scope)
< [not, in mathcomp.algebra.mxalgebra] (in matrix_set_scope)
< < [not, in mathcomp.algebra.mxalgebra] (in matrix_set_scope)
< <= [not, in mathcomp.algebra.mxalgebra] (in matrix_set_scope)
<= [not, in mathcomp.algebra.mxalgebra] (in matrix_set_scope)
<= [not, in mathcomp.algebra.mxalgebra] (in matrix_set_scope)
<= < [not, in mathcomp.algebra.mxalgebra] (in matrix_set_scope)
<= <= [not, in mathcomp.algebra.mxalgebra] (in matrix_set_scope)
<= <= [not, in mathcomp.algebra.mxalgebra] (in matrix_set_scope)
== [not, in mathcomp.algebra.mxalgebra] (in matrix_set_scope)
== [not, in mathcomp.algebra.mxalgebra] (in matrix_set_scope)
\in [not, in mathcomp.algebra.mxalgebra] (in matrix_set_scope)
^! [not, in mathcomp.algebra.spectral] (in matrix_set_scope)
^! [not, in mathcomp.algebra.sesquilinear] (in matrix_set_scope)
^C [not, in mathcomp.algebra.mxalgebra] (in matrix_set_scope)
^C [not, in mathcomp.algebra.mxalgebra] (in matrix_set_scope)

nat_scope

#| | [not, in mathcomp.boot.fintype] (in nat_scope)
'C ( , ) [not, in mathcomp.boot.binomial] (in nat_scope)
[ Num of ] [not, in mathcomp.boot.ssrnat] (in nat_scope)
[ arg max_ ( > ) ] [not, in mathcomp.boot.fintype] (in nat_scope)
[ arg max_ ( > in ) ] [not, in mathcomp.boot.fintype] (in nat_scope)
[ arg max_ ( > | ) ] [not, in mathcomp.boot.fintype] (in nat_scope)
[ arg min_ ( < ) ] [not, in mathcomp.boot.fintype] (in nat_scope)
[ arg min_ ( < in ) ] [not, in mathcomp.boot.fintype] (in nat_scope)
[ arg min_ ( < | ) ] [not, in mathcomp.boot.fintype] (in nat_scope)
[ arg[ ]_( < ) ] [not, in mathcomp.boot.fintype] (in nat_scope)
[ arg[ ]_( < in ) ] [not, in mathcomp.boot.fintype] (in nat_scope)
[ arg[ ]_( < | ) ] [not, in mathcomp.boot.fintype] (in nat_scope)
\dim [not, in mathcomp.algebra.vector] (in nat_scope)
\dim_ [not, in mathcomp.field.falgebra] (in nat_scope)
\max_ ( : ) [not, in mathcomp.boot.bigop] (in nat_scope)
\max_ ( : | ) [not, in mathcomp.boot.bigop] (in nat_scope)
\max_ ( < ) [not, in mathcomp.boot.bigop] (in nat_scope)
\max_ ( < | ) [not, in mathcomp.boot.bigop] (in nat_scope)
\max_ ( <- ) [not, in mathcomp.boot.bigop] (in nat_scope)
\max_ ( <- | ) [not, in mathcomp.boot.bigop] (in nat_scope)
\max_ ( <= < ) [not, in mathcomp.boot.bigop] (in nat_scope)
\max_ ( <= < | ) [not, in mathcomp.boot.bigop] (in nat_scope)
\max_ ( in ) [not, in mathcomp.boot.bigop] (in nat_scope)
\max_ ( in | ) [not, in mathcomp.boot.bigop] (in nat_scope)
\max_ ( | ) [not, in mathcomp.boot.bigop] (in nat_scope)
\max_ [not, in mathcomp.boot.bigop] (in nat_scope)
\p i ( ) [not, in mathcomp.boot.prime] (in nat_scope)
\pi ( ) [not, in mathcomp.boot.prime] (in nat_scope)
\prod_ ( : ) [not, in mathcomp.boot.bigop] (in nat_scope)
\prod_ ( : | ) [not, in mathcomp.boot.bigop] (in nat_scope)
\prod_ ( < ) [not, in mathcomp.boot.bigop] (in nat_scope)
\prod_ ( < | ) [not, in mathcomp.boot.bigop] (in nat_scope)
\prod_ ( <- ) [not, in mathcomp.boot.bigop] (in nat_scope)
\prod_ ( <- | ) [not, in mathcomp.boot.bigop] (in nat_scope)
\prod_ ( <= < ) [not, in mathcomp.boot.bigop] (in nat_scope)
\prod_ ( <= < | ) [not, in mathcomp.boot.bigop] (in nat_scope)
\prod_ ( in ) [not, in mathcomp.boot.bigop] (in nat_scope)
\prod_ ( in | ) [not, in mathcomp.boot.bigop] (in nat_scope)
\prod_ ( | ) [not, in mathcomp.boot.bigop] (in nat_scope)
\prod_ [not, in mathcomp.boot.bigop] (in nat_scope)
\rank [not, in mathcomp.algebra.mxalgebra] (in nat_scope)
\rank [not, in mathcomp.algebra.mxalgebra] (in nat_scope)
\sum_ ( : ) [not, in mathcomp.boot.bigop] (in nat_scope)
\sum_ ( : | ) [not, in mathcomp.boot.bigop] (in nat_scope)
\sum_ ( < ) [not, in mathcomp.boot.bigop] (in nat_scope)
\sum_ ( < | ) [not, in mathcomp.boot.bigop] (in nat_scope)
\sum_ ( <- ) [not, in mathcomp.boot.bigop] (in nat_scope)
\sum_ ( <- | ) [not, in mathcomp.boot.bigop] (in nat_scope)
\sum_ ( <= < ) [not, in mathcomp.boot.bigop] (in nat_scope)
\sum_ ( <= < | ) [not, in mathcomp.boot.bigop] (in nat_scope)
\sum_ ( in ) [not, in mathcomp.boot.bigop] (in nat_scope)
\sum_ ( in | ) [not, in mathcomp.boot.bigop] (in nat_scope)
\sum_ ( | ) [not, in mathcomp.boot.bigop] (in nat_scope)
\sum_ [not, in mathcomp.boot.bigop] (in nat_scope)
`| | [not, in mathcomp.algebra.ssrint] (in nat_scope)
`| | [not, in mathcomp.algebra.ssrint] (in nat_scope)
!= %[mod ] [not, in mathcomp.boot.div] (in nat_scope)
%% [not, in mathcomp.boot.div] (in nat_scope)
%/ [not, in mathcomp.boot.div] (in nat_scope)
%| [not, in mathcomp.boot.div] (in nat_scope)
* [not, in mathcomp.boot.ssrnat] (in nat_scope)
* [not, in mathcomp.boot.ssrnat] (in nat_scope)
+ [not, in mathcomp.boot.ssrnat] (in nat_scope)
+ [not, in mathcomp.boot.ssrnat] (in nat_scope)
- [not, in mathcomp.boot.ssrnat] (in nat_scope)
.*2 [not, in mathcomp.boot.ssrnat] (in nat_scope)
.*2 [not, in mathcomp.boot.ssrnat] (in nat_scope)
.+1 [not, in mathcomp.boot.ssrnat] (in nat_scope)
.+2 [not, in mathcomp.boot.ssrnat] (in nat_scope)
.+3 [not, in mathcomp.boot.ssrnat] (in nat_scope)
.+4 [not, in mathcomp.boot.ssrnat] (in nat_scope)
.-1 [not, in mathcomp.boot.ssrnat] (in nat_scope)
.-2 [not, in mathcomp.boot.ssrnat] (in nat_scope)
.-nat [not, in mathcomp.boot.prime] (in nat_scope)
./2 [not, in mathcomp.boot.ssrnat] (in nat_scope)
< [not, in mathcomp.boot.ssrnat] (in nat_scope)
< < [not, in mathcomp.boot.ssrnat] (in nat_scope)
< <= [not, in mathcomp.boot.ssrnat] (in nat_scope)
<= [not, in mathcomp.boot.ssrnat] (in nat_scope)
<= < [not, in mathcomp.boot.ssrnat] (in nat_scope)
<= <= [not, in mathcomp.boot.ssrnat] (in nat_scope)
<= ?= iff [not, in mathcomp.boot.ssrnat] (in nat_scope)
<> %[mod ] [not, in mathcomp.boot.div] (in nat_scope)
= %[mod ] [not, in mathcomp.boot.div] (in nat_scope)
== %[mod ] [not, in mathcomp.boot.div] (in nat_scope)
> [not, in mathcomp.boot.ssrnat] (in nat_scope)
>= [not, in mathcomp.boot.ssrnat] (in nat_scope)
^' [not, in mathcomp.boot.prime] (in nat_scope)
^ [not, in mathcomp.boot.ssrnat] (in nat_scope)
^ [not, in mathcomp.boot.ssrnat] (in nat_scope)
^? :: [not, in mathcomp.boot.prime] (in nat_scope)
^_ [not, in mathcomp.boot.binomial] (in nat_scope)
`! [not, in mathcomp.boot.ssrnat] (in nat_scope)
`_ [not, in mathcomp.boot.prime] (in nat_scope)

order_scope

+oo [not, in mathcomp.algebra.interval] (in order_scope)
-oo [not, in mathcomp.algebra.interval] (in order_scope)
< [not, in mathcomp.order.preorder] (in order_scope)
< :> [not, in mathcomp.order.preorder] (in order_scope)
<= [not, in mathcomp.order.preorder] (in order_scope)
<= :> [not, in mathcomp.order.preorder] (in order_scope)
<=^d [not, in mathcomp.order.preorder] (in order_scope)
<=^d :> [not, in mathcomp.order.preorder] (in order_scope)
<=^l [not, in mathcomp.order.preorder] (in order_scope)
<=^l [not, in mathcomp.order.preorder] (in order_scope)
<=^l :> [not, in mathcomp.order.preorder] (in order_scope)
<=^l :> [not, in mathcomp.order.preorder] (in order_scope)
<=^p [not, in mathcomp.order.preorder] (in order_scope)
<=^p :> [not, in mathcomp.order.preorder] (in order_scope)
<=^sp [not, in mathcomp.order.preorder] (in order_scope)
<=^sp :> [not, in mathcomp.order.preorder] (in order_scope)
<^d [not, in mathcomp.order.preorder] (in order_scope)
<^d :> [not, in mathcomp.order.preorder] (in order_scope)
<^l [not, in mathcomp.order.preorder] (in order_scope)
<^l [not, in mathcomp.order.preorder] (in order_scope)
<^l :> [not, in mathcomp.order.preorder] (in order_scope)
<^l :> [not, in mathcomp.order.preorder] (in order_scope)
<^p [not, in mathcomp.order.preorder] (in order_scope)
<^p :> [not, in mathcomp.order.preorder] (in order_scope)
<^sp [not, in mathcomp.order.preorder] (in order_scope)
<^sp :> [not, in mathcomp.order.preorder] (in order_scope)
> [not, in mathcomp.order.preorder] (in order_scope)
> :> [not, in mathcomp.order.preorder] (in order_scope)
>< [not, in mathcomp.order.preorder] (in order_scope)
>< :> [not, in mathcomp.order.preorder] (in order_scope)
><^d [not, in mathcomp.order.preorder] (in order_scope)
><^d :> [not, in mathcomp.order.preorder] (in order_scope)
><^l [not, in mathcomp.order.preorder] (in order_scope)
><^l [not, in mathcomp.order.preorder] (in order_scope)
><^l :> [not, in mathcomp.order.preorder] (in order_scope)
><^l :> [not, in mathcomp.order.preorder] (in order_scope)
><^p [not, in mathcomp.order.preorder] (in order_scope)
><^p :> [not, in mathcomp.order.preorder] (in order_scope)
><^sp [not, in mathcomp.order.preorder] (in order_scope)
><^sp :> [not, in mathcomp.order.preorder] (in order_scope)
>= [not, in mathcomp.order.preorder] (in order_scope)
>= :> [not, in mathcomp.order.preorder] (in order_scope)
>=< [not, in mathcomp.order.preorder] (in order_scope)
>=< :> [not, in mathcomp.order.preorder] (in order_scope)
>=<^d [not, in mathcomp.order.preorder] (in order_scope)
>=<^d :> [not, in mathcomp.order.preorder] (in order_scope)
>=<^l [not, in mathcomp.order.preorder] (in order_scope)
>=<^l [not, in mathcomp.order.preorder] (in order_scope)
>=<^l :> [not, in mathcomp.order.preorder] (in order_scope)
>=<^l :> [not, in mathcomp.order.preorder] (in order_scope)
>=<^p [not, in mathcomp.order.preorder] (in order_scope)
>=<^p :> [not, in mathcomp.order.preorder] (in order_scope)
>=<^sp [not, in mathcomp.order.preorder] (in order_scope)
>=<^sp :> [not, in mathcomp.order.preorder] (in order_scope)
>=^d [not, in mathcomp.order.preorder] (in order_scope)
>=^d :> [not, in mathcomp.order.preorder] (in order_scope)
>=^l [not, in mathcomp.order.preorder] (in order_scope)
>=^l [not, in mathcomp.order.preorder] (in order_scope)
>=^l :> [not, in mathcomp.order.preorder] (in order_scope)
>=^l :> [not, in mathcomp.order.preorder] (in order_scope)
>=^p [not, in mathcomp.order.preorder] (in order_scope)
>=^p :> [not, in mathcomp.order.preorder] (in order_scope)
>=^sp [not, in mathcomp.order.preorder] (in order_scope)
>=^sp :> [not, in mathcomp.order.preorder] (in order_scope)
>^d [not, in mathcomp.order.preorder] (in order_scope)
>^d :> [not, in mathcomp.order.preorder] (in order_scope)
>^l [not, in mathcomp.order.preorder] (in order_scope)
>^l [not, in mathcomp.order.preorder] (in order_scope)
>^l :> [not, in mathcomp.order.preorder] (in order_scope)
>^l :> [not, in mathcomp.order.preorder] (in order_scope)
>^p [not, in mathcomp.order.preorder] (in order_scope)
>^p :> [not, in mathcomp.order.preorder] (in order_scope)
>^sp [not, in mathcomp.order.preorder] (in order_scope)
>^sp :> [not, in mathcomp.order.preorder] (in order_scope)
[ arg max_ ( > ) ] [not, in mathcomp.order.preorder] (in order_scope)
[ arg max_ ( > in ) ] [not, in mathcomp.order.preorder] (in order_scope)
[ arg max_ ( > | ) ] [not, in mathcomp.order.preorder] (in order_scope)
[ arg min_ ( < ) ] [not, in mathcomp.order.preorder] (in order_scope)
[ arg min_ ( < in ) ] [not, in mathcomp.order.preorder] (in order_scope)
[ arg min_ ( < | ) ] [not, in mathcomp.order.preorder] (in order_scope)
\bot [not, in mathcomp.order.preorder] (in order_scope)
\bot^d [not, in mathcomp.order.preorder] (in order_scope)
\gcd_ ( : ) [not, in mathcomp.order.order] (in order_scope)
\gcd_ ( : | ) [not, in mathcomp.order.order] (in order_scope)
\gcd_ ( < ) [not, in mathcomp.order.order] (in order_scope)
\gcd_ ( < | ) [not, in mathcomp.order.order] (in order_scope)
\gcd_ ( <- ) [not, in mathcomp.order.order] (in order_scope)
\gcd_ ( <- | ) [not, in mathcomp.order.order] (in order_scope)
\gcd_ ( <= < ) [not, in mathcomp.order.order] (in order_scope)
\gcd_ ( <= < | ) [not, in mathcomp.order.order] (in order_scope)
\gcd_ ( in ) [not, in mathcomp.order.order] (in order_scope)
\gcd_ ( in | ) [not, in mathcomp.order.order] (in order_scope)
\gcd_ ( | ) [not, in mathcomp.order.order] (in order_scope)
\gcd_ [not, in mathcomp.order.order] (in order_scope)
\join^d_ ( : ) [not, in mathcomp.order.order] (in order_scope)
\join^d_ ( : | ) [not, in mathcomp.order.order] (in order_scope)
\join^d_ ( < ) [not, in mathcomp.order.order] (in order_scope)
\join^d_ ( < | ) [not, in mathcomp.order.order] (in order_scope)
\join^d_ ( <- ) [not, in mathcomp.order.order] (in order_scope)
\join^d_ ( <- | ) [not, in mathcomp.order.order] (in order_scope)
\join^d_ ( <= < ) [not, in mathcomp.order.order] (in order_scope)
\join^d_ ( <= < | ) [not, in mathcomp.order.order] (in order_scope)
\join^d_ ( in ) [not, in mathcomp.order.order] (in order_scope)
\join^d_ ( in | ) [not, in mathcomp.order.order] (in order_scope)
\join^d_ ( | ) [not, in mathcomp.order.order] (in order_scope)
\join^d_ [not, in mathcomp.order.order] (in order_scope)
\join^l_ ( : ) [not, in mathcomp.order.order] (in order_scope)
\join^l_ ( : ) [not, in mathcomp.order.order] (in order_scope)
\join^l_ ( : | ) [not, in mathcomp.order.order] (in order_scope)
\join^l_ ( : | ) [not, in mathcomp.order.order] (in order_scope)
\join^l_ ( < ) [not, in mathcomp.order.order] (in order_scope)
\join^l_ ( < ) [not, in mathcomp.order.order] (in order_scope)
\join^l_ ( < | ) [not, in mathcomp.order.order] (in order_scope)
\join^l_ ( < | ) [not, in mathcomp.order.order] (in order_scope)
\join^l_ ( <- ) [not, in mathcomp.order.order] (in order_scope)
\join^l_ ( <- ) [not, in mathcomp.order.order] (in order_scope)
\join^l_ ( <- | ) [not, in mathcomp.order.order] (in order_scope)
\join^l_ ( <- | ) [not, in mathcomp.order.order] (in order_scope)
\join^l_ ( <= < ) [not, in mathcomp.order.order] (in order_scope)
\join^l_ ( <= < ) [not, in mathcomp.order.order] (in order_scope)
\join^l_ ( <= < | ) [not, in mathcomp.order.order] (in order_scope)
\join^l_ ( <= < | ) [not, in mathcomp.order.order] (in order_scope)
\join^l_ ( in ) [not, in mathcomp.order.order] (in order_scope)
\join^l_ ( in ) [not, in mathcomp.order.order] (in order_scope)
\join^l_ ( in | ) [not, in mathcomp.order.order] (in order_scope)
\join^l_ ( in | ) [not, in mathcomp.order.order] (in order_scope)
\join^l_ ( | ) [not, in mathcomp.order.order] (in order_scope)
\join^l_ ( | ) [not, in mathcomp.order.order] (in order_scope)
\join^l_ [not, in mathcomp.order.order] (in order_scope)
\join^l_ [not, in mathcomp.order.order] (in order_scope)
\join^p_ ( : ) [not, in mathcomp.order.order] (in order_scope)
\join^p_ ( : | ) [not, in mathcomp.order.order] (in order_scope)
\join^p_ ( < ) [not, in mathcomp.order.order] (in order_scope)
\join^p_ ( < | ) [not, in mathcomp.order.order] (in order_scope)
\join^p_ ( <- ) [not, in mathcomp.order.order] (in order_scope)
\join^p_ ( <- | ) [not, in mathcomp.order.order] (in order_scope)
\join^p_ ( <= < ) [not, in mathcomp.order.order] (in order_scope)
\join^p_ ( <= < | ) [not, in mathcomp.order.order] (in order_scope)
\join^p_ ( in ) [not, in mathcomp.order.order] (in order_scope)
\join^p_ ( in | ) [not, in mathcomp.order.order] (in order_scope)
\join^p_ ( | ) [not, in mathcomp.order.order] (in order_scope)
\join^p_ [not, in mathcomp.order.order] (in order_scope)
\join^sp_ ( : ) [not, in mathcomp.order.order] (in order_scope)
\join^sp_ ( : | ) [not, in mathcomp.order.order] (in order_scope)
\join^sp_ ( < ) [not, in mathcomp.order.order] (in order_scope)
\join^sp_ ( < | ) [not, in mathcomp.order.order] (in order_scope)
\join^sp_ ( <- ) [not, in mathcomp.order.order] (in order_scope)
\join^sp_ ( <- | ) [not, in mathcomp.order.order] (in order_scope)
\join^sp_ ( <= < ) [not, in mathcomp.order.order] (in order_scope)
\join^sp_ ( <= < | ) [not, in mathcomp.order.order] (in order_scope)
\join^sp_ ( in ) [not, in mathcomp.order.order] (in order_scope)
\join^sp_ ( in | ) [not, in mathcomp.order.order] (in order_scope)
\join^sp_ ( | ) [not, in mathcomp.order.order] (in order_scope)
\join^sp_ [not, in mathcomp.order.order] (in order_scope)
\join_ ( : ) [not, in mathcomp.order.order] (in order_scope)
\join_ ( : | ) [not, in mathcomp.order.order] (in order_scope)
\join_ ( < ) [not, in mathcomp.order.order] (in order_scope)
\join_ ( < | ) [not, in mathcomp.order.order] (in order_scope)
\join_ ( <- ) [not, in mathcomp.order.order] (in order_scope)
\join_ ( <- | ) [not, in mathcomp.order.order] (in order_scope)
\join_ ( <= < ) [not, in mathcomp.order.order] (in order_scope)
\join_ ( <= < | ) [not, in mathcomp.order.order] (in order_scope)
\join_ ( in ) [not, in mathcomp.order.order] (in order_scope)
\join_ ( in | ) [not, in mathcomp.order.order] (in order_scope)
\join_ ( | ) [not, in mathcomp.order.order] (in order_scope)
\join_ [not, in mathcomp.order.order] (in order_scope)
\lcm_ ( : ) [not, in mathcomp.order.order] (in order_scope)
\lcm_ ( : | ) [not, in mathcomp.order.order] (in order_scope)
\lcm_ ( < ) [not, in mathcomp.order.order] (in order_scope)
\lcm_ ( < | ) [not, in mathcomp.order.order] (in order_scope)
\lcm_ ( <- ) [not, in mathcomp.order.order] (in order_scope)
\lcm_ ( <- | ) [not, in mathcomp.order.order] (in order_scope)
\lcm_ ( <= < ) [not, in mathcomp.order.order] (in order_scope)
\lcm_ ( <= < | ) [not, in mathcomp.order.order] (in order_scope)
\lcm_ ( in ) [not, in mathcomp.order.order] (in order_scope)
\lcm_ ( in | ) [not, in mathcomp.order.order] (in order_scope)
\lcm_ ( | ) [not, in mathcomp.order.order] (in order_scope)
\lcm_ [not, in mathcomp.order.order] (in order_scope)
\max^d_ ( : ) [not, in mathcomp.order.preorder] (in order_scope)
\max^d_ ( : | ) [not, in mathcomp.order.preorder] (in order_scope)
\max^d_ ( < ) [not, in mathcomp.order.preorder] (in order_scope)
\max^d_ ( < ) [not, in mathcomp.order.preorder] (in order_scope)
\max^d_ ( < | ) [not, in mathcomp.order.preorder] (in order_scope)
\max^d_ ( <- | ) [not, in mathcomp.order.preorder] (in order_scope)
\max^d_ ( <= < ) [not, in mathcomp.order.preorder] (in order_scope)
\max^d_ ( <= < | ) [not, in mathcomp.order.preorder] (in order_scope)
\max^d_ ( in ) [not, in mathcomp.order.preorder] (in order_scope)
\max^d_ ( in | ) [not, in mathcomp.order.preorder] (in order_scope)
\max^d_ ( | ) [not, in mathcomp.order.preorder] (in order_scope)
\max^d_ [not, in mathcomp.order.preorder] (in order_scope)
\max^l_ ( : ) [not, in mathcomp.order.order] (in order_scope)
\max^l_ ( : ) [not, in mathcomp.order.order] (in order_scope)
\max^l_ ( : | ) [not, in mathcomp.order.order] (in order_scope)
\max^l_ ( : | ) [not, in mathcomp.order.order] (in order_scope)
\max^l_ ( < ) [not, in mathcomp.order.order] (in order_scope)
\max^l_ ( < ) [not, in mathcomp.order.order] (in order_scope)
\max^l_ ( < ) [not, in mathcomp.order.order] (in order_scope)
\max^l_ ( < ) [not, in mathcomp.order.order] (in order_scope)
\max^l_ ( < | ) [not, in mathcomp.order.order] (in order_scope)
\max^l_ ( < | ) [not, in mathcomp.order.order] (in order_scope)
\max^l_ ( <- | ) [not, in mathcomp.order.order] (in order_scope)
\max^l_ ( <- | ) [not, in mathcomp.order.order] (in order_scope)
\max^l_ ( <= < ) [not, in mathcomp.order.order] (in order_scope)
\max^l_ ( <= < ) [not, in mathcomp.order.order] (in order_scope)
\max^l_ ( <= < | ) [not, in mathcomp.order.order] (in order_scope)
\max^l_ ( <= < | ) [not, in mathcomp.order.order] (in order_scope)
\max^l_ ( in ) [not, in mathcomp.order.order] (in order_scope)
\max^l_ ( in ) [not, in mathcomp.order.order] (in order_scope)
\max^l_ ( in | ) [not, in mathcomp.order.order] (in order_scope)
\max^l_ ( in | ) [not, in mathcomp.order.order] (in order_scope)
\max^l_ ( | ) [not, in mathcomp.order.order] (in order_scope)
\max^l_ ( | ) [not, in mathcomp.order.order] (in order_scope)
\max^l_ [not, in mathcomp.order.order] (in order_scope)
\max^l_ [not, in mathcomp.order.order] (in order_scope)
\max^p_ ( : ) [not, in mathcomp.order.order] (in order_scope)
\max^p_ ( : | ) [not, in mathcomp.order.order] (in order_scope)
\max^p_ ( < ) [not, in mathcomp.order.order] (in order_scope)
\max^p_ ( < ) [not, in mathcomp.order.order] (in order_scope)
\max^p_ ( < | ) [not, in mathcomp.order.order] (in order_scope)
\max^p_ ( <- | ) [not, in mathcomp.order.order] (in order_scope)
\max^p_ ( <= < ) [not, in mathcomp.order.order] (in order_scope)
\max^p_ ( <= < | ) [not, in mathcomp.order.order] (in order_scope)
\max^p_ ( in ) [not, in mathcomp.order.order] (in order_scope)
\max^p_ ( in | ) [not, in mathcomp.order.order] (in order_scope)
\max^p_ ( | ) [not, in mathcomp.order.order] (in order_scope)
\max^p_ [not, in mathcomp.order.order] (in order_scope)
\max^sp_ ( : ) [not, in mathcomp.order.order] (in order_scope)
\max^sp_ ( : | ) [not, in mathcomp.order.order] (in order_scope)
\max^sp_ ( < ) [not, in mathcomp.order.order] (in order_scope)
\max^sp_ ( < ) [not, in mathcomp.order.order] (in order_scope)
\max^sp_ ( < | ) [not, in mathcomp.order.order] (in order_scope)
\max^sp_ ( <- | ) [not, in mathcomp.order.order] (in order_scope)
\max^sp_ ( <= < ) [not, in mathcomp.order.order] (in order_scope)
\max^sp_ ( <= < | ) [not, in mathcomp.order.order] (in order_scope)
\max^sp_ ( in ) [not, in mathcomp.order.order] (in order_scope)
\max^sp_ ( in | ) [not, in mathcomp.order.order] (in order_scope)
\max^sp_ ( | ) [not, in mathcomp.order.order] (in order_scope)
\max^sp_ [not, in mathcomp.order.order] (in order_scope)
\max_ ( : ) [not, in mathcomp.order.preorder] (in order_scope)
\max_ ( : | ) [not, in mathcomp.order.preorder] (in order_scope)
\max_ ( < ) [not, in mathcomp.order.preorder] (in order_scope)
\max_ ( < ) [not, in mathcomp.order.preorder] (in order_scope)
\max_ ( < | ) [not, in mathcomp.order.preorder] (in order_scope)
\max_ ( <- | ) [not, in mathcomp.order.preorder] (in order_scope)
\max_ ( <= < ) [not, in mathcomp.order.preorder] (in order_scope)
\max_ ( <= < | ) [not, in mathcomp.order.preorder] (in order_scope)
\max_ ( in ) [not, in mathcomp.order.preorder] (in order_scope)
\max_ ( in | ) [not, in mathcomp.order.preorder] (in order_scope)
\max_ ( | ) [not, in mathcomp.order.preorder] (in order_scope)
\max_ [not, in mathcomp.order.preorder] (in order_scope)
\meet^d_ ( : ) [not, in mathcomp.order.order] (in order_scope)
\meet^d_ ( : | ) [not, in mathcomp.order.order] (in order_scope)
\meet^d_ ( < ) [not, in mathcomp.order.order] (in order_scope)
\meet^d_ ( < | ) [not, in mathcomp.order.order] (in order_scope)
\meet^d_ ( <- ) [not, in mathcomp.order.order] (in order_scope)
\meet^d_ ( <- | ) [not, in mathcomp.order.order] (in order_scope)
\meet^d_ ( <= < ) [not, in mathcomp.order.order] (in order_scope)
\meet^d_ ( <= < | ) [not, in mathcomp.order.order] (in order_scope)
\meet^d_ ( in ) [not, in mathcomp.order.order] (in order_scope)
\meet^d_ ( in | ) [not, in mathcomp.order.order] (in order_scope)
\meet^d_ ( | ) [not, in mathcomp.order.order] (in order_scope)
\meet^d_ [not, in mathcomp.order.order] (in order_scope)
\meet^l_ ( : ) [not, in mathcomp.order.order] (in order_scope)
\meet^l_ ( : ) [not, in mathcomp.order.order] (in order_scope)
\meet^l_ ( : | ) [not, in mathcomp.order.order] (in order_scope)
\meet^l_ ( : | ) [not, in mathcomp.order.order] (in order_scope)
\meet^l_ ( < ) [not, in mathcomp.order.order] (in order_scope)
\meet^l_ ( < ) [not, in mathcomp.order.order] (in order_scope)
\meet^l_ ( < | ) [not, in mathcomp.order.order] (in order_scope)
\meet^l_ ( < | ) [not, in mathcomp.order.order] (in order_scope)
\meet^l_ ( <- ) [not, in mathcomp.order.order] (in order_scope)
\meet^l_ ( <- ) [not, in mathcomp.order.order] (in order_scope)
\meet^l_ ( <- | ) [not, in mathcomp.order.order] (in order_scope)
\meet^l_ ( <- | ) [not, in mathcomp.order.order] (in order_scope)
\meet^l_ ( <= < ) [not, in mathcomp.order.order] (in order_scope)
\meet^l_ ( <= < ) [not, in mathcomp.order.order] (in order_scope)
\meet^l_ ( <= < | ) [not, in mathcomp.order.order] (in order_scope)
\meet^l_ ( <= < | ) [not, in mathcomp.order.order] (in order_scope)
\meet^l_ ( in ) [not, in mathcomp.order.order] (in order_scope)
\meet^l_ ( in ) [not, in mathcomp.order.order] (in order_scope)
\meet^l_ ( in | ) [not, in mathcomp.order.order] (in order_scope)
\meet^l_ ( in | ) [not, in mathcomp.order.order] (in order_scope)
\meet^l_ ( | ) [not, in mathcomp.order.order] (in order_scope)
\meet^l_ ( | ) [not, in mathcomp.order.order] (in order_scope)
\meet^l_ [not, in mathcomp.order.order] (in order_scope)
\meet^l_ [not, in mathcomp.order.order] (in order_scope)
\meet^p_ ( : ) [not, in mathcomp.order.order] (in order_scope)
\meet^p_ ( : | ) [not, in mathcomp.order.order] (in order_scope)
\meet^p_ ( < ) [not, in mathcomp.order.order] (in order_scope)
\meet^p_ ( < | ) [not, in mathcomp.order.order] (in order_scope)
\meet^p_ ( <- ) [not, in mathcomp.order.order] (in order_scope)
\meet^p_ ( <- | ) [not, in mathcomp.order.order] (in order_scope)
\meet^p_ ( <= < ) [not, in mathcomp.order.order] (in order_scope)
\meet^p_ ( <= < | ) [not, in mathcomp.order.order] (in order_scope)
\meet^p_ ( in ) [not, in mathcomp.order.order] (in order_scope)
\meet^p_ ( in | ) [not, in mathcomp.order.order] (in order_scope)
\meet^p_ ( | ) [not, in mathcomp.order.order] (in order_scope)
\meet^p_ [not, in mathcomp.order.order] (in order_scope)
\meet^sp_ ( : ) [not, in mathcomp.order.order] (in order_scope)
\meet^sp_ ( : | ) [not, in mathcomp.order.order] (in order_scope)
\meet^sp_ ( < ) [not, in mathcomp.order.order] (in order_scope)
\meet^sp_ ( < | ) [not, in mathcomp.order.order] (in order_scope)
\meet^sp_ ( <- ) [not, in mathcomp.order.order] (in order_scope)
\meet^sp_ ( <- | ) [not, in mathcomp.order.order] (in order_scope)
\meet^sp_ ( <= < ) [not, in mathcomp.order.order] (in order_scope)
\meet^sp_ ( <= < | ) [not, in mathcomp.order.order] (in order_scope)
\meet^sp_ ( in ) [not, in mathcomp.order.order] (in order_scope)
\meet^sp_ ( in | ) [not, in mathcomp.order.order] (in order_scope)
\meet^sp_ ( | ) [not, in mathcomp.order.order] (in order_scope)
\meet^sp_ [not, in mathcomp.order.order] (in order_scope)
\meet_ ( : ) [not, in mathcomp.order.order] (in order_scope)
\meet_ ( : | ) [not, in mathcomp.order.order] (in order_scope)
\meet_ ( < ) [not, in mathcomp.order.order] (in order_scope)
\meet_ ( < | ) [not, in mathcomp.order.order] (in order_scope)
\meet_ ( <- ) [not, in mathcomp.order.order] (in order_scope)
\meet_ ( <- | ) [not, in mathcomp.order.order] (in order_scope)
\meet_ ( <= < ) [not, in mathcomp.order.order] (in order_scope)
\meet_ ( <= < | ) [not, in mathcomp.order.order] (in order_scope)
\meet_ ( in ) [not, in mathcomp.order.order] (in order_scope)
\meet_ ( in | ) [not, in mathcomp.order.order] (in order_scope)
\meet_ ( | ) [not, in mathcomp.order.order] (in order_scope)
\meet_ [not, in mathcomp.order.order] (in order_scope)
\min^d_ ( : ) [not, in mathcomp.order.preorder] (in order_scope)
\min^d_ ( : | ) [not, in mathcomp.order.preorder] (in order_scope)
\min^d_ ( < ) [not, in mathcomp.order.preorder] (in order_scope)
\min^d_ ( < ) [not, in mathcomp.order.preorder] (in order_scope)
\min^d_ ( < | ) [not, in mathcomp.order.preorder] (in order_scope)
\min^d_ ( <- | ) [not, in mathcomp.order.preorder] (in order_scope)
\min^d_ ( <= < ) [not, in mathcomp.order.preorder] (in order_scope)
\min^d_ ( <= < | ) [not, in mathcomp.order.preorder] (in order_scope)
\min^d_ ( in ) [not, in mathcomp.order.preorder] (in order_scope)
\min^d_ ( in | ) [not, in mathcomp.order.preorder] (in order_scope)
\min^d_ ( | ) [not, in mathcomp.order.preorder] (in order_scope)
\min^d_ [not, in mathcomp.order.preorder] (in order_scope)
\min^l_ ( : ) [not, in mathcomp.order.order] (in order_scope)
\min^l_ ( : ) [not, in mathcomp.order.order] (in order_scope)
\min^l_ ( : | ) [not, in mathcomp.order.order] (in order_scope)
\min^l_ ( : | ) [not, in mathcomp.order.order] (in order_scope)
\min^l_ ( < ) [not, in mathcomp.order.order] (in order_scope)
\min^l_ ( < ) [not, in mathcomp.order.order] (in order_scope)
\min^l_ ( < ) [not, in mathcomp.order.order] (in order_scope)
\min^l_ ( < ) [not, in mathcomp.order.order] (in order_scope)
\min^l_ ( < | ) [not, in mathcomp.order.order] (in order_scope)
\min^l_ ( < | ) [not, in mathcomp.order.order] (in order_scope)
\min^l_ ( <- | ) [not, in mathcomp.order.order] (in order_scope)
\min^l_ ( <- | ) [not, in mathcomp.order.order] (in order_scope)
\min^l_ ( <= < ) [not, in mathcomp.order.order] (in order_scope)
\min^l_ ( <= < ) [not, in mathcomp.order.order] (in order_scope)
\min^l_ ( <= < | ) [not, in mathcomp.order.order] (in order_scope)
\min^l_ ( <= < | ) [not, in mathcomp.order.order] (in order_scope)
\min^l_ ( in ) [not, in mathcomp.order.order] (in order_scope)
\min^l_ ( in ) [not, in mathcomp.order.order] (in order_scope)
\min^l_ ( in | ) [not, in mathcomp.order.order] (in order_scope)
\min^l_ ( in | ) [not, in mathcomp.order.order] (in order_scope)
\min^l_ ( | ) [not, in mathcomp.order.order] (in order_scope)
\min^l_ ( | ) [not, in mathcomp.order.order] (in order_scope)
\min^l_ [not, in mathcomp.order.order] (in order_scope)
\min^l_ [not, in mathcomp.order.order] (in order_scope)
\min^p_ ( : ) [not, in mathcomp.order.order] (in order_scope)
\min^p_ ( : | ) [not, in mathcomp.order.order] (in order_scope)
\min^p_ ( < ) [not, in mathcomp.order.order] (in order_scope)
\min^p_ ( < ) [not, in mathcomp.order.order] (in order_scope)
\min^p_ ( < | ) [not, in mathcomp.order.order] (in order_scope)
\min^p_ ( <- | ) [not, in mathcomp.order.order] (in order_scope)
\min^p_ ( <= < ) [not, in mathcomp.order.order] (in order_scope)
\min^p_ ( <= < | ) [not, in mathcomp.order.order] (in order_scope)
\min^p_ ( in ) [not, in mathcomp.order.order] (in order_scope)
\min^p_ ( in | ) [not, in mathcomp.order.order] (in order_scope)
\min^p_ ( | ) [not, in mathcomp.order.order] (in order_scope)
\min^p_ [not, in mathcomp.order.order] (in order_scope)
\min^sp_ ( : ) [not, in mathcomp.order.order] (in order_scope)
\min^sp_ ( : | ) [not, in mathcomp.order.order] (in order_scope)
\min^sp_ ( < ) [not, in mathcomp.order.order] (in order_scope)
\min^sp_ ( < ) [not, in mathcomp.order.order] (in order_scope)
\min^sp_ ( < | ) [not, in mathcomp.order.order] (in order_scope)
\min^sp_ ( <- | ) [not, in mathcomp.order.order] (in order_scope)
\min^sp_ ( <= < ) [not, in mathcomp.order.order] (in order_scope)
\min^sp_ ( <= < | ) [not, in mathcomp.order.order] (in order_scope)
\min^sp_ ( in ) [not, in mathcomp.order.order] (in order_scope)
\min^sp_ ( in | ) [not, in mathcomp.order.order] (in order_scope)
\min^sp_ ( | ) [not, in mathcomp.order.order] (in order_scope)
\min^sp_ [not, in mathcomp.order.order] (in order_scope)
\min_ ( : ) [not, in mathcomp.order.preorder] (in order_scope)
\min_ ( : | ) [not, in mathcomp.order.preorder] (in order_scope)
\min_ ( < ) [not, in mathcomp.order.preorder] (in order_scope)
\min_ ( < ) [not, in mathcomp.order.preorder] (in order_scope)
\min_ ( < | ) [not, in mathcomp.order.preorder] (in order_scope)
\min_ ( <- | ) [not, in mathcomp.order.preorder] (in order_scope)
\min_ ( <= < ) [not, in mathcomp.order.preorder] (in order_scope)
\min_ ( <= < | ) [not, in mathcomp.order.preorder] (in order_scope)
\min_ ( in ) [not, in mathcomp.order.preorder] (in order_scope)
\min_ ( in | ) [not, in mathcomp.order.preorder] (in order_scope)
\min_ ( | ) [not, in mathcomp.order.preorder] (in order_scope)
\min_ [not, in mathcomp.order.preorder] (in order_scope)
\top [not, in mathcomp.order.preorder] (in order_scope)
\top^d [not, in mathcomp.order.preorder] (in order_scope)
`[ , +oo [ [not, in mathcomp.algebra.interval] (in order_scope)
`[ , [ [not, in mathcomp.algebra.interval] (in order_scope)
`[ , ] [not, in mathcomp.algebra.interval] (in order_scope)
`] -oo , +oo [ [not, in mathcomp.algebra.interval] (in order_scope)
`] -oo , [ [not, in mathcomp.algebra.interval] (in order_scope)
`] -oo , ] [not, in mathcomp.algebra.interval] (in order_scope)
`] , +oo [ [not, in mathcomp.algebra.interval] (in order_scope)
`] , [ [not, in mathcomp.algebra.interval] (in order_scope)
`] , ] [not, in mathcomp.algebra.interval] (in order_scope)
~` [not, in mathcomp.order.order] (in order_scope)
%<| [not, in mathcomp.order.preorder] (in order_scope)
%| [not, in mathcomp.order.preorder] (in order_scope)
< [not, in mathcomp.order.preorder] (in order_scope)
< [not, in mathcomp.order.preorder] (in order_scope)
< :> [not, in mathcomp.order.preorder] (in order_scope)
< < [not, in mathcomp.order.preorder] (in order_scope)
< <= [not, in mathcomp.order.preorder] (in order_scope)
< ?<= if [not, in mathcomp.order.preorder] (in order_scope)
< ?<= if :> [not, in mathcomp.order.preorder] (in order_scope)
<= [not, in mathcomp.order.preorder] (in order_scope)
<= [not, in mathcomp.order.preorder] (in order_scope)
<= :> [not, in mathcomp.order.preorder] (in order_scope)
<= < [not, in mathcomp.order.preorder] (in order_scope)
<= <= [not, in mathcomp.order.preorder] (in order_scope)
<= ?= iff [not, in mathcomp.order.preorder] (in order_scope)
<= ?= iff :> [not, in mathcomp.order.preorder] (in order_scope)
<=^d [not, in mathcomp.order.preorder] (in order_scope)
<=^d :> [not, in mathcomp.order.preorder] (in order_scope)
<=^d <=^d [not, in mathcomp.order.preorder] (in order_scope)
<=^d <^d [not, in mathcomp.order.preorder] (in order_scope)
<=^d ?= iff [not, in mathcomp.order.preorder] (in order_scope)
<=^d ?= iff :> [not, in mathcomp.order.preorder] (in order_scope)
<=^l [not, in mathcomp.order.preorder] (in order_scope)
<=^l [not, in mathcomp.order.preorder] (in order_scope)
<=^l :> [not, in mathcomp.order.preorder] (in order_scope)
<=^l :> [not, in mathcomp.order.preorder] (in order_scope)
<=^l <=^l [not, in mathcomp.order.preorder] (in order_scope)
<=^l <=^l [not, in mathcomp.order.preorder] (in order_scope)
<=^l <^l [not, in mathcomp.order.preorder] (in order_scope)
<=^l <^l [not, in mathcomp.order.preorder] (in order_scope)
<=^l ?= iff [not, in mathcomp.order.preorder] (in order_scope)
<=^l ?= iff [not, in mathcomp.order.preorder] (in order_scope)
<=^l ?= iff :> [not, in mathcomp.order.preorder] (in order_scope)
<=^l ?= iff :> [not, in mathcomp.order.preorder] (in order_scope)
<=^p [not, in mathcomp.order.preorder] (in order_scope)
<=^p :> [not, in mathcomp.order.preorder] (in order_scope)
<=^p <=^p [not, in mathcomp.order.preorder] (in order_scope)
<=^p <^p [not, in mathcomp.order.preorder] (in order_scope)
<=^p ?= iff [not, in mathcomp.order.preorder] (in order_scope)
<=^p ?= iff :> [not, in mathcomp.order.preorder] (in order_scope)
<=^sp [not, in mathcomp.order.preorder] (in order_scope)
<=^sp :> [not, in mathcomp.order.preorder] (in order_scope)
<=^sp <=^sp [not, in mathcomp.order.preorder] (in order_scope)
<=^sp <^sp [not, in mathcomp.order.preorder] (in order_scope)
<=^sp ?= iff [not, in mathcomp.order.preorder] (in order_scope)
<=^sp ?= iff :> [not, in mathcomp.order.preorder] (in order_scope)
<^d [not, in mathcomp.order.preorder] (in order_scope)
<^d :> [not, in mathcomp.order.preorder] (in order_scope)
<^d <=^d [not, in mathcomp.order.preorder] (in order_scope)
<^d <^d [not, in mathcomp.order.preorder] (in order_scope)
<^d ?<= if [not, in mathcomp.order.preorder] (in order_scope)
<^d ?<= if :> [not, in mathcomp.order.preorder] (in order_scope)
<^l [not, in mathcomp.order.preorder] (in order_scope)
<^l [not, in mathcomp.order.preorder] (in order_scope)
<^l :> [not, in mathcomp.order.preorder] (in order_scope)
<^l :> [not, in mathcomp.order.preorder] (in order_scope)
<^l <=^l [not, in mathcomp.order.preorder] (in order_scope)
<^l <=^l [not, in mathcomp.order.preorder] (in order_scope)
<^l <^l [not, in mathcomp.order.preorder] (in order_scope)
<^l <^l [not, in mathcomp.order.preorder] (in order_scope)
<^p [not, in mathcomp.order.preorder] (in order_scope)
<^p :> [not, in mathcomp.order.preorder] (in order_scope)
<^p <=^p [not, in mathcomp.order.preorder] (in order_scope)
<^p <^p [not, in mathcomp.order.preorder] (in order_scope)
<^sp [not, in mathcomp.order.preorder] (in order_scope)
<^sp :> [not, in mathcomp.order.preorder] (in order_scope)
<^sp <=^sp [not, in mathcomp.order.preorder] (in order_scope)
<^sp <^sp [not, in mathcomp.order.preorder] (in order_scope)
> [not, in mathcomp.order.preorder] (in order_scope)
> :> [not, in mathcomp.order.preorder] (in order_scope)
>< [not, in mathcomp.order.preorder] (in order_scope)
>< [not, in mathcomp.order.preorder] (in order_scope)
><^d [not, in mathcomp.order.preorder] (in order_scope)
><^l [not, in mathcomp.order.preorder] (in order_scope)
><^l [not, in mathcomp.order.preorder] (in order_scope)
><^p [not, in mathcomp.order.preorder] (in order_scope)
><^sp [not, in mathcomp.order.preorder] (in order_scope)
>= [not, in mathcomp.order.preorder] (in order_scope)
>= :> [not, in mathcomp.order.preorder] (in order_scope)
>=< [not, in mathcomp.order.preorder] (in order_scope)
>=< [not, in mathcomp.order.preorder] (in order_scope)
>=<^d [not, in mathcomp.order.preorder] (in order_scope)
>=<^l [not, in mathcomp.order.preorder] (in order_scope)
>=<^l [not, in mathcomp.order.preorder] (in order_scope)
>=<^p [not, in mathcomp.order.preorder] (in order_scope)
>=<^sp [not, in mathcomp.order.preorder] (in order_scope)
>=^d [not, in mathcomp.order.preorder] (in order_scope)
>=^d :> [not, in mathcomp.order.preorder] (in order_scope)
>=^l [not, in mathcomp.order.preorder] (in order_scope)
>=^l [not, in mathcomp.order.preorder] (in order_scope)
>=^l :> [not, in mathcomp.order.preorder] (in order_scope)
>=^l :> [not, in mathcomp.order.preorder] (in order_scope)
>=^p [not, in mathcomp.order.preorder] (in order_scope)
>=^p :> [not, in mathcomp.order.preorder] (in order_scope)
>=^sp [not, in mathcomp.order.preorder] (in order_scope)
>=^sp :> [not, in mathcomp.order.preorder] (in order_scope)
>^d [not, in mathcomp.order.preorder] (in order_scope)
>^d :> [not, in mathcomp.order.preorder] (in order_scope)
>^l [not, in mathcomp.order.preorder] (in order_scope)
>^l [not, in mathcomp.order.preorder] (in order_scope)
>^l :> [not, in mathcomp.order.preorder] (in order_scope)
>^l :> [not, in mathcomp.order.preorder] (in order_scope)
>^p [not, in mathcomp.order.preorder] (in order_scope)
>^p :> [not, in mathcomp.order.preorder] (in order_scope)
>^sp [not, in mathcomp.order.preorder] (in order_scope)
>^sp :> [not, in mathcomp.order.preorder] (in order_scope)
`&^d` [not, in mathcomp.order.order] (in order_scope)
`&^l` [not, in mathcomp.order.order] (in order_scope)
`&^l` [not, in mathcomp.order.order] (in order_scope)
`&^p` [not, in mathcomp.order.order] (in order_scope)
`&^sp` [not, in mathcomp.order.order] (in order_scope)
`&` [not, in mathcomp.order.order] (in order_scope)
`\` [not, in mathcomp.order.order] (in order_scope)
`|^d` [not, in mathcomp.order.order] (in order_scope)
`|^l` [not, in mathcomp.order.order] (in order_scope)
`|^l` [not, in mathcomp.order.order] (in order_scope)
`|^p` [not, in mathcomp.order.order] (in order_scope)
`|^sp` [not, in mathcomp.order.order] (in order_scope)
`|` [not, in mathcomp.order.order] (in order_scope)

quotient_scope

\pi [not, in mathcomp.boot.generic_quotient] (in quotient_scope)
\pi_ [not, in mathcomp.boot.generic_quotient] (in quotient_scope)
{eq_quot } [not, in mathcomp.boot.generic_quotient] (in quotient_scope)
{pi } [not, in mathcomp.boot.generic_quotient] (in quotient_scope)
{pi_ } [not, in mathcomp.boot.generic_quotient] (in quotient_scope)
!= %[ mod_ideal ] [not, in mathcomp.algebra.ring_quotient] (in quotient_scope)
!= %[mod ] [not, in mathcomp.boot.generic_quotient] (in quotient_scope)
!= %[mod_eq ] [not, in mathcomp.boot.generic_quotient] (in quotient_scope)
<> %[ mod_ideal ] [not, in mathcomp.algebra.ring_quotient] (in quotient_scope)
<> %[mod ] [not, in mathcomp.boot.generic_quotient] (in quotient_scope)
<> %[mod_eq ] [not, in mathcomp.boot.generic_quotient] (in quotient_scope)
= %[ mod_ideal ] [not, in mathcomp.algebra.ring_quotient] (in quotient_scope)
= %[mod ] [not, in mathcomp.boot.generic_quotient] (in quotient_scope)
= %[mod_eq ] [not, in mathcomp.boot.generic_quotient] (in quotient_scope)
== %[ mod_ideal ] [not, in mathcomp.algebra.ring_quotient] (in quotient_scope)
== %[mod ] [not, in mathcomp.boot.generic_quotient] (in quotient_scope)
== %[mod_eq ] [not, in mathcomp.boot.generic_quotient] (in quotient_scope)

rat_scope

- [not, in mathcomp.algebra.rat] (in rat_scope)
* [not, in mathcomp.algebra.rat] (in rat_scope)
+ [not, in mathcomp.algebra.rat] (in rat_scope)
- [not, in mathcomp.algebra.rat] (in rat_scope)
/ [not, in mathcomp.algebra.rat] (in rat_scope)
^-1 [not, in mathcomp.algebra.rat] (in rat_scope)

ring_scope

'1_ [not, in mathcomp.group_representation.classfun] (in ring_scope)
'1_ [not, in mathcomp.group_representation.classfun] (in ring_scope)
'CF ( , ) [not, in mathcomp.group_representation.classfun] (in ring_scope)
'CF ( , ) [not, in mathcomp.group_representation.classfun] (in ring_scope)
'Im [not, in mathcomp.algebra.numeric_hierarchy.numfield] (in ring_scope)
'Im [not, in mathcomp.algebra.numeric_hierarchy.numfield] (in ring_scope)
'Ind [not, in mathcomp.group_representation.classfun] (in ring_scope)
'Ind[ , ] [not, in mathcomp.group_representation.classfun] (in ring_scope)
'Ind[ , ] [not, in mathcomp.group_representation.classfun] (in ring_scope)
'Ind[ ] [not, in mathcomp.group_representation.classfun] (in ring_scope)
'Ind[ ] [not, in mathcomp.group_representation.classfun] (in ring_scope)
'K_ [not, in mathcomp.group_representation.integral_char] (in ring_scope)
'K_ [not, in mathcomp.group_representation.integral_char] (in ring_scope)
'Re [not, in mathcomp.algebra.numeric_hierarchy.numfield] (in ring_scope)
'Re [not, in mathcomp.algebra.numeric_hierarchy.numfield] (in ring_scope)
'Res [not, in mathcomp.group_representation.classfun] (in ring_scope)
'Res[ , ] [not, in mathcomp.group_representation.classfun] (in ring_scope)
'Res[ ] [not, in mathcomp.group_representation.classfun] (in ring_scope)
'X [not, in mathcomp.algebra.poly] (in ring_scope)
'X^ [not, in mathcomp.algebra.poly] (in ring_scope)
'Y [not, in mathcomp.algebra.polyXY] (in ring_scope)
'[ , ] [not, in mathcomp.group_representation.classfun] (in ring_scope)
'[ , ] [not, in mathcomp.algebra.spectral] (in ring_scope)
'[ , ] [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
'[ , ] [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
'[ , ] [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
'[ , ] [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
'[ , ] [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
'[ , ] [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
'[ , ] [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
'[ , ] [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
'[ , ] [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
'[ , ] [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
'[ , ] [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
'[ , ]_ [not, in mathcomp.group_representation.classfun] (in ring_scope)
'[ , ]_1 [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
'[ , ]_2 [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
'[ ] [not, in mathcomp.group_representation.classfun] (in ring_scope)
'[ ] [not, in mathcomp.algebra.spectral] (in ring_scope)
'[ ] [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
'[ ] [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
'[ ] [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
'[ ] [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
'[ ] [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
'[ ] [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
'[ ] [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
'[ ] [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
'[ ] [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
'[ ] [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
'[ ] [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
'[ ]_ [not, in mathcomp.group_representation.classfun] (in ring_scope)
'[ ]_1 [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
'[ ]_2 [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
'chi[ ]_ [not, in mathcomp.group_representation.character] (in ring_scope)
'chi_ [not, in mathcomp.group_representation.character] (in ring_scope)
'e_ [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
'i [not, in mathcomp.algebra.numeric_hierarchy.numfield] (in ring_scope)
'i [not, in mathcomp.algebra.numeric_hierarchy.numfield] (in ring_scope)
'nX^ [not, in mathcomp.algebra.qpoly] (in ring_scope)
'omega_ [ ] [not, in mathcomp.group_representation.integral_char] (in ring_scope)
'qX [not, in mathcomp.algebra.qpoly] (in ring_scope)
-%R [not, in mathcomp.boot.nmodule] (in ring_scope)
-%R [not, in mathcomp.boot.nmodule] (in ring_scope)
-%R [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
- 1 [not, in mathcomp.boot.nmodule] (in ring_scope)
- 1 [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
- 1 [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
- [not, in mathcomp.boot.nmodule] (in ring_scope)
- [not, in mathcomp.boot.nmodule] (in ring_scope)
- [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
0 [not, in mathcomp.boot.nmodule] (in ring_scope)
0 [not, in mathcomp.boot.nmodule] (in ring_scope)
0 [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
1 [not, in mathcomp.boot.nmodule] (in ring_scope)
1 [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
1 [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
< [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in ring_scope)
< :> [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in ring_scope)
<= [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in ring_scope)
<= :> [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in ring_scope)
> [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in ring_scope)
> :> [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in ring_scope)
>< [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in ring_scope)
>< :> [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in ring_scope)
>= [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in ring_scope)
>= :> [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in ring_scope)
>=< [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in ring_scope)
>=< :> [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in ring_scope)
[ arg max_ ( > ) ] [not, in mathcomp.algebra.numeric_hierarchy.numdomain] (in ring_scope)
[ arg max_ ( > in ) ] [not, in mathcomp.algebra.numeric_hierarchy.numdomain] (in ring_scope)
[ arg max_ ( > | ) ] [not, in mathcomp.algebra.numeric_hierarchy.numdomain] (in ring_scope)
[ arg min_ ( < ) ] [not, in mathcomp.algebra.numeric_hierarchy.numdomain] (in ring_scope)
[ arg min_ ( < in ) ] [not, in mathcomp.algebra.numeric_hierarchy.numdomain] (in ring_scope)
[ arg min_ ( < | ) ] [not, in mathcomp.algebra.numeric_hierarchy.numdomain] (in ring_scope)
[ char ] [not, in mathcomp.algebra.algebraic_hierarchy.ssralg] (in ring_scope)
[ itv of ] [not, in mathcomp.algebra.interval_inference] (in ring_scope)
[ pchar ] [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
[ rat // ] [not, in mathcomp.algebra.rat] (in ring_scope)
[ rat // ] [not, in mathcomp.algebra.rat] (in ring_scope)
\- [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
\0 [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
\adj [not, in mathcomp.algebra.matrix] (in ring_scope)
\col_ ( < ) [not, in mathcomp.algebra.matrix] (in ring_scope)
\col_ [not, in mathcomp.algebra.matrix] (in ring_scope)
\det [not, in mathcomp.algebra.matrix] (in ring_scope)
\matrix[ ]_ ( , ) [not, in mathcomp.algebra.matrix] (in ring_scope)
\matrix_ ( , ) [not, in mathcomp.algebra.matrix] (in ring_scope)
\matrix_ ( , < ) [not, in mathcomp.algebra.matrix] (in ring_scope)
\matrix_ ( < ) [not, in mathcomp.algebra.matrix] (in ring_scope)
\matrix_ ( < , < ) [not, in mathcomp.algebra.matrix] (in ring_scope)
\matrix_ [not, in mathcomp.algebra.matrix] (in ring_scope)
\mxblock_ ( , ) [not, in mathcomp.algebra.matrix] (in ring_scope)
\mxblock_ ( , ) [not, in mathcomp.algebra.matrix] (in ring_scope)
\mxblock_ ( , < ) [not, in mathcomp.algebra.matrix] (in ring_scope)
\mxblock_ ( < , < ) [not, in mathcomp.algebra.matrix] (in ring_scope)
\mxcol_ ( < ) [not, in mathcomp.algebra.matrix] (in ring_scope)
\mxcol_ [not, in mathcomp.algebra.matrix] (in ring_scope)
\mxcol_ [not, in mathcomp.algebra.matrix] (in ring_scope)
\mxdiag_ ( < ) [not, in mathcomp.algebra.matrix] (in ring_scope)
\mxdiag_ [not, in mathcomp.algebra.matrix] (in ring_scope)
\mxdiag_ [not, in mathcomp.algebra.matrix] (in ring_scope)
\mxrow_ ( < ) [not, in mathcomp.algebra.matrix] (in ring_scope)
\mxrow_ [not, in mathcomp.algebra.matrix] (in ring_scope)
\mxrow_ [not, in mathcomp.algebra.matrix] (in ring_scope)
\poly_ ( < ) [not, in mathcomp.algebra.poly] (in ring_scope)
\prod_ ( : ) [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
\prod_ ( : | ) [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
\prod_ ( < ) [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
\prod_ ( < | ) [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
\prod_ ( <- ) [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
\prod_ ( <- | ) [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
\prod_ ( <= < ) [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
\prod_ ( <= < | ) [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
\prod_ ( in ) [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
\prod_ ( in | ) [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
\prod_ ( | ) [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
\prod_ [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
\row_ ( < ) [not, in mathcomp.algebra.matrix] (in ring_scope)
\row_ [not, in mathcomp.algebra.matrix] (in ring_scope)
\sum_ ( : ) [not, in mathcomp.boot.nmodule] (in ring_scope)
\sum_ ( : ) [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
\sum_ ( : | ) [not, in mathcomp.boot.nmodule] (in ring_scope)
\sum_ ( : | ) [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
\sum_ ( < ) [not, in mathcomp.boot.nmodule] (in ring_scope)
\sum_ ( < ) [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
\sum_ ( < | ) [not, in mathcomp.boot.nmodule] (in ring_scope)
\sum_ ( < | ) [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
\sum_ ( <- ) [not, in mathcomp.boot.nmodule] (in ring_scope)
\sum_ ( <- ) [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
\sum_ ( <- | ) [not, in mathcomp.boot.nmodule] (in ring_scope)
\sum_ ( <- | ) [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
\sum_ ( <= < ) [not, in mathcomp.boot.nmodule] (in ring_scope)
\sum_ ( <= < ) [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
\sum_ ( <= < | ) [not, in mathcomp.boot.nmodule] (in ring_scope)
\sum_ ( <= < | ) [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
\sum_ ( in ) [not, in mathcomp.boot.nmodule] (in ring_scope)
\sum_ ( in ) [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
\sum_ ( in | ) [not, in mathcomp.boot.nmodule] (in ring_scope)
\sum_ ( in | ) [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
\sum_ ( | ) [not, in mathcomp.boot.nmodule] (in ring_scope)
\sum_ ( | ) [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
\sum_ [not, in mathcomp.boot.nmodule] (in ring_scope)
\sum_ [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
\tr [not, in mathcomp.algebra.matrix] (in ring_scope)
\tr [not, in mathcomp.algebra.matrix] (in ring_scope)
\tr [not, in mathcomp.algebra.matrix] (in ring_scope)
`[ , +oo [ [not, in mathcomp.algebra.interval] (in ring_scope)
`[ , [ [not, in mathcomp.algebra.interval] (in ring_scope)
`[ , ] [not, in mathcomp.algebra.interval] (in ring_scope)
`] -oo , +oo [ [not, in mathcomp.algebra.interval] (in ring_scope)
`] -oo , [ [not, in mathcomp.algebra.interval] (in ring_scope)
`] -oo , ] [not, in mathcomp.algebra.interval] (in ring_scope)
`] , +oo [ [not, in mathcomp.algebra.interval] (in ring_scope)
`] , [ [not, in mathcomp.algebra.interval] (in ring_scope)
`] , ] [not, in mathcomp.algebra.interval] (in ring_scope)
`| | [not, in mathcomp.algebra.numeric_hierarchy.numdomain] (in ring_scope)
`| | [not, in mathcomp.algebra.numeric_hierarchy.numdomain] (in ring_scope)
`| | [not, in mathcomp.algebra.numeric_hierarchy.numdomain] (in ring_scope)
`| | [not, in mathcomp.algebra.numeric_hierarchy.numdomain] (in ring_scope)
`| | [not, in mathcomp.algebra.numeric_hierarchy.numdomain] (in ring_scope)
{ bilinear -> -> | & } [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
{ bilinear -> -> | } [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
{ bilinear -> -> } [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
{ biscalar } [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
{ dot for } [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
{ hermitian for & } [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
{ hermitian_sym for } [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
{ nonneg } [not, in mathcomp.algebra.interval_inference] (in ring_scope)
{ posnum } [not, in mathcomp.algebra.interval_inference] (in ring_scope)
{ skew_symmetric } [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
{ symmetric } [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
!= :> int [not, in mathcomp.algebra.ssrint] (in ring_scope)
!= :> int [not, in mathcomp.algebra.ssrint] (in ring_scope)
%% [not, in mathcomp.algebra.polydiv] (in ring_scope)
%/ [not, in mathcomp.algebra.polydiv] (in ring_scope)
%:A [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
%:A [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
%:M [not, in mathcomp.algebra.matrix] (in ring_scope)
%:M [not, in mathcomp.algebra.matrix] (in ring_scope)
%:M [not, in mathcomp.algebra.matrix] (in ring_scope)
%:M [not, in mathcomp.algebra.matrix] (in ring_scope)
%:P [not, in mathcomp.algebra.poly] (in ring_scope)
%:Q [not, in mathcomp.algebra.rat] (in ring_scope)
%:R [not, in mathcomp.boot.nmodule] (in ring_scope)
%:R [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
%:R [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
%:Z [not, in mathcomp.algebra.ssrint] (in ring_scope)
%:i01 [not, in mathcomp.algebra.interval_inference] (in ring_scope)
%:i01 [not, in mathcomp.algebra.interval_inference] (in ring_scope)
%:inum [not, in mathcomp.algebra.interval_inference] (in ring_scope)
%:itv [not, in mathcomp.algebra.interval_inference] (in ring_scope)
%:n01 [not, in mathcomp.algebra.interval_inference] (in ring_scope)
%:n01 [not, in mathcomp.algebra.interval_inference] (in ring_scope)
%:nng [not, in mathcomp.algebra.interval_inference] (in ring_scope)
%:nng [not, in mathcomp.algebra.interval_inference] (in ring_scope)
%:nngnum [not, in mathcomp.algebra.interval_inference] (in ring_scope)
%:num [not, in mathcomp.algebra.interval_inference] (in ring_scope)
%:pos [not, in mathcomp.algebra.interval_inference] (in ring_scope)
%:pos [not, in mathcomp.algebra.interval_inference] (in ring_scope)
%:posnat [not, in mathcomp.algebra.interval_inference] (in ring_scope)
%:posnum [not, in mathcomp.algebra.interval_inference] (in ring_scope)
%:~R [not, in mathcomp.algebra.ssrint] (in ring_scope)
%= [not, in mathcomp.algebra.polydiv] (in ring_scope)
%| [not, in mathcomp.algebra.polydiv] (in ring_scope)
'_|_ [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
'_|_ [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
* [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
* [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
*+ [not, in mathcomp.boot.nmodule] (in ring_scope)
*+ [not, in mathcomp.boot.nmodule] (in ring_scope)
*+ [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
*- [not, in mathcomp.boot.nmodule] (in ring_scope)
*- [not, in mathcomp.boot.nmodule] (in ring_scope)
*- [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
*: [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
*: [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
*m [not, in mathcomp.algebra.matrix] (in ring_scope)
*m [not, in mathcomp.algebra.matrix] (in ring_scope)
*m: [not, in mathcomp.algebra.matrix] (in ring_scope)
*t [not, in mathcomp.algebra.tensor] (in ring_scope)
*~ [not, in mathcomp.algebra.ssrint] (in ring_scope)
+ [not, in mathcomp.boot.nmodule] (in ring_scope)
+ [not, in mathcomp.boot.nmodule] (in ring_scope)
+ [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
- [not, in mathcomp.boot.nmodule] (in ring_scope)
- [not, in mathcomp.boot.nmodule] (in ring_scope)
- [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
.-lagrange [not, in mathcomp.algebra.qpoly] (in ring_scope)
.-lagrange_ [not, in mathcomp.algebra.qpoly] (in ring_scope)
.-primitive_root [not, in mathcomp.algebra.poly] (in ring_scope)
.-primitive_root [not, in mathcomp.algebra.poly] (in ring_scope)
.-root [not, in mathcomp.algebra.numeric_hierarchy.numfield] (in ring_scope)
.-sesqui [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
.-unity_root [not, in mathcomp.algebra.poly] (in ring_scope)
.-unity_root [not, in mathcomp.algebra.poly] (in ring_scope)
.[ , ] [not, in mathcomp.algebra.polyXY] (in ring_scope)
.[ ] [not, in mathcomp.algebra.poly] (in ring_scope)
.[ ] [not, in mathcomp.algebra.poly] (in ring_scope)
/ [not, in mathcomp.algebra.algebraic_hierarchy.divalg] (in ring_scope)
< [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in ring_scope)
< [not, in mathcomp.algebra.numeric_hierarchy.numdomain] (in ring_scope)
< [not, in mathcomp.algebra.numeric_hierarchy.numdomain] (in ring_scope)
< [not, in mathcomp.algebra.numeric_hierarchy.numdomain] (in ring_scope)
< :> [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in ring_scope)
< < [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in ring_scope)
< <= [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in ring_scope)
< ?<= if [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in ring_scope)
< ?<= if :> [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in ring_scope)
<= [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in ring_scope)
<= [not, in mathcomp.algebra.numeric_hierarchy.numdomain] (in ring_scope)
<= [not, in mathcomp.algebra.numeric_hierarchy.numdomain] (in ring_scope)
<= [not, in mathcomp.algebra.numeric_hierarchy.numdomain] (in ring_scope)
<= :> [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in ring_scope)
<= < [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in ring_scope)
<= <= [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in ring_scope)
<= ?= iff [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in ring_scope)
<= ?= iff :> [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in ring_scope)
<> :> int [not, in mathcomp.algebra.ssrint] (in ring_scope)
<> :> int [not, in mathcomp.algebra.ssrint] (in ring_scope)
= :> int [not, in mathcomp.algebra.ssrint] (in ring_scope)
= :> int [not, in mathcomp.algebra.ssrint] (in ring_scope)
== :> int [not, in mathcomp.algebra.ssrint] (in ring_scope)
== :> int [not, in mathcomp.algebra.ssrint] (in ring_scope)
> [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in ring_scope)
> :> [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in ring_scope)
>< [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in ring_scope)
>= [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in ring_scope)
>= :> [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in ring_scope)
>=< [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in ring_scope)
\* [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
\*: [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
\*o [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
\+ [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
\- [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
\Po [not, in mathcomp.algebra.poly] (in ring_scope)
\Po [not, in mathcomp.algebra.poly] (in ring_scope)
\o* [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
^%:A [not, in mathcomp.field.finfield] (in ring_scope)
^ [not, in mathcomp.field.separable] (in ring_scope)
^ [not, in mathcomp.field.algebraics_fundamentals] (in ring_scope)
^ [not, in mathcomp.algebra.ssrint] (in ring_scope)
^ [not, in mathcomp.algebra.polyXY] (in ring_scope)
^* [not, in mathcomp.algebra.numeric_hierarchy.numfield] (in ring_scope)
^+ [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
^+ [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
^- [not, in mathcomp.algebra.algebraic_hierarchy.divalg] (in ring_scope)
^-1 [not, in mathcomp.algebra.algebraic_hierarchy.divalg] (in ring_scope)
^:P [not, in mathcomp.algebra.polyXY] (in ring_scope)
^:P [not, in mathcomp.algebra.poly] (in ring_scope)
^@ [not, in mathcomp.field.algebraics_fundamentals] (in ring_scope)
^@ [not, in mathcomp.solvable.finmodule] (in ring_scope)
^@ [not, in mathcomp.solvable.finmodule] (in ring_scope)
^T [not, in mathcomp.algebra.matrix] (in ring_scope)
^T [not, in mathcomp.algebra.matrix] (in ring_scope)
^_|_ [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
^` ( ) [not, in mathcomp.algebra.poly] (in ring_scope)
^` ( ) [not, in mathcomp.algebra.poly] (in ring_scope)
^` () [not, in mathcomp.algebra.poly] (in ring_scope)
^`N ( ) [not, in mathcomp.algebra.poly] (in ring_scope)
^`N ( ) [not, in mathcomp.algebra.poly] (in ring_scope)
^f [not, in mathcomp.group_representation.mxrepresentation] (in ring_scope)
^f [not, in mathcomp.group_representation.mxrepresentation] (in ring_scope)
^f [not, in mathcomp.algebra.polydiv] (in ring_scope)
^f [not, in mathcomp.algebra.polydiv] (in ring_scope)
^f [not, in mathcomp.algebra.poly] (in ring_scope)
^f [not, in mathcomp.algebra.poly] (in ring_scope)
^f [not, in mathcomp.algebra.poly] (in ring_scope)
^f [not, in mathcomp.algebra.poly] (in ring_scope)
^f [not, in mathcomp.algebra.poly] (in ring_scope)
^f [not, in mathcomp.algebra.mxpoly] (in ring_scope)
^f [not, in mathcomp.algebra.mxpoly] (in ring_scope)
^f [not, in mathcomp.algebra.mxpoly] (in ring_scope)
^f [not, in mathcomp.algebra.mxpoly] (in ring_scope)
^f [not, in mathcomp.algebra.mxalgebra] (in ring_scope)
^f [not, in mathcomp.algebra.matrix] (in ring_scope)
^f [not, in mathcomp.algebra.matrix] (in ring_scope)
^f [not, in mathcomp.algebra.matrix] (in ring_scope)
^f [not, in mathcomp.algebra.matrix] (in ring_scope)
^f [not, in mathcomp.algebra.matrix] (in ring_scope)
^f [not, in mathcomp.algebra.matrix] (in ring_scope)
^iota [not, in mathcomp.field.fieldext] (in ring_scope)
`_ [not, in mathcomp.boot.nmodule] (in ring_scope)
`_ [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
~_ { in } [not, in mathcomp.algebra.mxpoly] (in ring_scope)

section_scope

/ [not, in mathcomp.solvable.jordanholder] (in section_scope)

seq_scope

[ :: ] [not, in mathcomp.boot.seq] (in seq_scope)
[ :: & ] [not, in mathcomp.boot.seq] (in seq_scope)
[ :: , , .. , & ] [not, in mathcomp.boot.seq] (in seq_scope)
[ :: ; ; .. ; ] [not, in mathcomp.boot.seq] (in seq_scope)
[ :: ] [not, in mathcomp.boot.seq] (in seq_scope)
[ seq ' <- | & ] [not, in mathcomp.boot.seq] (in seq_scope)
[ seq ' <- | ] [not, in mathcomp.boot.seq] (in seq_scope)
[ seq , ] [not, in mathcomp.boot.fintype] (in seq_scope)
[ seq : | <- & ] [not, in mathcomp.boot.seq] (in seq_scope)
[ seq : | <- , <- ] [not, in mathcomp.boot.seq] (in seq_scope)
[ seq : | <- ] [not, in mathcomp.boot.seq] (in seq_scope)
[ seq <- | & ] [not, in mathcomp.boot.seq] (in seq_scope)
[ seq <- | ] [not, in mathcomp.boot.seq] (in seq_scope)
[ seq | : ] [not, in mathcomp.boot.fintype] (in seq_scope)
[ seq | <- & ] [not, in mathcomp.boot.seq] (in seq_scope)
[ seq | <- , <- ] [not, in mathcomp.boot.seq] (in seq_scope)
[ seq | <- ] [not, in mathcomp.boot.seq] (in seq_scope)
[ seq | ] [not, in mathcomp.boot.fintype] (in seq_scope)
[ seq | in ] [not, in mathcomp.boot.fintype] (in seq_scope)
++ [not, in mathcomp.boot.seq] (in seq_scope)
++ [not, in mathcomp.boot.seq] (in seq_scope)
:: [not, in mathcomp.boot.seq] (in seq_scope)

sesquilinear_scope

^ [not, in mathcomp.algebra.sesquilinear] (in sesquilinear_scope)
^t [not, in mathcomp.algebra.sesquilinear] (in sesquilinear_scope)
^t* [not, in mathcomp.algebra.spectral] (in sesquilinear_scope)

set_scope

[ set : ] [not, in mathcomp.boot.finset] (in set_scope)
[ set :: ] [not, in mathcomp.boot.finset] (in set_scope)
[ set ~ ] [not, in mathcomp.boot.finset] (in set_scope)
[ set : ] [not, in mathcomp.boot.finset] (in set_scope)
[ set : in ] [not, in mathcomp.boot.finset] (in set_scope)
[ set : in | & ] [not, in mathcomp.boot.finset] (in set_scope)
[ set : in | ] [not, in mathcomp.boot.finset] (in set_scope)
[ set : | & ] [not, in mathcomp.boot.finset] (in set_scope)
[ set : | ] [not, in mathcomp.boot.finset] (in set_scope)
[ set ; ; .. ; ] [not, in mathcomp.boot.finset] (in set_scope)
[ set ] [not, in mathcomp.boot.finset] (in set_scope)
[ set in ] [not, in mathcomp.boot.finset] (in set_scope)
[ set in | & ] [not, in mathcomp.boot.finset] (in set_scope)
[ set in | ] [not, in mathcomp.boot.finset] (in set_scope)
[ set | & ] [not, in mathcomp.boot.finset] (in set_scope)
[ set | , & ] [not, in mathcomp.boot.finset] (in set_scope)
[ set | , ] [not, in mathcomp.boot.finset] (in set_scope)
[ set | , in & ] [not, in mathcomp.boot.finset] (in set_scope)
[ set | , in ] [not, in mathcomp.boot.finset] (in set_scope)
[ set | : & ] [not, in mathcomp.boot.finset] (in set_scope)
[ set | : , : & ] [not, in mathcomp.boot.finset] (in set_scope)
[ set | : , : ] [not, in mathcomp.boot.finset] (in set_scope)
[ set | : , : in & ] [not, in mathcomp.boot.finset] (in set_scope)
[ set | : , : in ] [not, in mathcomp.boot.finset] (in set_scope)
[ set | : ] [not, in mathcomp.boot.finset] (in set_scope)
[ set | : in & ] [not, in mathcomp.boot.finset] (in set_scope)
[ set | : in , : & ] [not, in mathcomp.boot.finset] (in set_scope)
[ set | : in , : ] [not, in mathcomp.boot.finset] (in set_scope)
[ set | : in , : in & ] [not, in mathcomp.boot.finset] (in set_scope)
[ set | : in , : in ] [not, in mathcomp.boot.finset] (in set_scope)
[ set | : in ] [not, in mathcomp.boot.finset] (in set_scope)
[ set | ] [not, in mathcomp.boot.finset] (in set_scope)
[ set | in & ] [not, in mathcomp.boot.finset] (in set_scope)
[ set | in , & ] [not, in mathcomp.boot.finset] (in set_scope)
[ set | in , ] [not, in mathcomp.boot.finset] (in set_scope)
[ set | in , in & ] [not, in mathcomp.boot.finset] (in set_scope)
[ set | in , in ] [not, in mathcomp.boot.finset] (in set_scope)
[ set | in ] [not, in mathcomp.boot.finset] (in set_scope)
\bigcap_ ( : ) [not, in mathcomp.boot.finset] (in set_scope)
\bigcap_ ( : | ) [not, in mathcomp.boot.finset] (in set_scope)
\bigcap_ ( < ) [not, in mathcomp.boot.finset] (in set_scope)
\bigcap_ ( < | ) [not, in mathcomp.boot.finset] (in set_scope)
\bigcap_ ( <- ) [not, in mathcomp.boot.finset] (in set_scope)
\bigcap_ ( <- | ) [not, in mathcomp.boot.finset] (in set_scope)
\bigcap_ ( <= < ) [not, in mathcomp.boot.finset] (in set_scope)
\bigcap_ ( <= < | ) [not, in mathcomp.boot.finset] (in set_scope)
\bigcap_ ( in ) [not, in mathcomp.boot.finset] (in set_scope)
\bigcap_ ( in | ) [not, in mathcomp.boot.finset] (in set_scope)
\bigcap_ ( | ) [not, in mathcomp.boot.finset] (in set_scope)
\bigcap_ [not, in mathcomp.boot.finset] (in set_scope)
\bigcup_ ( : ) [not, in mathcomp.boot.finset] (in set_scope)
\bigcup_ ( : | ) [not, in mathcomp.boot.finset] (in set_scope)
\bigcup_ ( < ) [not, in mathcomp.boot.finset] (in set_scope)
\bigcup_ ( < | ) [not, in mathcomp.boot.finset] (in set_scope)
\bigcup_ ( <- ) [not, in mathcomp.boot.finset] (in set_scope)
\bigcup_ ( <- | ) [not, in mathcomp.boot.finset] (in set_scope)
\bigcup_ ( <= < ) [not, in mathcomp.boot.finset] (in set_scope)
\bigcup_ ( <= < | ) [not, in mathcomp.boot.finset] (in set_scope)
\bigcup_ ( in ) [not, in mathcomp.boot.finset] (in set_scope)
\bigcup_ ( in | ) [not, in mathcomp.boot.finset] (in set_scope)
\bigcup_ ( | ) [not, in mathcomp.boot.finset] (in set_scope)
\bigcup_ [not, in mathcomp.boot.finset] (in set_scope)
~: [not, in mathcomp.boot.finset] (in set_scope)
.-dtuple ( ) [not, in mathcomp.solvable.primitive_action] (in set_scope)
:!=: [not, in mathcomp.boot.finset] (in set_scope)
:&: [not, in mathcomp.boot.finset] (in set_scope)
::&: [not, in mathcomp.boot.finset] (in set_scope)
:<>: [not, in mathcomp.boot.finset] (in set_scope)
:=: [not, in mathcomp.boot.finset] (in set_scope)
:==: [not, in mathcomp.boot.finset] (in set_scope)
:=P: [not, in mathcomp.boot.finset] (in set_scope)
:\ [not, in mathcomp.boot.finset] (in set_scope)
:\: [not, in mathcomp.boot.finset] (in set_scope)
:|: [not, in mathcomp.boot.finset] (in set_scope)
@2: ( , ) [not, in mathcomp.boot.finset] (in set_scope)
@: [not, in mathcomp.boot.finset] (in set_scope)
@^-1: [not, in mathcomp.boot.finset] (in set_scope)
|: [not, in mathcomp.boot.finset] (in set_scope)

ssr_scope

> [not, in mathcomp.boot.ssreflect] (in ssr_scope)

ssripat_scope

[ cofix ] [not, in mathcomp.boot.ssreflect] (in ssripat_scope)
[ fix ] [not, in mathcomp.boot.ssreflect] (in ssripat_scope)
[ hide ] [not, in mathcomp.boot.ssreflect] (in ssripat_scope)
[ let ] [not, in mathcomp.boot.ssreflect] (in ssripat_scope)

term_scope

'X_ [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
'X_ [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
'exists 'X_ , [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
'exists 'X_ , [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
'forall 'X_ , [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
'forall 'X_ , [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
- [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
- [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
0 [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
0 [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
1 [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
1 [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
~ [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
~ [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
!= [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
!= [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
%:R [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
%:R [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
%:T [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
%:T [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
* [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
* [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
*+ [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
*+ [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
+ [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
+ [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
- [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
- [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
/ [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
/ [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
/\ [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
/\ [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
== [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
== [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
==> [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
==> [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
\/ [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
\/ [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
^+ [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
^+ [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
^-1 [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
^-1 [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)

type_scope

'A [ ]_ ( ) [not, in mathcomp.algebra.mxalgebra] (in type_scope)
'A [ ]_ ( , ) [not, in mathcomp.algebra.mxalgebra] (in type_scope)
'A [ ]_ [not, in mathcomp.algebra.mxalgebra] (in type_scope)
'AEnd ( ) [not, in mathcomp.field.falgebra] (in type_scope)
'AHom ( , ) [not, in mathcomp.field.falgebra] (in type_scope)
'A_ ( ) [not, in mathcomp.algebra.mxalgebra] (in type_scope)
'A_ ( , ) [not, in mathcomp.algebra.mxalgebra] (in type_scope)
'A_ [not, in mathcomp.algebra.mxalgebra] (in type_scope)
'CF ( ) [not, in mathcomp.group_representation.classfun] (in type_scope)
'D^ [not, in mathcomp.solvable.extraspecial] (in type_scope)
'D^ * Q [not, in mathcomp.solvable.extraspecial] (in type_scope)
'D_ [not, in mathcomp.solvable.extremal] (in type_scope)
'End ( ) [not, in mathcomp.algebra.vector] (in type_scope)
'F_ [not, in mathcomp.algebra.zmodp] (in type_scope)
'Hom ( , ) [not, in mathcomp.algebra.vector] (in type_scope)
'M[ ]_ ( ) [not, in mathcomp.algebra.matrix] (in type_scope)
'M[ ]_ ( , ) [not, in mathcomp.algebra.matrix] (in type_scope)
'M[ ]_ [not, in mathcomp.algebra.matrix] (in type_scope)
'M_ ( ) [not, in mathcomp.algebra.matrix] (in type_scope)
'M_ ( , ) [not, in mathcomp.algebra.mxalgebra] (in type_scope)
'M_ ( , ) [not, in mathcomp.algebra.mxalgebra] (in type_scope)
'M_ ( , ) [not, in mathcomp.algebra.mxalgebra] (in type_scope)
'M_ ( , ) [not, in mathcomp.algebra.matrix] (in type_scope)
'M_ [not, in mathcomp.algebra.mxalgebra] (in type_scope)
'M_ [not, in mathcomp.algebra.mxalgebra] (in type_scope)
'M_ [not, in mathcomp.algebra.mxalgebra] (in type_scope)
'M_ [not, in mathcomp.algebra.matrix] (in type_scope)
'Mod_ [not, in mathcomp.solvable.extremal] (in type_scope)
'Q_ [not, in mathcomp.solvable.extremal] (in type_scope)
'SD_ [not, in mathcomp.solvable.extremal] (in type_scope)
'T[ ]_ ( , ) [not, in mathcomp.algebra.tensor] (in type_scope)
'T[ ]_ [ , .. , ; , .. , ] [not, in mathcomp.algebra.tensor] (in type_scope)
'T_ ( , ) [not, in mathcomp.algebra.tensor] (in type_scope)
'Z_ [not, in mathcomp.algebra.zmodp] (in type_scope)
'cV[ ]_ [not, in mathcomp.algebra.matrix] (in type_scope)
'cV_ [not, in mathcomp.algebra.matrix] (in type_scope)
'nT[ ]_ ( ) [not, in mathcomp.algebra.tensor] (in type_scope)
'nT[ ]_ [ , .. , ] [not, in mathcomp.algebra.tensor] (in type_scope)
'nT_ ( ) [not, in mathcomp.algebra.tensor] (in type_scope)
'oT[ ]_ ( ) [not, in mathcomp.algebra.tensor] (in type_scope)
'oT[ ]_ [ , .. , ] [not, in mathcomp.algebra.tensor] (in type_scope)
'oT_ ( ) [not, in mathcomp.algebra.tensor] (in type_scope)
'rV[ ]_ [not, in mathcomp.algebra.matrix] (in type_scope)
'rV_ [not, in mathcomp.algebra.matrix] (in type_scope)
'sT [not, in mathcomp.algebra.tensor] (in type_scope)
'sT[ ] [not, in mathcomp.algebra.tensor] (in type_scope)
@ fun_adjunction [not, in mathcomp.boot.fingraph] (in type_scope)
@ rel_adjunction [not, in mathcomp.boot.fingraph] (in type_scope)
[ subg ] [not, in mathcomp.finite_group.fingroup] (in type_scope)
{ 'GL_ ( ) } [not, in mathcomp.algebra.matrix] (in type_scope)
{ 'GL_ [ ] } [not, in mathcomp.algebra.matrix] (in type_scope)
{ ? : | } [not, in mathcomp.boot.eqtype] (in type_scope)
{ ? in | } [not, in mathcomp.boot.eqtype] (in type_scope)
{ ? in } [not, in mathcomp.boot.eqtype] (in type_scope)
{ ? | } [not, in mathcomp.boot.eqtype] (in type_scope)
{ action &-> } [not, in mathcomp.finite_group.action] (in type_scope)
{ acts , on group | } [not, in mathcomp.finite_group.action] (in type_scope)
{ acts , on | } [not, in mathcomp.finite_group.action] (in type_scope)
{ additive -> } [not, in mathcomp.boot.nmodule] (in type_scope)
{ aspace } [not, in mathcomp.field.falgebra] (in type_scope)
{ blmorphism -> } [not, in mathcomp.order.order] (in type_scope)
{ bseq of } [not, in mathcomp.boot.tuple] (in type_scope)
{ dffun } [not, in mathcomp.boot.finfun] (in type_scope)
{ ffun } [not, in mathcomp.boot.finfun] (in type_scope)
{ group } [not, in mathcomp.finite_group.fingroup] (in type_scope)
{ i01 nat } [not, in mathcomp.algebra.interval_inference] (in type_scope)
{ i01 } [not, in mathcomp.algebra.interval_inference] (in type_scope)
{ ideal_quot } [not, in mathcomp.algebra.ring_quotient] (in type_scope)
{ in , isometry , to } [not, in mathcomp.group_representation.classfun] (in type_scope)
{ in , isometry , to } [not, in mathcomp.algebra.sesquilinear] (in type_scope)
{ itv nat & } [not, in mathcomp.algebra.interval_inference] (in type_scope)
{ itv & } [not, in mathcomp.algebra.interval_inference] (in type_scope)
{ jlmorphism -> } [not, in mathcomp.order.order] (in type_scope)
{ linear -> | } [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in type_scope)
{ linear -> } [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in type_scope)
{ lmorphism -> } [not, in mathcomp.order.order] (in type_scope)
{ lrmorphism -> | } [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in type_scope)
{ lrmorphism -> } [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in type_scope)
{ mlmorphism -> } [not, in mathcomp.order.order] (in type_scope)
{ morphism >-> } [not, in mathcomp.finite_group.morphism] (in type_scope)
{ multiplicative -> } [not, in mathcomp.boot.monoid] (in type_scope)
{ omorphism -> } [not, in mathcomp.order.preorder] (in type_scope)
{ perm } [not, in mathcomp.finite_group.perm] (in type_scope)
{ poly %/ } [not, in mathcomp.algebra.qpoly] (in type_scope)
{ poly } [not, in mathcomp.algebra.poly] (in type_scope)
{ posnum nat } [not, in mathcomp.algebra.interval_inference] (in type_scope)
{ quot } [not, in mathcomp.algebra.ring_quotient] (in type_scope)
{ ratio } [not, in mathcomp.algebra.fraction] (in type_scope)
{ rmorphism -> } [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in type_scope)
{ scalar } [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in type_scope)
{ set } [not, in mathcomp.boot.finset] (in type_scope)
{ subfield } [not, in mathcomp.field.fieldext] (in type_scope)
{ subset [ ] } [not, in mathcomp.order.preorder] (in type_scope)
{ subset } [not, in mathcomp.order.preorder] (in type_scope)
{ tblmorphism -> } [not, in mathcomp.order.order] (in type_scope)
{ tlmorphism -> } [not, in mathcomp.order.order] (in type_scope)
{ tuple of } [not, in mathcomp.boot.tuple] (in type_scope)
{ unit } [not, in mathcomp.algebra.finalg] (in type_scope)
{ vspace } [not, in mathcomp.algebra.vector] (in type_scope)
{ in | } [not, in mathcomp.boot.eqtype] (in type_scope)
{ in } [not, in mathcomp.boot.eqtype] (in type_scope)
{poly_ } [not, in mathcomp.algebra.qpoly] (in type_scope)
%:posnat [not, in mathcomp.algebra.interval_inference] (in type_scope)
* [not, in mathcomp.order.preorder] (in type_scope)
* [not, in mathcomp.order.preorder] (in type_scope)
* [not, in mathcomp.order.preorder] (in type_scope)
* [not, in mathcomp.order.preorder] (in type_scope)
* [not, in mathcomp.order.preorder] (in type_scope)
* [not, in mathcomp.order.preorder] (in type_scope)
* [not, in mathcomp.order.preorder] (in type_scope)
* [not, in mathcomp.order.preorder] (in type_scope)
* [not, in mathcomp.order.preorder] (in type_scope)
* [not, in mathcomp.order.preorder] (in type_scope)
* [not, in mathcomp.order.order] (in type_scope)
* [not, in mathcomp.order.order] (in type_scope)
* [not, in mathcomp.order.order] (in type_scope)
* [not, in mathcomp.order.order] (in type_scope)
* [not, in mathcomp.order.order] (in type_scope)
* [not, in mathcomp.order.order] (in type_scope)
* [not, in mathcomp.order.order] (in type_scope)
* [not, in mathcomp.order.order] (in type_scope)
* [not, in mathcomp.order.order] (in type_scope)
* [not, in mathcomp.order.order] (in type_scope)
* [not, in mathcomp.order.order] (in type_scope)
* [not, in mathcomp.order.order] (in type_scope)
* [not, in mathcomp.order.order] (in type_scope)
* [not, in mathcomp.order.order] (in type_scope)
* [not, in mathcomp.order.order] (in type_scope)
*l [not, in mathcomp.order.preorder] (in type_scope)
*lexi[ ] [not, in mathcomp.order.preorder] (in type_scope)
*p [not, in mathcomp.order.preorder] (in type_scope)
*prod[ ] [not, in mathcomp.order.preorder] (in type_scope)
.-bseq [not, in mathcomp.boot.tuple] (in type_scope)
.-tuple [not, in mathcomp.order.preorder] (in type_scope)
.-tuple [not, in mathcomp.order.preorder] (in type_scope)
.-tuple [not, in mathcomp.order.order] (in type_scope)
.-tuple [not, in mathcomp.order.order] (in type_scope)
.-tuple [not, in mathcomp.boot.tuple] (in type_scope)
.-tuplelexi [not, in mathcomp.order.preorder] (in type_scope)
.-tuplelexi[ ] [not, in mathcomp.order.preorder] (in type_scope)
.-tupleprod [not, in mathcomp.order.preorder] (in type_scope)
.-tupleprod[ ] [not, in mathcomp.order.preorder] (in type_scope)
^ [not, in mathcomp.boot.finfun] (in type_scope)
^c [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in type_scope)
^c [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in type_scope)
^d [not, in mathcomp.order.preorder] (in type_scope)
^o [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in type_scope)
^o [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in type_scope)
^z [not, in mathcomp.algebra.ssrint] (in type_scope)
^{1+2* } [not, in mathcomp.solvable.extraspecial] (in type_scope)
^{1+2} [not, in mathcomp.solvable.extraspecial] (in type_scope)

unity_root_scope

.-primitive_root [not, in mathcomp.algebra.poly] (in unity_root_scope)
.-unity_root [not, in mathcomp.algebra.poly] (in unity_root_scope)

vspace_scope

'C ( ) [not, in mathcomp.field.falgebra] (in vspace_scope)
'C ( ) [not, in mathcomp.field.falgebra] (in vspace_scope)
'C [ ] [not, in mathcomp.field.falgebra] (in vspace_scope)
'C [ ] [not, in mathcomp.field.falgebra] (in vspace_scope)
'CF ( ) [not, in mathcomp.group_representation.classfun] (in vspace_scope)
'C_ ( ) ( ) [not, in mathcomp.field.falgebra] (in vspace_scope)
'C_ ( ) [ ] [not, in mathcomp.field.falgebra] (in vspace_scope)
'C_ ( ) [not, in mathcomp.field.falgebra] (in vspace_scope)
'C_ [ ] [not, in mathcomp.field.falgebra] (in vspace_scope)
'Z ( ) [not, in mathcomp.field.falgebra] (in vspace_scope)
'Z ( ) [not, in mathcomp.field.falgebra] (in vspace_scope)
0 [not, in mathcomp.algebra.vector] (in vspace_scope)
1 [not, in mathcomp.field.falgebra] (in vspace_scope)
<< & >> [not, in mathcomp.field.falgebra] (in vspace_scope)
<< & >> [not, in mathcomp.field.falgebra] (in vspace_scope)
<< ; >> [not, in mathcomp.field.falgebra] (in vspace_scope)
<< ; >> [not, in mathcomp.field.falgebra] (in vspace_scope)
<< >> [not, in mathcomp.algebra.vector] (in vspace_scope)
<[ ] > [not, in mathcomp.algebra.vector] (in vspace_scope)
\bigcap_ ( : ) [not, in mathcomp.algebra.vector] (in vspace_scope)
\bigcap_ ( : | ) [not, in mathcomp.algebra.vector] (in vspace_scope)
\bigcap_ ( < ) [not, in mathcomp.algebra.vector] (in vspace_scope)
\bigcap_ ( < | ) [not, in mathcomp.algebra.vector] (in vspace_scope)
\bigcap_ ( <- ) [not, in mathcomp.algebra.vector] (in vspace_scope)
\bigcap_ ( <- | ) [not, in mathcomp.algebra.vector] (in vspace_scope)
\bigcap_ ( <= < ) [not, in mathcomp.algebra.vector] (in vspace_scope)
\bigcap_ ( <= < | ) [not, in mathcomp.algebra.vector] (in vspace_scope)
\bigcap_ ( in ) [not, in mathcomp.algebra.vector] (in vspace_scope)
\bigcap_ ( in | ) [not, in mathcomp.algebra.vector] (in vspace_scope)
\bigcap_ ( | ) [not, in mathcomp.algebra.vector] (in vspace_scope)
\bigcap_ [not, in mathcomp.algebra.vector] (in vspace_scope)
\sum_ ( : ) [not, in mathcomp.algebra.vector] (in vspace_scope)
\sum_ ( : | ) [not, in mathcomp.algebra.vector] (in vspace_scope)
\sum_ ( < ) [not, in mathcomp.algebra.vector] (in vspace_scope)
\sum_ ( < | ) [not, in mathcomp.algebra.vector] (in vspace_scope)
\sum_ ( <- ) [not, in mathcomp.algebra.vector] (in vspace_scope)
\sum_ ( <- | ) [not, in mathcomp.algebra.vector] (in vspace_scope)
\sum_ ( <= < ) [not, in mathcomp.algebra.vector] (in vspace_scope)
\sum_ ( <= < | ) [not, in mathcomp.algebra.vector] (in vspace_scope)
\sum_ ( in ) [not, in mathcomp.algebra.vector] (in vspace_scope)
\sum_ ( in | ) [not, in mathcomp.algebra.vector] (in vspace_scope)
\sum_ ( | ) [not, in mathcomp.algebra.vector] (in vspace_scope)
\sum_ [not, in mathcomp.algebra.vector] (in vspace_scope)
{ : } [not, in mathcomp.algebra.vector] (in vspace_scope)
'_|_ [not, in mathcomp.algebra.sesquilinear] (in vspace_scope)
* [not, in mathcomp.field.falgebra] (in vspace_scope)
* [not, in mathcomp.field.falgebra] (in vspace_scope)
+ [not, in mathcomp.algebra.vector] (in vspace_scope)
:&: [not, in mathcomp.algebra.vector] (in vspace_scope)
:\: [not, in mathcomp.algebra.vector] (in vspace_scope)
<= [not, in mathcomp.algebra.vector] (in vspace_scope)
<= <= [not, in mathcomp.algebra.vector] (in vspace_scope)
@: [not, in mathcomp.algebra.vector] (in vspace_scope)
@^-1: [not, in mathcomp.algebra.vector] (in vspace_scope)
^+ [not, in mathcomp.field.falgebra] (in vspace_scope)
^+ [not, in mathcomp.field.falgebra] (in vspace_scope)
^C [not, in mathcomp.algebra.vector] (in vspace_scope)