Top source

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

!! x [not, in mathcomp.reals.signed] (no scope)
'Alt_T [not, in mathcomp.solvable.alt] (no scope)
'D_ x x [not, in mathcomp.analysis.derive] (no scope)
'D_ x x [not, in mathcomp.analysis.derive] (no scope)
'D_ x x x [not, in mathcomp.analysis.derive] (no scope)
'D_ x x x [not, in mathcomp.analysis.derive] (no scope)
'I_ x [not, in mathcomp.boot.fintype] (no scope)
'J x x [not, in mathcomp.analysis.derive] (no scope)
'M_ x x [not, in mathcomp.analysis.probability_theory.random_variable] (no scope)
'N_ x [ x ] [not, in mathcomp.analysis.hoelder] (no scope)
'N_ x [ x ] [not, in mathcomp.analysis.hoelder] (no scope)
'N_ x [ x ] [not, in mathcomp.analysis.hoelder] (no scope)
'N_ x [ x ] [not, in mathcomp.analysis.hoelder] (no scope)
'O [not, in mathcomp.analysis.landau] (no scope)
'O '_' x [not, in mathcomp.analysis.landau] (no scope)
'O '_' x [not, in mathcomp.analysis.landau] (no scope)
'O _( x \near x ) x [not, in mathcomp.analysis.landau] (no scope)
'O _( x \near x ) x [not, in mathcomp.analysis.landau] (no scope)
'O_ x [not, in mathcomp.analysis.landau] (no scope)
'O_ x x [not, in mathcomp.analysis.landau] (no scope)
'O_ x x [not, in mathcomp.analysis.landau] (no scope)
'O_( x \near x ) x [not, in mathcomp.analysis.landau] (no scope)
'O_( x \near x ) x [not, in mathcomp.analysis.landau] (no scope)
'Omega_ x x [not, in mathcomp.analysis.landau] (no scope)
'Omega_ x x [not, in mathcomp.analysis.landau] (no scope)
'Phi_ x [not, in mathcomp.field.cyclotomic] (no scope)
'S_ x [not, in mathcomp.finite_group.perm] (no scope)
'Sym_T [not, in mathcomp.solvable.alt] (no scope)
'T[ x ] [not, in mathcomp.algebra.tensor] (no scope)
'T[ x ] [not, in mathcomp.algebra.tensor] (no scope)
'Theta_ x x [not, in mathcomp.analysis.landau] (no scope)
'Theta_ x x [not, in mathcomp.analysis.landau] (no scope)
'V_ x [ x ] [not, in mathcomp.analysis.probability_theory.random_variable] (no scope)
'V_ x [ x ] [not, in mathcomp.analysis.probability_theory.random_variable] (no scope)
'X [not, in mathcomp.algebra.poly] (no scope)
'X^ x [not, in mathcomp.algebra.poly] (no scope)
'a_O_ x x [not, in mathcomp.analysis.landau] (no scope)
'a_O_ x x [not, in mathcomp.analysis.landau] (no scope)
'a_O_( x \near x ) x [not, in mathcomp.analysis.landau] (no scope)
'a_O_( x \near x ) x [not, in mathcomp.analysis.landau] (no scope)
'a_o_ x x [not, in mathcomp.analysis.landau] (no scope)
'a_o_ x x [not, in mathcomp.analysis.landau] (no scope)
'a_o_( x \near x ) x [not, in mathcomp.analysis.landau] (no scope)
'a_o_( x \near x ) x [not, in mathcomp.analysis.landau] (no scope)
'all_ x [not, in mathcomp.boot.seq] (no scope)
'd x '/d x [not, in mathcomp.analysis.charge] (no scope)
'd x '/d x [not, in mathcomp.analysis.charge] (no scope)
'd x x [not, in mathcomp.analysis.derive] (no scope)
'd x x [not, in mathcomp.analysis.derive] (no scope)
'd x x [not, in mathcomp.analysis.derive] (no scope)
'd1 x [not, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_under] (no scope)
'd1 x [not, in mathcomp.analysis.gauss_integral] (no scope)
'exists_ x [not, in mathcomp.boot.fintype] (no scope)
'exists_in_ x [not, in mathcomp.boot.fintype] (no scope)
'forall_ x [not, in mathcomp.boot.fintype] (no scope)
'forall_in_ x [not, in mathcomp.boot.fintype] (no scope)
'has_ x [not, in mathcomp.boot.seq] (no scope)
'if x then x else x [not, in mathcomp.field.closed_field] (no scope)
'let x <- x ; x [not, in mathcomp.field.closed_field] (no scope)
'nX^ x [not, in mathcomp.algebra.qpoly] (no scope)
'o [not, in mathcomp.analysis.landau] (no scope)
'o '_' x [not, in mathcomp.analysis.landau] (no scope)
'o '_' x [not, in mathcomp.analysis.landau] (no scope)
'o _( x \near x ) x [not, in mathcomp.analysis.landau] (no scope)
'o _( x \near x ) x [not, in mathcomp.analysis.landau] (no scope)
'o_ x [not, in mathcomp.analysis.landau] (no scope)
'o_ x x [not, in mathcomp.analysis.landau] (no scope)
'o_ x x [not, in mathcomp.analysis.landau] (no scope)
'o_( x \near x ) x [not, in mathcomp.analysis.landau] (no scope)
'o_( x \near x ) x [not, in mathcomp.analysis.landau] (no scope)
'oinv_ x [not, in mathcomp.classical.functions] (no scope)
'qX [not, in mathcomp.algebra.qpoly] (no scope)
( x ) [not, in mathcomp.finite_group.presentation] (no scope)
*%E [not, in mathcomp.reals.constructive_ereal] (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)
+%E [not, in mathcomp.reals.constructive_ereal] (no scope)
+%E [not, in mathcomp.reals.constructive_ereal] (no scope)
+%E [not, in mathcomp.reals.constructive_ereal] (no scope)
+%M [not, in mathcomp.boot.bigop] (no scope)
+%N [not, in mathcomp.boot.bigop] (no scope)
+%dE [not, in mathcomp.reals.constructive_ereal] (no scope)
+%dE [not, in mathcomp.reals.constructive_ereal] (no scope)
+%dE [not, in mathcomp.reals.constructive_ereal] (no scope)
+oo [not, in mathcomp.analysis.normedtype_theory.normed_module] (no scope)
+oo [not, in mathcomp.analysis.landau] (no scope)
-%E [not, in mathcomp.reals.constructive_ereal] (no scope)
0 [not, in mathcomp.boot.bigop] (no scope)
1 [not, in mathcomp.finmap.finperm] (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)
<< x ; x >> [not, in mathcomp.field.algebraics_fundamentals] (no scope)
@ ffun_on x x [not, in mathcomp.boot.finfun] (no scope)
@ gee x [not, in mathcomp.reals.constructive_ereal] (no scope)
@ gte x [not, in mathcomp.reals.constructive_ereal] (no scope)
@ lee x [not, in mathcomp.reals.constructive_ereal] (no scope)
@ lte x [not, in mathcomp.reals.constructive_ereal] (no scope)
[ bounded x | x in x ] [not, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule] (no scope)
[ cmp0 of x ] [not, in mathcomp.reals.signed] (no scope)
[ cmp0 of x ] [not, in mathcomp.algebra.interval_inference] (no scope)
[ ge0 of x ] [not, in mathcomp.reals.signed] (no scope)
[ ge0 of x ] [not, in mathcomp.algebra.interval_inference] (no scope)
[ gt0 of x ] [not, in mathcomp.reals.signed] (no scope)
[ gt0 of x ] [not, in mathcomp.algebra.interval_inference] (no scope)
[ le0 of x ] [not, in mathcomp.reals.signed] (no scope)
[ le0 of x ] [not, in mathcomp.algebra.interval_inference] (no scope)
[ locally x ] [not, in mathcomp.analysis.topology_theory.topology_structure] (no scope)
[ locally x ] [not, in mathcomp.analysis.topology_theory.topology_structure] (no scope)
[ lt0 of x ] [not, in mathcomp.reals.signed] (no scope)
[ lt0 of x ] [not, in mathcomp.algebra.interval_inference] (no scope)
[ neq0 of x ] [not, in mathcomp.reals.signed] (no scope)
[ neq0 of x ] [not, in mathcomp.algebra.interval_inference] (no scope)
[ rec x , x , x , x , x , x ] [not, in mathcomp.boot.prime] (no scope)
[ rec x , x , x ] [not, in mathcomp.boot.choice] (no scope)
[ rec x , x ] [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (no scope)
[ seq x : x <- x | x & x ] [not, in mathcomp.boot.seq] (no scope)
[ seq x : x <- x | x ] [not, in mathcomp.boot.seq] (no scope)
[ ~ x , x , .. , x ] [not, in mathcomp.finite_group.presentation] (no scope)
[ x : x | x ] [not, in mathcomp.boot.fintype] (no scope)
[ x | x ] [not, in mathcomp.boot.fintype] (no scope)
[O '_' x x of x ] [not, in mathcomp.analysis.landau] (no scope)
[O '_' x x of x ] [not, in mathcomp.analysis.landau] (no scope)
[O _( x \near x ) x of x ] [not, in mathcomp.analysis.landau] (no scope)
[O _( x \near x ) x of x ] [not, in mathcomp.analysis.landau] (no scope)
[O_ x x of x ] [not, in mathcomp.analysis.landau] (no scope)
[O_ x x of x ] [not, in mathcomp.analysis.landau] (no scope)
[O_( x \near x ) x of x ] [not, in mathcomp.analysis.landau] (no scope)
[O_( x \near x ) x of x ] [not, in mathcomp.analysis.landau] (no scope)
[Omega '_' x x of x ] [not, in mathcomp.analysis.landau] (no scope)
[Omega '_' x x of x ] [not, in mathcomp.analysis.landau] (no scope)
[Omega_ x x of x ] [not, in mathcomp.analysis.landau] (no scope)
[Omega_ x x of x ] [not, in mathcomp.analysis.landau] (no scope)
[Theta '_' x x of x ] [not, in mathcomp.analysis.landau] (no scope)
[Theta '_' x x of x ] [not, in mathcomp.analysis.landau] (no scope)
[Theta_ x x of x ] [not, in mathcomp.analysis.landau] (no scope)
[Theta_ x x of x ] [not, in mathcomp.analysis.landau] (no scope)
[bigO of x ] [not, in mathcomp.analysis.landau] (no scope)
[bigO of x ] [not, in mathcomp.analysis.landau] (no scope)
[bigO of x for x ] [not, in mathcomp.analysis.landau] (no scope)
[bigO of x for x ] [not, in mathcomp.analysis.landau] (no scope)
[bigOmega of x ] [not, in mathcomp.analysis.landau] (no scope)
[bigOmega of x ] [not, in mathcomp.analysis.landau] (no scope)
[bigOmega of x for x ] [not, in mathcomp.analysis.landau] (no scope)
[bigTheta of x ] [not, in mathcomp.analysis.landau] (no scope)
[bigTheta of x ] [not, in mathcomp.analysis.landau] (no scope)
[bigTheta of x for x ] [not, in mathcomp.analysis.landau] (no scope)
[littleo of x ] [not, in mathcomp.analysis.landau] (no scope)
[littleo of x ] [not, in mathcomp.analysis.landau] (no scope)
[littleo of x for x ] [not, in mathcomp.analysis.landau] (no scope)
[littleo of x for x ] [not, in mathcomp.analysis.landau] (no scope)
[o '_' x x of x ] [not, in mathcomp.analysis.landau] (no scope)
[o '_' x x of x ] [not, in mathcomp.analysis.landau] (no scope)
[o '_' x x of x ] [not, in mathcomp.analysis.landau] (no scope)
[o _( x \near x ) x of x ] [not, in mathcomp.analysis.landau] (no scope)
[o _( x \near x ) x of x ] [not, in mathcomp.analysis.landau] (no scope)
[o_ x x of x ] [not, in mathcomp.analysis.landau] (no scope)
[o_ x x of x ] [not, in mathcomp.analysis.landau] (no scope)
[o_ x x of x ] [not, in mathcomp.analysis.landau] (no scope)
[o_( x \near x ) x of x ] [not, in mathcomp.analysis.landau] (no scope)
[o_( x \near x ) x of x ] [not, in mathcomp.analysis.landau] (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_ x [not, in mathcomp.algebra.fraction] (no scope)
\esum_ ( x in x ) x [not, in mathcomp.analysis.esum] (no scope)
\int_ ( x in x ) x [not, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_definition] (no scope)
\mpi [not, in mathcomp.boot.generic_quotient] (no scope)
\n_ x [not, in mathcomp.algebra.fraction] (no scope)
\pi [not, in mathcomp.boot.generic_quotient] (no scope)
\poly_ ( x < x ) x [not, in mathcomp.algebra.poly] (no scope)
\prod_ ( x <- x | x ) x [not, in mathcomp.boot.monoid] (no scope)
\prod_ ( x <- x | x ) x [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (no scope)
\prod_ ( x <= x < x ) x [not, in mathcomp.boot.monoid] (no scope)
\prod_ ( x <= x < x ) x [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (no scope)
\prod_ ( x in x ) x [not, in mathcomp.boot.monoid] (no scope)
\prod_ ( x in x ) x [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (no scope)
\prod_ ( x | x ) x [not, in mathcomp.boot.monoid] (no scope)
\prod_ ( x | x ) x [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (no scope)
\sum_ ( x < x ) x [not, in mathcomp.boot.nmodule] (no scope)
\sum_ ( x <- x | x ) x [not, in mathcomp.boot.nmodule] (no scope)
\sum_ ( x <= x < x ) x [not, in mathcomp.boot.nmodule] (no scope)
\sum_ ( x in x ) x [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)
`I_ x [not, in mathcomp.classical.classical_sets] (no scope)
decreasing_fun x [not, in mathcomp.analysis.numfun] (no scope)
decreasing_seq x [not, in mathcomp.analysis.sequences] (no scope)
increasing_fun x [not, in mathcomp.analysis.numfun] (no scope)
increasing_seq x [not, in mathcomp.analysis.sequences] (no scope)
is_diff x [not, in mathcomp.analysis.derive] (no scope)
mu^* [not, in mathcomp.analysis.measure_theory.measure_extension] (no scope)
nondecreasing_fun x [not, in mathcomp.analysis.numfun] (no scope)
nondecreasing_seq x [not, in mathcomp.analysis.sequences] (no scope)
nonincreasing_fun x [not, in mathcomp.analysis.numfun] (no scope)
nonincreasing_seq x [not, in mathcomp.analysis.sequences] (no scope)
weak_open x [not, in mathcomp.analysis.topology_theory.function_spaces] (no scope)
{ all1 x } [not, in mathcomp.classical.filter] (no scope)
{ all2 x } [not, in mathcomp.classical.filter] (no scope)
{ all3 x } [not, in mathcomp.classical.filter] (no scope)
{ allA x } [not, in mathcomp.classical.wochoice] (no scope)
{ compact-open , x --> x } [not, in mathcomp.analysis.topology_theory.function_spaces] (no scope)
{ compact-open , x -> x } [not, in mathcomp.analysis.topology_theory.function_spaces] (no scope)
{ family x , x -> x } [not, in mathcomp.analysis.topology_theory.function_spaces] (no scope)
{ fraction x } [not, in mathcomp.algebra.fraction] (no scope)
{ poly %/ x with x } [not, in mathcomp.field.qfpoly] (no scope)
{ subset x } [not, in mathcomp.order.preorder] (no scope)
{ subset x } [not, in mathcomp.order.order] (no scope)
{O_ x x } [not, in mathcomp.analysis.landau] (no scope)
{O_ x x } [not, in mathcomp.analysis.landau] (no scope)
{Omega_ x x } [not, in mathcomp.analysis.landau] (no scope)
{Omega_ x x } [not, in mathcomp.analysis.landau] (no scope)
{Theta_ x x } [not, in mathcomp.analysis.landau] (no scope)
{Theta_ x x } [not, in mathcomp.analysis.landau] (no scope)
{o_ x x } [not, in mathcomp.analysis.landau] (no scope)
{o_ x x } [not, in mathcomp.analysis.landau] (no scope)
{o_ x x } [not, in mathcomp.analysis.landau] (no scope)
{subset x <= x } [not, in mathcomp.order.order] (no scope)
x [not, in mathcomp.finite_group.presentation] (no scope)
x %:E [not, in mathcomp.reals.constructive_ereal] (no scope)
x %:F [not, in mathcomp.algebra.fraction] (no scope)
x %:F [not, in mathcomp.algebra.fraction] (no scope)
x %:P [not, in mathcomp.algebra.poly] (no scope)
x %:R [not, in mathcomp.solvable.extremal] (no scope)
x %:R [not, in mathcomp.solvable.extraspecial] (no scope)
x %| x [not, in mathcomp.field.finfield] (no scope)
x * x [not, in mathcomp.finite_group.presentation] (no scope)
x * x [not, in mathcomp.finite_group.fingroup] (no scope)
x * x [not, in mathcomp.boot.bigop] (no scope)
x * x [not, in mathcomp.boot.bigop] (no scope)
x * x [not, in mathcomp.boot.bigop] (no scope)
x * x [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (no scope)
x *:l x [not, in mathcomp.algebra.vector] (no scope)
x *? x [not, in mathcomp.reals.constructive_ereal] (no scope)
x *F0: x [not, in mathcomp.field.fieldext] (no scope)
x *F: x [not, in mathcomp.field.fieldext] (no scope)
x *` x [not, in mathcomp.analysis.normedtype_theory.vitali_lemma] (no scope)
x *p': x [not, in mathcomp.field.finfield] (no scope)
x + x [not, in mathcomp.boot.bigop] (no scope)
x +? x [not, in mathcomp.reals.constructive_ereal] (no scope)
x , x , .. , x [not, in mathcomp.finite_group.presentation] (no scope)
x ->_ x x [not, in mathcomp.field.closed_field] (no scope)
x .-fker x ~> x [not, in mathcomp.analysis.kernel] (no scope)
x .-ftker x ~> x [not, in mathcomp.analysis.kernel] (no scope)
x .-ker x ~> x [not, in mathcomp.analysis.kernel] (no scope)
x .-negligible [not, in mathcomp.analysis.measure_theory.measure_negligible] (no scope)
x .-null_set [not, in mathcomp.analysis.measure_theory.measure_negligible] (no scope)
x .-pker x ~> x [not, in mathcomp.analysis.kernel] (no scope)
x .-ring [not, in mathcomp.analysis.measure_theory.measure_function] (no scope)
x .-ring.-measurable [not, in mathcomp.analysis.measure_theory.measure_function] (no scope)
x .-root [not, in mathcomp.algebra.numeric_hierarchy.numfield] (no scope)
x .-sesqui [not, in mathcomp.algebra.sesquilinear] (no scope)
x .-sfker x ~> x [not, in mathcomp.analysis.kernel] (no scope)
x .-sigmafker x ~> x [not, in mathcomp.analysis.kernel] (no scope)
x .-spker x ~> x [not, in mathcomp.analysis.kernel] (no scope)
x .-tuplelexi [not, in mathcomp.order.preorder] (no scope)
x .-tupleprod [not, in mathcomp.order.preorder] (no scope)
x .[ AC x x ] [not, in mathcomp.boot.ssrAC] (no scope)
x .[ ACl x ] [not, in mathcomp.boot.ssrAC] (no scope)
x .[ ACof x x ] [not, in mathcomp.boot.ssrAC] (no scope)
x / x [not, in mathcomp.algebra.algebraic_hierarchy.divalg] (no scope)
x : x [not, in mathcomp.finite_group.presentation] (no scope)
x < x [not, in mathcomp.classical.boolp] (no scope)
x <= x [not, in mathcomp.classical.boolp] (no scope)
x <| x |> x [not, in mathcomp.analysis.convex] (no scope)
x = x [not, in mathcomp.finite_group.presentation] (no scope)
x = x %[ae x ] [not, in mathcomp.analysis.measure_theory.measure_negligible] (no scope)
x = x %[ae x in x ] [not, in mathcomp.analysis.measure_theory.measure_negligible] (no scope)
x = x +O_ x x [not, in mathcomp.analysis.landau] (no scope)
x = x +O_ x x [not, in mathcomp.analysis.landau] (no scope)
x = x +O_( x \near x ) x [not, in mathcomp.analysis.landau] (no scope)
x = x +O_( x \near x ) x [not, in mathcomp.analysis.landau] (no scope)
x = x +o_ x x [not, in mathcomp.analysis.landau] (no scope)
x = x +o_ x x [not, in mathcomp.analysis.landau] (no scope)
x = x +o_( x \near x ) x [not, in mathcomp.analysis.landau] (no scope)
x = x +o_( x \near x ) x [not, in mathcomp.analysis.landau] (no scope)
x = x = x [not, in mathcomp.finite_group.presentation] (no scope)
x == x +O_ x x [not, in mathcomp.analysis.landau] (no scope)
x == x +O_ x x [not, in mathcomp.analysis.landau] (no scope)
x == x +O_( x \near x ) x [not, in mathcomp.analysis.landau] (no scope)
x == x +O_( x \near x ) x [not, in mathcomp.analysis.landau] (no scope)
x == x +o_ x x [not, in mathcomp.analysis.landau] (no scope)
x == x +o_ x x [not, in mathcomp.analysis.landau] (no scope)
x == x +o_( x \near x ) x [not, in mathcomp.analysis.landau] (no scope)
x == x +o_( x \near x ) x [not, in mathcomp.analysis.landau] (no scope)
x ==O_ x x [not, in mathcomp.analysis.landau] (no scope)
x ==O_ x x [not, in mathcomp.analysis.landau] (no scope)
x ==O_( x \near x ) x [not, in mathcomp.analysis.landau] (no scope)
x ==O_( x \near x ) x [not, in mathcomp.analysis.landau] (no scope)
x ==o_ x x [not, in mathcomp.analysis.landau] (no scope)
x ==o_ x x [not, in mathcomp.analysis.landau] (no scope)
x ==o_( x \near x ) x [not, in mathcomp.analysis.landau] (no scope)
x ==o_( x \near x ) x [not, in mathcomp.analysis.landau] (no scope)
x =O_ x x [not, in mathcomp.analysis.landau] (no scope)
x =O_ x x [not, in mathcomp.analysis.landau] (no scope)
x =O_( x \near x ) x [not, in mathcomp.analysis.landau] (no scope)
x =O_( x \near x ) x [not, in mathcomp.analysis.landau] (no scope)
x =Omega_ x x [not, in mathcomp.analysis.landau] (no scope)
x =Omega_ x x [not, in mathcomp.analysis.landau] (no scope)
x =Theta_ x x [not, in mathcomp.analysis.landau] (no scope)
x =Theta_ x x [not, in mathcomp.analysis.landau] (no scope)
x =o_ x x [not, in mathcomp.analysis.landau] (no scope)
x =o_ x x [not, in mathcomp.analysis.landau] (no scope)
x =o_( x \near x ) x [not, in mathcomp.analysis.landau] (no scope)
x =o_( x \near x ) x [not, in mathcomp.analysis.landau] (no scope)
x >>= x [not, in mathcomp.analysis.lebesgue_integral_theory.giry] (no scope)
x \char x [not, in mathcomp.finite_group.automorphism] (no scope)
x \in x [not, in mathcomp.algebra.mxalgebra] (no scope)
x \is_near x [not, in mathcomp.classical.filter] (no scope)
x \isog x [not, in mathcomp.finite_group.morphism] (no scope)
x \isog x [not, in mathcomp.finite_group.morphism] (no scope)
x ^ x [not, in mathcomp.finite_group.presentation] (no scope)
x ^ x [not, in mathcomp.algebra.matrix] (no scope)
x ^* [not, in mathcomp.boot.fintype] (no scope)
x ^* [not, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation] (no scope)
x ^* [not, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation] (no scope)
x ^+ x [not, in mathcomp.finite_group.presentation] (no scope)
x ^- x [not, in mathcomp.finite_group.presentation] (no scope)
x ^- x [not, in mathcomp.algebra.algebraic_hierarchy.divalg] (no scope)
x ^-1 [not, in mathcomp.finite_group.presentation] (no scope)
x ^-1 [not, in mathcomp.finite_group.fingroup] (no scope)
x ^-1 [not, in mathcomp.algebra.algebraic_hierarchy.divalg] (no scope)
x ^^ x [not, in mathcomp.field.algC] (no scope)
x ^` ( x ) [not, in mathcomp.analysis.derive] (no scope)
x ^` () [not, in mathcomp.analysis.derive] (no scope)
x ^` () [not, in mathcomp.algebra.poly] (no scope)
x ^f [not, in mathcomp.algebra.ssrint] (no scope)
x ^f [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (no scope)
x ^f [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (no scope)
x ^° [not, in mathcomp.analysis.topology_theory.topology_structure] (no scope)
x `<< x [not, in mathcomp.analysis.measure_theory.measure_negligible] (no scope)
x `<=` x [not, in mathcomp.classical.classical_sets] (no scope)
x `^ x [not, in mathcomp.analysis.exp] (no scope)
x `^ x [not, in mathcomp.analysis.exp] (no scope)
x ~_ x x [not, in mathcomp.analysis.landau] (no scope)
x ~_ x x [not, in mathcomp.algebra.mxpoly] (no scope)
x ~_{in x } { in x } [not, in mathcomp.algebra.mxpoly] (no scope)
x ~_{in x } x [not, in mathcomp.algebra.mxpoly] (no scope)
x ~~_ x x [not, in mathcomp.analysis.landau] (no scope)
x ° [not, in mathcomp.analysis.topology_theory.topology_structure] (no scope)
x ≡μ x [not, in mathcomp.analysis.lebesgue_integral_theory.giry] (no scope)

AC_scope

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

C_expanded_scope

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

C_scope

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

Group_scope

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

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)
'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)
<< x >> [not, in mathcomp.finite_group.action] (in action_scope)
<[ x ] > [not, in mathcomp.finite_group.action] (in action_scope)
<[nRA]> [not, in mathcomp.finite_group.action] (in action_scope)
[ Aut x ] [not, in mathcomp.finite_group.action] (in action_scope)
x %% x [not, in mathcomp.finite_group.action] (in action_scope)
x * x [not, in mathcomp.solvable.primitive_action] (in action_scope)
x / x [not, in mathcomp.finite_group.action] (in action_scope)
x \ x [not, in mathcomp.finite_group.action] (in action_scope)
x \o x [not, in mathcomp.finite_group.action] (in action_scope)
x ^* [not, in mathcomp.finite_group.action] (in action_scope)
x ^? [not, in mathcomp.finite_group.action] (in action_scope)

algC_expanded_scope

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

algC_scope

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

aspace_scope

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

big_scope

\big [ x / x ]_ ( x : x ) x [not, in mathcomp.boot.bigop] (in big_scope)
\big [ x / x ]_ ( x : x | x ) x [not, in mathcomp.boot.bigop] (in big_scope)
\big [ x / x ]_ ( x < x ) x [not, in mathcomp.boot.bigop] (in big_scope)
\big [ x / x ]_ ( x < x | x ) x [not, in mathcomp.boot.bigop] (in big_scope)
\big [ x / x ]_ ( x <- x ) x [not, in mathcomp.boot.bigop] (in big_scope)
\big [ x / x ]_ ( x <- x | x ) x [not, in mathcomp.boot.bigop] (in big_scope)
\big [ x / x ]_ ( x <= x < x ) x [not, in mathcomp.boot.bigop] (in big_scope)
\big [ x / x ]_ ( x <= x < x | x ) x [not, in mathcomp.boot.bigop] (in big_scope)
\big [ x / x ]_ ( x <= x <oo ) x [not, in mathcomp.analysis.sequences] (in big_scope)
\big [ x / x ]_ ( x <= x <oo | x ) x [not, in mathcomp.analysis.sequences] (in big_scope)
\big [ x / x ]_ ( x <oo ) x [not, in mathcomp.analysis.sequences] (in big_scope)
\big [ x / x ]_ ( x <oo | x ) x [not, in mathcomp.analysis.sequences] (in big_scope)
\big [ x / x ]_ ( x \in x ) x [not, in mathcomp.classical.fsbigop] (in big_scope)
\big [ x / x ]_ ( x \in x ) x [not, in mathcomp.classical.fsbigop] (in big_scope)
\big [ x / x ]_ ( x in x ) x [not, in mathcomp.boot.bigop] (in big_scope)
\big [ x / x ]_ ( x in x | x ) x [not, in mathcomp.boot.bigop] (in big_scope)
\big [ x / x ]_ ( x | x ) x [not, in mathcomp.boot.bigop] (in big_scope)
\big [ x / x ]_ x x [not, in mathcomp.boot.bigop] (in big_scope)

bool_scope

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

card_scope

x #!= x [not, in mathcomp.classical.cardinality] (in card_scope)
x #<= x [not, in mathcomp.classical.cardinality] (in card_scope)
x #= x [not, in mathcomp.classical.cardinality] (in card_scope)
x #>= x [not, in mathcomp.classical.cardinality] (in card_scope)

charge_scope

'd x '/d x [not, in mathcomp.analysis.charge] (in charge_scope)
x .-negative_set [not, in mathcomp.analysis.charge] (in charge_scope)
x .-positive_set [not, in mathcomp.analysis.charge] (in charge_scope)

classical_set_scope

'measurable [not, in mathcomp.analysis.measure_theory.measurable_structure] (in classical_set_scope)
<<M x >> [not, in mathcomp.analysis.measure_theory.measurable_structure] (in classical_set_scope)
<<d x >> [not, in mathcomp.analysis.measure_theory.measurable_structure] (in classical_set_scope)
<<l x , x >> [not, in mathcomp.analysis.measure_theory.measurable_structure] (in classical_set_scope)
<<l x >> [not, in mathcomp.analysis.measure_theory.measurable_structure] (in classical_set_scope)
<<r x >> [not, in mathcomp.analysis.measure_theory.measurable_structure] (in classical_set_scope)
<<s x , x >> [not, in mathcomp.analysis.measure_theory.measurable_structure] (in classical_set_scope)
<<s x >> [not, in mathcomp.analysis.measure_theory.measurable_structure] (in classical_set_scope)
<<sr x >> [not, in mathcomp.analysis.measure_theory.measurable_structure] (in classical_set_scope)
[ cvg x in x ] [not, in mathcomp.classical.filter] (in classical_set_scope)
[ disjoint x & x ] [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
[ lim x in x ] [not, in mathcomp.classical.filter] (in classical_set_scope)
[ set : x ] [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
[ set ~ x ] [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
[ set x : x ] [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
[ set x : x | x ] [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
[ set x ; x ; .. ; x ] [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
[ set x ] [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
[ set x | x ] [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
[ set x | x in x & x in x ] [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
[ set x | x in x ] [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
[ set` x ] [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
\bigcap_ ( x : x ) x [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
\bigcap_ ( x < x ) x [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
\bigcap_ ( x >= x ) x [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
\bigcap_ ( x in x ) x [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
\bigcap_ x x [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
\bigcup_ ( x : x ) x [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
\bigcup_ ( x < x ) x [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
\bigcup_ ( x >= x ) x [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
\bigcup_ ( x in x ) x [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
\bigcup_ x x [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
\oo [not, in mathcomp.classical.filter] (in classical_set_scope)
`[ x , +oo [ [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
`[ x , x [ [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
`[ x , x ] [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
`] -oo , +oo [ [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
`] -oo , x [ [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
`] -oo , x ] [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
`] x , +oo [ [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
`] x , x [ [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
`] x , x ] [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
{ ptws , x --> x } [not, in mathcomp.analysis.topology_theory.function_spaces] (in classical_set_scope)
{ uniform , x --> x } [not, in mathcomp.analysis.topology_theory.function_spaces] (in classical_set_scope)
{ uniform x , x --> x } [not, in mathcomp.analysis.topology_theory.function_spaces] (in classical_set_scope)
{ within x , continuous x } [not, in mathcomp.analysis.topology_theory.subspace_topology] (in classical_set_scope)
~` x [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
x !=set0 [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
x *` x [not, in mathcomp.analysis.normedtype_theory.vitali_lemma] (in classical_set_scope)
x --> x [not, in mathcomp.classical.filter] (in classical_set_scope)
x .-cara.-measurable [not, in mathcomp.analysis.measure_theory.measure_extension] (in classical_set_scope)
x .-caratheodory [not, in mathcomp.analysis.measure_theory.measure_extension] (in classical_set_scope)
x .-measurable [not, in mathcomp.analysis.measure_theory.measurable_structure] (in classical_set_scope)
x .-ocitv.-measurable [not, in mathcomp.analysis.lebesgue_stieltjes_measure] (in classical_set_scope)
x .-preimage.-measurable [not, in mathcomp.analysis.measure_theory.measurable_structure] (in classical_set_scope)
x .-prod.-measurable [not, in mathcomp.analysis.measure_theory.measurable_structure] (in classical_set_scope)
x .-ring.-measurable [not, in mathcomp.analysis.measure_theory.measure_function] (in classical_set_scope)
x .-sigma.-measurable [not, in mathcomp.analysis.measure_theory.measurable_structure] (in classical_set_scope)
x .`1 [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
x .`2 [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
x @ x [not, in mathcomp.classical.filter] (in classical_set_scope)
x @[ x --> x ] [not, in mathcomp.classical.filter] (in classical_set_scope)
x @[ x \oo ] [not, in mathcomp.classical.filter] (in classical_set_scope)
x @^-1` x [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
x @` x [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
x @`[ x , x ] [not, in mathcomp.analysis.normedtype_theory.num_normedtype] (in classical_set_scope)
x @`] x , x [ [not, in mathcomp.analysis.normedtype_theory.num_normedtype] (in classical_set_scope)
x ^' [not, in mathcomp.analysis.topology_theory.topology_structure] (in classical_set_scope)
x ^'+ [not, in mathcomp.analysis.topology_theory.num_topology] (in classical_set_scope)
x ^'+ [not, in mathcomp.analysis.topology_theory.num_topology] (in classical_set_scope)
x ^'- [not, in mathcomp.analysis.topology_theory.num_topology] (in classical_set_scope)
x ^'- [not, in mathcomp.analysis.topology_theory.num_topology] (in classical_set_scope)
x ^` ( x ) [not, in mathcomp.analysis.derive] (in classical_set_scope)
x ^` () [not, in mathcomp.analysis.derive] (in classical_set_scope)
x `#` x [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
x `&` x [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
x `*` x [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
x `*`` x [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
x `+` x [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
x `<=>` x [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
x `<=` x [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
x `<` x [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
x `=>` x [not, in mathcomp.classical.filter] (in classical_set_scope)
x `@ x [not, in mathcomp.classical.filter] (in classical_set_scope)
x `@[ x --> x ] [not, in mathcomp.classical.filter] (in classical_set_scope)
x `\ x [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
x `\` x [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
x ``*` x [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
x `|` x [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
x |` x [not, in mathcomp.classical.classical_sets] (in classical_set_scope)
x ° [not, in mathcomp.analysis.topology_theory.topology_structure] (in classical_set_scope)

convex_scope

x <| x |> x [not, in mathcomp.analysis.convex] (in convex_scope)

coq_nat_scope

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

distn_scope

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

eq_scope

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

ereal_dual_scope

+oo [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
- 1 [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
- x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
-oo [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
0 [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
1 [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
\- x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
\sum_ ( x : x ) x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
\sum_ ( x : x | x ) x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
\sum_ ( x < x ) x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
\sum_ ( x < x | x ) x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
\sum_ ( x <- x ) x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
\sum_ ( x <- x | x ) x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
\sum_ ( x <= x < x ) x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
\sum_ ( x <= x < x | x ) x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
\sum_ ( x \in x ) x [not, in mathcomp.analysis.ereal] (in ereal_dual_scope)
\sum_ ( x in x ) x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
\sum_ ( x in x | x ) x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
\sum_ ( x | x ) x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
\sum_ x x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
`| x | [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x %:E [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x %:dE [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x %:nng [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x %:nng [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x %:pos [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x %:pos [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x * x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x *+ x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x *? x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x + x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x + x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x + x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x +? x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x - x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x - x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x - x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x / x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x < x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x < x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x < x < x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x < x < x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x < x <= x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x < x <= x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x <= x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x <= x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x <= x < x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x <= x < x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x <= x <= x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x <= x <= x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x > x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x >= x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x \* x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x \+ x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x \+ x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x \+ x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x \- x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x \- x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x \- x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x ^+ x [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)
x ^-1 [not, in mathcomp.reals.constructive_ereal] (in ereal_dual_scope)

ereal_scope

'E_ x [ x ] [not, in mathcomp.analysis.probability_theory.random_variable] (in ereal_scope)
'N[ x ]_ x [ x ] [not, in mathcomp.analysis.hoelder] (in ereal_scope)
+oo [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
- 1 [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
- x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
-oo [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
0 [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
1 [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
[ sequence x ]_ x [not, in mathcomp.analysis.sequences] (in ereal_scope)
[ series x ]_ x [not, in mathcomp.analysis.sequences] (in ereal_scope)
\- x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
\int [ x ]_ ( x in x ) x [not, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_definition] (in ereal_scope)
\int [ x ]_ x x [not, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_definition] (in ereal_scope)
\prod_ ( x : x ) x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
\prod_ ( x : x | x ) x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
\prod_ ( x < x ) x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
\prod_ ( x < x | x ) x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
\prod_ ( x <- x ) x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
\prod_ ( x <- x | x ) x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
\prod_ ( x <= x < x ) x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
\prod_ ( x <= x < x | x ) x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
\prod_ ( x in x ) x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
\prod_ ( x in x | x ) x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
\prod_ ( x | x ) x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
\prod_ x x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
\sum_ ( x : x ) x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
\sum_ ( x : x | x ) x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
\sum_ ( x < x ) x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
\sum_ ( x < x | x ) x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
\sum_ ( x <- x ) x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
\sum_ ( x <- x | x ) x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
\sum_ ( x <= x < x ) x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
\sum_ ( x <= x < x | x ) x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
\sum_ ( x <= x <oo ) x [not, in mathcomp.analysis.sequences] (in ereal_scope)
\sum_ ( x <= x <oo | x ) x [not, in mathcomp.analysis.sequences] (in ereal_scope)
\sum_ ( x <oo ) x [not, in mathcomp.analysis.sequences] (in ereal_scope)
\sum_ ( x <oo | x ) x [not, in mathcomp.analysis.sequences] (in ereal_scope)
\sum_ ( x \in x ) x [not, in mathcomp.analysis.ereal] (in ereal_scope)
\sum_ ( x in x ) x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
\sum_ ( x in x | x ) x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
\sum_ ( x | x ) x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
\sum_ x x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
`| x | [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x %:nng [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x %:nng [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x %:pos [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x %:pos [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x * x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x *+ x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x *? x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x *^-1? x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x + x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x + x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x + x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x +? x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x - x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x - x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x - x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x / x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x < x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x < x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x < x :> x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x < x < x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x < x < x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x < x <= x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x < x <= x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x <= x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x <= x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x <= x :> x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x <= x < x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x <= x < x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x <= x <= x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x <= x <= x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x > x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x >= x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x \* x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x \+ x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x \+ x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x \+ x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x \- x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x \- x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x \- x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x \; x [not, in mathcomp.analysis.kernel] (in ereal_scope)
x \x x [not, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_fubini] (in ereal_scope)
x \x^ x [not, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_fubini] (in ereal_scope)
x ^* [not, in mathcomp.analysis.hoelder] (in ereal_scope)
x ^+ x [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x ^-1 [not, in mathcomp.reals.constructive_ereal] (in ereal_scope)
x ^\+ [not, in mathcomp.analysis.numfun] (in ereal_scope)
x ^\- [not, in mathcomp.analysis.numfun] (in ereal_scope)
x `^ x [not, in mathcomp.analysis.exp] (in ereal_scope)
x `^? ( x +? x ) [not, in mathcomp.analysis.exp] (in ereal_scope)

fin_quant_scope

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

fmap_scope

[ fmap of x -> x ] [not, in mathcomp.finmap.finmap] (in fmap_scope)
[fmap] [not, in mathcomp.finmap.finmap] (in fmap_scope)
x .[& x ] [not, in mathcomp.finmap.finmap] (in fmap_scope)
x .[& x ] [not, in mathcomp.finmap.finmap] (in fmap_scope)
x .[ x <- x ] [not, in mathcomp.finmap.finmap] (in fmap_scope)
x .[ x ] [not, in mathcomp.finmap.finmap] (in fmap_scope)
x .[? x ] [not, in mathcomp.finmap.finmap] (in fmap_scope)
x .[\ x ] [not, in mathcomp.finmap.finmap] (in fmap_scope)
x .[\ x ] [not, in mathcomp.finmap.finmap] (in fmap_scope)
x .[~ x ] [not, in mathcomp.finmap.finmap] (in fmap_scope)
x .[~ x ] [not, in mathcomp.finmap.finmap] (in fmap_scope)

form_scope

$| x | [not, in mathcomp.classical.classical_sets] (in form_scope)
'bijTT_ x [not, in mathcomp.classical.functions] (in form_scope)
'bij_ x [not, in mathcomp.classical.functions] (in form_scope)
'funK_ x [not, in mathcomp.classical.functions] (in form_scope)
'funS_ x [not, in mathcomp.classical.functions] (in form_scope)
'funoK_ x [not, in mathcomp.classical.functions] (in form_scope)
'funpPinj_ x [not, in mathcomp.classical.functions] (in form_scope)
'inj_ x [not, in mathcomp.classical.functions] (in form_scope)
'injpPfun_ x [not, in mathcomp.classical.functions] (in form_scope)
'invK_ x [not, in mathcomp.classical.functions] (in form_scope)
'invS_ x [not, in mathcomp.classical.functions] (in form_scope)
'mem_fun_ x [not, in mathcomp.classical.functions] (in form_scope)
'oinvK_ x [not, in mathcomp.classical.functions] (in form_scope)
'oinvP_ x [not, in mathcomp.classical.functions] (in form_scope)
'oinvS_ x [not, in mathcomp.classical.functions] (in form_scope)
'oinvT_ x [not, in mathcomp.classical.functions] (in form_scope)
'pPbij_ x [not, in mathcomp.classical.functions] (in form_scope)
'pPinj_ x [not, in mathcomp.classical.functions] (in form_scope)
'pinv_ x [not, in mathcomp.classical.functions] (in form_scope)
'split_ x [not, in mathcomp.classical.functions] (in form_scope)
'surj_ x [not, in mathcomp.classical.functions] (in form_scope)
'totalfun_ x [not, in mathcomp.classical.functions] (in form_scope)
'valL_ x [not, in mathcomp.classical.functions] (in form_scope)
'valLfun_ x [not, in mathcomp.classical.functions] (in form_scope)
[ <-> x ; x ; .. ; x ] [not, in mathcomp.boot.seq] (in form_scope)
[ Choice of x by <:%/ ] [not, in mathcomp.boot.generic_quotient] (in form_scope)
[ Choice of x by <: ] [not, in mathcomp.boot.choice] (in form_scope)
[ Countable of x by <:%/ ] [not, in mathcomp.boot.generic_quotient] (in form_scope)
[ Countable of x by <: ] [not, in mathcomp.boot.choice] (in form_scope)
[ Equality of x by <:%/ ] [not, in mathcomp.boot.generic_quotient] (in form_scope)
[ Equality of x by <: ] [not, in mathcomp.boot.eqtype] (in form_scope)
[ Finite of x by <:%/ ] [not, in mathcomp.boot.generic_quotient] (in form_scope)
[ Finite of x by <: ] [not, in mathcomp.boot.fintype] (in form_scope)
[ Order of x by <: ] [not, in mathcomp.order.order] (in form_scope)
[ POrder of x by <: ] [not, in mathcomp.order.order] (in form_scope)
[ Sub x by %/ ] [not, in mathcomp.boot.generic_quotient] (in form_scope)
[ Sub x of x by %/ ] [not, in mathcomp.boot.generic_quotient] (in form_scope)
[ SubChoice_isBSubLattice of x by <: ] [not, in mathcomp.order.order] (in form_scope)
[ SubChoice_isBSubLattice of x by <: with x ] [not, in mathcomp.order.order] (in form_scope)
[ SubChoice_isSubAlgebra of x by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.ssralg] (in form_scope)
[ SubChoice_isSubComNzRing of x by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in form_scope)
[ SubChoice_isSubComNzSemiRing of x by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in form_scope)
[ SubChoice_isSubComPzRing of x by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in form_scope)
[ SubChoice_isSubComPzSemiRing of x by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in form_scope)
[ SubChoice_isSubComRing of x by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.ssralg] (in form_scope)
[ SubChoice_isSubComSemiRing of x by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.ssralg] (in form_scope)
[ SubChoice_isSubComUnitRing of x by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.divalg] (in form_scope)
[ SubChoice_isSubIntegralDomain of x by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.divalg] (in form_scope)
[ SubChoice_isSubLSemiAlgebra of x by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.ssralg] (in form_scope)
[ SubChoice_isSubLSemiModule of x by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in form_scope)
[ SubChoice_isSubLalgebra of x by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.ssralg] (in form_scope)
[ SubChoice_isSubLattice of x by <: ] [not, in mathcomp.order.order] (in form_scope)
[ SubChoice_isSubLattice of x by <: with x ] [not, in mathcomp.order.order] (in form_scope)
[ SubChoice_isSubLmodule of x by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in form_scope)
[ SubChoice_isSubNmodule of x by <: ] [not, in mathcomp.boot.nmodule] (in form_scope)
[ SubChoice_isSubNzAlgebra of x by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in form_scope)
[ SubChoice_isSubNzLSemiAlgebra of x by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in form_scope)
[ SubChoice_isSubNzLalgebra of x by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in form_scope)
[ SubChoice_isSubNzRing of x by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in form_scope)
[ SubChoice_isSubNzSemiAlgebra of x by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in form_scope)
[ SubChoice_isSubNzSemiRing of x by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in form_scope)
[ SubChoice_isSubOrder of x by <: ] [not, in mathcomp.order.order] (in form_scope)
[ SubChoice_isSubOrder of x by <: with x ] [not, in mathcomp.order.order] (in form_scope)
[ SubChoice_isSubPOrder of x by <: ] [not, in mathcomp.order.order] (in form_scope)
[ SubChoice_isSubPOrder of x by <: with x ] [not, in mathcomp.order.order] (in form_scope)
[ SubChoice_isSubPreorder of x by <: ] [not, in mathcomp.order.preorder] (in form_scope)
[ SubChoice_isSubPreorder of x by <: with x ] [not, in mathcomp.order.preorder] (in form_scope)
[ SubChoice_isSubPzAlgebra of x by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in form_scope)
[ SubChoice_isSubPzLSemiAlgebra of x by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in form_scope)
[ SubChoice_isSubPzLalgebra of x by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in form_scope)
[ SubChoice_isSubPzRing of x by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in form_scope)
[ SubChoice_isSubPzSemiAlgebra of x by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in form_scope)
[ SubChoice_isSubPzSemiRing of x by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in form_scope)
[ SubChoice_isSubRing of x by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.ssralg] (in form_scope)
[ SubChoice_isSubSemiAlgebra of x by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.ssralg] (in form_scope)
[ SubChoice_isSubSemiRing of x by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.ssralg] (in form_scope)
[ SubChoice_isSubUnitRing of x by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.divalg] (in form_scope)
[ SubChoice_isSubZmodule of x by <: ] [not, in mathcomp.boot.nmodule] (in form_scope)
[ SubChoice_isTBSubLattice of x by <: ] [not, in mathcomp.order.order] (in form_scope)
[ SubChoice_isTBSubLattice of x by <: with x ] [not, in mathcomp.order.order] (in form_scope)
[ SubChoice_isTSubLattice of x by <: ] [not, in mathcomp.order.order] (in form_scope)
[ SubChoice_isTSubLattice of x by <: with x ] [not, in mathcomp.order.order] (in form_scope)
[ SubComUnitRing_isSubIntegralDomain of x by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.divalg] (in form_scope)
[ SubIntegralDomain_isSubField of x by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.divalg] (in form_scope)
[ SubLSemiAlgebra_isSubSemiAlgebra of x by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in form_scope)
[ SubLalgebra_isSubAlgebra of x by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.ssralg] (in form_scope)
[ SubLattice_isSubOrder of x by <: ] [not, in mathcomp.order.order] (in form_scope)
[ SubLattice_isSubOrder of x by <: with x ] [not, in mathcomp.order.order] (in form_scope)
[ SubNmodule_isSubLSemiModule of x by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in form_scope)
[ SubNmodule_isSubNzSemiRing of x by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in form_scope)
[ SubNmodule_isSubPzSemiRing of x by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in form_scope)
[ SubNmodule_isSubSemiRing of x by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.ssralg] (in form_scope)
[ SubNmodule_isSubZmodule of x by <: ] [not, in mathcomp.boot.nmodule] (in form_scope)
[ SubNzRing_SubLmodule_isSubLalgebra of x by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.ssralg] (in form_scope)
[ SubNzRing_isSubComNzRing of x by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.ssralg] (in form_scope)
[ SubNzRing_isSubUnitRing of x by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.divalg] (in form_scope)
[ SubNzSemiRing_SubLSemiModule_isSubLSemiAlgebra of x by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.ssralg] (in form_scope)
[ SubNzSemiRing_isSubComNzSemiRing of x by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.ssralg] (in form_scope)
[ SubPOrder_isBSubLattice of x by <: ] [not, in mathcomp.order.order] (in form_scope)
[ SubPOrder_isBSubLattice of x by <: with x ] [not, in mathcomp.order.order] (in form_scope)
[ SubPOrder_isSubLattice of x by <: ] [not, in mathcomp.order.order] (in form_scope)
[ SubPOrder_isSubLattice of x by <: with x ] [not, in mathcomp.order.order] (in form_scope)
[ SubPOrder_isSubOrder of x by <: ] [not, in mathcomp.order.order] (in form_scope)
[ SubPOrder_isSubOrder of x by <: with x ] [not, in mathcomp.order.order] (in form_scope)
[ SubPOrder_isTBSubLattice of x by <: ] [not, in mathcomp.order.order] (in form_scope)
[ SubPOrder_isTBSubLattice of x by <: with x ] [not, in mathcomp.order.order] (in form_scope)
[ SubPOrder_isTSubLattice of x by <: ] [not, in mathcomp.order.order] (in form_scope)
[ SubPOrder_isTSubLattice of x by <: with x ] [not, in mathcomp.order.order] (in form_scope)
[ SubPzRing_isSubComPzRing of x by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.ssralg] (in form_scope)
[ SubPzSemiRing_isSubComPzSemiRing of x by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.ssralg] (in form_scope)
[ SubRing_SubLmodule_isSubLalgebra of x by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in form_scope)
[ SubRing_isSubComRing of x by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.ssralg] (in form_scope)
[ SubRing_isSubUnitRing of x by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.ssralg] (in form_scope)
[ SubSemiRing_SubLSemiModule_isSubLSemiAlgebra of x by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in form_scope)
[ SubSemiRing_isSubComSemiRing of x by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in form_scope)
[ SubZmodule_isSubLmodule of x by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.ssralg] (in form_scope)
[ SubZmodule_isSubNzRing of x by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.ssralg] (in form_scope)
[ SubZmodule_isSubRing of x by <: ] [not, in mathcomp.algebra.algebraic_hierarchy.ssralg] (in form_scope)
[ action of x ] [not, in mathcomp.finite_group.action] (in form_scope)
[ acts x , on x | x ] [not, in mathcomp.finite_group.action] (in form_scope)
[ aspace of x ] [not, in mathcomp.field.falgebra] (in form_scope)
[ aspace of x for x ] [not, in mathcomp.field.falgebra] (in form_scope)
[ bij of x ] [not, in mathcomp.classical.functions] (in form_scope)
[ bseq ] [not, in mathcomp.boot.tuple] (in form_scope)
[ bseq of x ] [not, in mathcomp.boot.tuple] (in form_scope)
[ bseq x ; .. ; x ] [not, in mathcomp.boot.tuple] (in form_scope)
[ equiv_rel of x ] [not, in mathcomp.boot.generic_quotient] (in form_scope)
[ faithful x , on x | x ] [not, in mathcomp.finite_group.action] (in form_scope)
[ fimfun of x ] [not, in mathcomp.classical.cardinality] (in form_scope)
[ finGroupMixin of x for +%R ] [not, in mathcomp.algebra.finalg] (in form_scope)
[ finpredType of x ] [not, in mathcomp.finmap.finmap] (in form_scope)
[ fun of x ] [not, in mathcomp.classical.functions] (in form_scope)
[ gFun by x ] [not, in mathcomp.solvable.gfunctor] (in form_scope)
[ gFun of x ] [not, in mathcomp.solvable.gfunctor] (in form_scope)
[ get x : x | x ] [not, in mathcomp.classical.classical_sets] (in form_scope)
[ get x | x ] [not, in mathcomp.classical.classical_sets] (in form_scope)
[ get x | x ] [not, in mathcomp.classical.classical_sets] (in form_scope)
[ group of x ] [not, in mathcomp.finite_group.fingroup] (in form_scope)
[ groupAction of x ] [not, in mathcomp.finite_group.action] (in form_scope)
[ igFun by x & ! x ] [not, in mathcomp.solvable.gfunctor] (in form_scope)
[ igFun by x & x ] [not, in mathcomp.solvable.gfunctor] (in form_scope)
[ igFun of x ] [not, in mathcomp.solvable.gfunctor] (in form_scope)
[ inj of x ] [not, in mathcomp.classical.functions] (in form_scope)
[ injfun of x ] [not, in mathcomp.classical.functions] (in form_scope)
[ inv of x ] [not, in mathcomp.classical.functions] (in form_scope)
[ invfun of x ] [not, in mathcomp.classical.functions] (in form_scope)
[ isNew for x ] [not, in mathcomp.boot.eqtype] (in form_scope)
[ isNew for x ] [not, in mathcomp.boot.eqtype] (in form_scope)
[ isNew of x for x ] [not, in mathcomp.boot.eqtype] (in form_scope)
[ isSub for x ] [not, in mathcomp.boot.eqtype] (in form_scope)
[ isSub for x ] [not, in mathcomp.boot.eqtype] (in form_scope)
[ isSub for x by x ] [not, in mathcomp.boot.eqtype] (in form_scope)
[ isSub of x for x ] [not, in mathcomp.boot.eqtype] (in form_scope)
[ jlmorphism of x ] [not, in mathcomp.order.order] (in form_scope)
[ jlmorphism of x as x ] [not, in mathcomp.order.order] (in form_scope)
[ lmorphism of x ] [not, in mathcomp.order.order] (in form_scope)
[ lmorphism of x as x ] [not, in mathcomp.order.order] (in form_scope)
[ mfun of x ] [not, in mathcomp.analysis.measure_theory.measurable_function] (in form_scope)
[ mgFun by x ] [not, in mathcomp.solvable.gfunctor] (in form_scope)
[ mgFun of x ] [not, in mathcomp.solvable.gfunctor] (in form_scope)
[ mlmorphism of x ] [not, in mathcomp.order.order] (in form_scope)
[ mlmorphism of x as x ] [not, in mathcomp.order.order] (in form_scope)
[ morphism of x ] [not, in mathcomp.finite_group.morphism] (in form_scope)
[ morphism x of x ] [not, in mathcomp.finite_group.morphism] (in form_scope)
[ nnfun of x ] [not, in mathcomp.analysis.numfun] (in form_scope)
[ nnsfun of x ] [not, in mathcomp.analysis.lebesgue_integral_theory.simple_functions] (in form_scope)
[ oinv of x ] [not, in mathcomp.classical.functions] (in form_scope)
[ oinvfun of x ] [not, in mathcomp.classical.functions] (in form_scope)
[ pgFun by x ] [not, in mathcomp.solvable.gfunctor] (in form_scope)
[ pgFun of x ] [not, in mathcomp.solvable.gfunctor] (in form_scope)
[ pick x : x ] [not, in mathcomp.boot.fintype] (in form_scope)
[ pick x : x ] [not, in mathcomp.boot.fintype] (in form_scope)
[ pick x : x in x ] [not, in mathcomp.boot.fintype] (in form_scope)
[ pick x : x in x | x & x ] [not, in mathcomp.boot.fintype] (in form_scope)
[ pick x : x in x | x ] [not, in mathcomp.boot.fintype] (in form_scope)
[ pick x : x | x & x ] [not, in mathcomp.boot.fintype] (in form_scope)
[ pick x : x | x ] [not, in mathcomp.boot.fintype] (in form_scope)
[ pick x ] [not, in mathcomp.boot.fintype] (in form_scope)
[ pick x in x ] [not, in mathcomp.boot.fintype] (in form_scope)
[ pick x in x | x & x ] [not, in mathcomp.boot.fintype] (in form_scope)
[ pick x in x | x ] [not, in mathcomp.boot.fintype] (in form_scope)
[ pick x | x & x ] [not, in mathcomp.boot.fintype] (in form_scope)
[ pick x | x ] [not, in mathcomp.boot.fintype] (in form_scope)
[ primitive x , on x | x ] [not, in mathcomp.solvable.primitive_action] (in form_scope)
[ sfun of x ] [not, in mathcomp.analysis.lebesgue_integral_theory.simple_functions] (in form_scope)
[ splitbij of x ] [not, in mathcomp.classical.functions] (in form_scope)
[ splitinj of x ] [not, in mathcomp.classical.functions] (in form_scope)
[ splitinjfun of x ] [not, in mathcomp.classical.functions] (in form_scope)
[ splitsurj of x ] [not, in mathcomp.classical.functions] (in form_scope)
[ splitsurjfun of x ] [not, in mathcomp.classical.functions] (in form_scope)
[ surj of x ] [not, in mathcomp.classical.functions] (in form_scope)
[ surjfun of x ] [not, in mathcomp.classical.functions] (in form_scope)
[ tnth x x ] [not, in mathcomp.boot.tuple] (in form_scope)
[ transitive ^ x x , on x | x ] [not, in mathcomp.solvable.primitive_action] (in form_scope)
[ transitive x , on x | x ] [not, in mathcomp.finite_group.action] (in form_scope)
[ tuple ] [not, in mathcomp.boot.tuple] (in form_scope)
[ tuple of x ] [not, in mathcomp.boot.tuple] (in form_scope)
[ tuple x ; .. ; x ] [not, in mathcomp.boot.tuple] (in form_scope)
[ tuple x | x < x ] [not, in mathcomp.boot.tuple] (in form_scope)
{ RV x >-> x } [not, in mathcomp.analysis.probability_theory.random_variable] (in form_scope)
{ dRV x >-> x } [not, in mathcomp.analysis.probability_theory.random_variable] (in form_scope)
{ dmfun x >-> x } [not, in mathcomp.analysis.probability_theory.random_variable] (in form_scope)
{ fimfun x >-> x } [not, in mathcomp.classical.cardinality] (in form_scope)
{ fun x >-> x } [not, in mathcomp.classical.functions] (in form_scope)
{ mfun x >-> x } [not, in mathcomp.analysis.measure_theory.measurable_function] (in form_scope)
{ mfun_ x , x >-> x } [not, in mathcomp.analysis.hoelder] (in form_scope)
{ nnfun x >-> x } [not, in mathcomp.analysis.numfun] (in form_scope)
{ nnsfun x >-> x } [not, in mathcomp.analysis.lebesgue_integral_theory.simple_functions] (in form_scope)
{ sfun x >-> x } [not, in mathcomp.analysis.lebesgue_integral_theory.simple_functions] (in form_scope)

fperm_scope

1 [not, in mathcomp.finmap.finperm] (in fperm_scope)
x * x [not, in mathcomp.finmap.finperm] (in fperm_scope)
x ^+ x [not, in mathcomp.finmap.finperm] (in fperm_scope)
x ^-1 [not, in mathcomp.finmap.finperm] (in fperm_scope)

fset_scope

[ disjoint x & x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ f set x : x | x & x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ f set x : x | x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ f set x in x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ f set x in x | x & x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ f set x in x | x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ f set x | x : x & x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ f set x | x : x , x : x & x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ f set x | x : x , x : x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ f set x | x : x , x in x & x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ f set x | x : x , x in x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ f set x | x : x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ f set x | x in x & x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ f set x | x in x , x : x & x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ f set x | x in x , x : x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ f set x | x in x , x in x & x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ f set x | x in x , x in x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ f set x | x in x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ f setval x : x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ f setval x : x | x & x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ f setval x : x | x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ f setval x in x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ f setval x in x | x & x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ f setval x in x | x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ fset x : x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ fset x : x in x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ fset x : x in x | x & x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ fset x : x in x | x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ fset x : x | x & x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ fset x : x | x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ fset x ; x ; .. ; x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ fset x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ fset x in x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ fset x in x | x & x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ fset x in x | x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ fset x | x : x & x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ fset x | x : x , x : x & x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ fset x | x : x , x : x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ fset x | x : x , x in x & x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ fset x | x : x , x in x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ fset x | x : x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ fset x | x : x in x , x : x in x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ fset x | x : x in x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ fset x | x in x & x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ fset x | x in x , x : x & x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ fset x | x in x , x : x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ fset x | x in x , x in x & x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ fset x | x in x , x in x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ fset x | x in x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ fset[ x ] x : x in x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ fset[ x ] x : x in x | x & x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ fset[ x ] x : x in x | x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ fset[ x ] x : x | x & x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ fset[ x ] x : x | x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ fset[ x ] x in x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ fset[ x ] x in x | x & x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ fset[ x ] x in x | x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ fset[ x ] x | x : x & x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ fset[ x ] x | x : x , x : x & x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ fset[ x ] x | x : x , x : x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ fset[ x ] x | x : x , x : x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ fset[ x ] x | x : x , x in x & x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ fset[ x ] x | x : x , x in x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ fset[ x ] x | x : x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ fset[ x ] x | x : x in x , x : x in x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ fset[ x ] x | x : x in x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ fset[ x ] x | x in x & x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ fset[ x ] x | x in x , x : x & x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ fset[ x ] x | x in x , x : x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ fset[ x ] x | x in x , x in x & x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ fset[ x ] x | x in x , x in x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ fset[ x ] x | x in x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ fsetval x : x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ fsetval x : x | x & x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ fsetval x : x | x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ fsetval x in x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ fsetval x in x | x & x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ fsetval x in x | x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ fsetval[ x ] x : x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ fsetval[ x ] x : x | x & x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ fsetval[ x ] x : x | x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ fsetval[ x ] x in x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ fsetval[ x ] x in x | x & x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[ fsetval[ x ] x in x | x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
[` x ] [not, in mathcomp.finmap.finmap] (in fset_scope)
\bigcup_ ( x <- x ) x [not, in mathcomp.finmap.finmap] (in fset_scope)
\bigcup_ ( x <- x | x ) x [not, in mathcomp.finmap.finmap] (in fset_scope)
\bigcup_ ( x in x ) x [not, in mathcomp.finmap.finmap] (in fset_scope)
\bigcup_ ( x in x | x ) x [not, in mathcomp.finmap.finmap] (in fset_scope)
\bigcup_ ( x | x ) x [not, in mathcomp.finmap.finmap] (in fset_scope)
x + x [not, in mathcomp.finmap.finmap] (in fset_scope)
x + x [not, in mathcomp.finmap.finmap] (in fset_scope)
x .`1 [not, in mathcomp.classical.cardinality] (in fset_scope)
x .`2 [not, in mathcomp.classical.cardinality] (in fset_scope)
x @2` ( x , x ) [not, in mathcomp.finmap.finmap] (in fset_scope)
x @2`[ x ] ( x , x ) [not, in mathcomp.finmap.finmap] (in fset_scope)
x @` x [not, in mathcomp.finmap.finmap] (in fset_scope)
x @`[ x ] x [not, in mathcomp.finmap.finmap] (in fset_scope)
x `!=` x [not, in mathcomp.finmap.finmap] (in fset_scope)
x `&` x [not, in mathcomp.finmap.finmap] (in fset_scope)
x `*` x [not, in mathcomp.finmap.finmap] (in fset_scope)
x `<=` x [not, in mathcomp.finmap.finmap] (in fset_scope)
x `<>` x [not, in mathcomp.finmap.finmap] (in fset_scope)
x `<` x [not, in mathcomp.finmap.finmap] (in fset_scope)
x `==` x [not, in mathcomp.finmap.finmap] (in fset_scope)
x `=P` x [not, in mathcomp.finmap.finmap] (in fset_scope)
x `=` x [not, in mathcomp.finmap.finmap] (in fset_scope)
x `\ x [not, in mathcomp.finmap.finmap] (in fset_scope)
x `\` x [not, in mathcomp.finmap.finmap] (in fset_scope)
x `|` x [not, in mathcomp.finmap.finmap] (in fset_scope)
x |` x [not, in mathcomp.finmap.finmap] (in fset_scope)

fsfun_scope

x \o x [not, in mathcomp.finmap.finmap] (in fsfun_scope)

fun_delta_scope

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

fun_scope

x ^-1 [not, in mathcomp.classical.functions] (in fun_scope)
x ^-1 [not, in mathcomp.classical.functions] (in fun_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)
<?<=%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)
<?=%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)
<^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 x [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in function_scope)
@ dvd x [not, in mathcomp.order.preorder] (in function_scope)
@ gcd x [not, in mathcomp.order.order] (in function_scope)
@ ger x [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in function_scope)
@ gtr x [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in function_scope)
@ lcm x [not, in mathcomp.order.order] (in function_scope)
@ ler x [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in function_scope)
@ lerif x [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in function_scope)
@ lteif x [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in function_scope)
@ ltr x [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in function_scope)
@ maxe x [not, in mathcomp.reals.constructive_ereal] (in function_scope)
@ maxr x [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in function_scope)
@ mine x [not, in mathcomp.reals.constructive_ereal] (in function_scope)
@ minr x [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in function_scope)
@ sdvd x [not, in mathcomp.order.preorder] (in function_scope)
[ eta x with x , .. , x ] [not, in mathcomp.boot.eqtype] (in function_scope)
[ ffun => x ] [not, in mathcomp.boot.finfun] (in function_scope)
[ ffun x : x => x ] [not, in mathcomp.boot.finfun] (in function_scope)
[ ffun x => x ] [not, in mathcomp.boot.finfun] (in function_scope)
[ fmap : x => x ] [not, in mathcomp.finmap.finmap] (in function_scope)
[ fmap => x ] [not, in mathcomp.finmap.finmap] (in function_scope)
[ fmap x : x => x ] [not, in mathcomp.finmap.finmap] (in function_scope)
[ fmap x => x ] [not, in mathcomp.finmap.finmap] (in function_scope)
[ fprod : x => x ] [not, in mathcomp.boot.finfun] (in function_scope)
[ fprod => x ] [not, in mathcomp.boot.finfun] (in function_scope)
[ fprod x : x => x ] [not, in mathcomp.boot.finfun] (in function_scope)
[ fprod x => x ] [not, in mathcomp.boot.finfun] (in function_scope)
[ fs fun x : x => x ] [not, in mathcomp.finmap.finmap] (in function_scope)
[ fs fun x in x => x ] [not, in mathcomp.finmap.finmap] (in function_scope)
[ fsfun ] [not, in mathcomp.finmap.finmap] (in function_scope)
[ fsfun for x ] [not, in mathcomp.finmap.finmap] (in function_scope)
[ fsfun in x => x ] [not, in mathcomp.finmap.finmap] (in function_scope)
[ fsfun in x => x | x ] [not, in mathcomp.finmap.finmap] (in function_scope)
[ fsfun of x => x ] [not, in mathcomp.finmap.finmap] (in function_scope)
[ fsfun with x ] [not, in mathcomp.finmap.finmap] (in function_scope)
[ fsfun x : x => x ] [not, in mathcomp.finmap.finmap] (in function_scope)
[ fsfun x : x => x | x ] [not, in mathcomp.finmap.finmap] (in function_scope)
[ fsfun x => x ] [not, in mathcomp.finmap.finmap] (in function_scope)
[ fsfun x => x | x ] [not, in mathcomp.finmap.finmap] (in function_scope)
[ fsfun x in x => x ] [not, in mathcomp.finmap.finmap] (in function_scope)
[ fsfun x in x => x | x ] [not, in mathcomp.finmap.finmap] (in function_scope)
[ fsfun x with x , .. , x ] [not, in mathcomp.finmap.finmap] (in function_scope)
[ fsfun x without x , .. , x ] [not, in mathcomp.finmap.finmap] (in function_scope)
[ fsfun=> x ] [not, in mathcomp.finmap.finmap] (in function_scope)
[ fsfun=> x | x ] [not, in mathcomp.finmap.finmap] (in function_scope)
[ fsfun[ x ] in x => x ] [not, in mathcomp.finmap.finmap] (in function_scope)
[ fsfun[ x ] in x => x | x ] [not, in mathcomp.finmap.finmap] (in function_scope)
[ fsfun[ x ] x : x => x ] [not, in mathcomp.finmap.finmap] (in function_scope)
[ fsfun[ x ] x : x => x | x ] [not, in mathcomp.finmap.finmap] (in function_scope)
[ fsfun[ x ] x => x ] [not, in mathcomp.finmap.finmap] (in function_scope)
[ fsfun[ x ] x => x | x ] [not, in mathcomp.finmap.finmap] (in function_scope)
[ fsfun[ x ] x in x => x ] [not, in mathcomp.finmap.finmap] (in function_scope)
[ fsfun[ x ] x in x => x | x ] [not, in mathcomp.finmap.finmap] (in function_scope)
[ fsfun[ x ]=> x ] [not, in mathcomp.finmap.finmap] (in function_scope)
[ fsfun[ x ]=> x | x ] [not, in mathcomp.finmap.finmap] (in function_scope)
[ fun x : x => x with x , .. , x ] [not, in mathcomp.boot.eqtype] (in function_scope)
[ fun x => x with x , .. , x ] [not, in mathcomp.boot.eqtype] (in function_scope)
[ fun x in x ] [not, in mathcomp.classical.functions] (in function_scope)
[ predD1 x & x ] [not, in mathcomp.boot.eqtype] (in function_scope)
[ predU1 x & x ] [not, in mathcomp.boot.eqtype] (in function_scope)
[ predX x & x ] [not, in mathcomp.boot.eqtype] (in function_scope)
\- x [not, in mathcomp.boot.nmodule] (in function_scope)
\- x [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)
x .-support [not, in mathcomp.boot.finfun] (in function_scope)
x \* x [not, in mathcomp.boot.monoid] (in function_scope)
x \* x [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in function_scope)
x \*: x [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in function_scope)
x \*o x [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in function_scope)
x \+ x [not, in mathcomp.boot.nmodule] (in function_scope)
x \+ x [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in function_scope)
x \- x [not, in mathcomp.boot.nmodule] (in function_scope)
x \- x [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in function_scope)
x \_ x [not, in mathcomp.classical.functions] (in function_scope)
x \max x [not, in mathcomp.order.preorder] (in function_scope)
x \min x [not, in mathcomp.order.preorder] (in function_scope)
x \o* x [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in function_scope)
x ^* [not, in mathcomp.finite_group.action] (in function_scope)
x ^-1 [not, in mathcomp.classical.functions] (in function_scope)
x ^-1 [not, in mathcomp.classical.functions] (in function_scope)

gFun_scope

x %% x [not, in mathcomp.solvable.gfunctor] (in gFun_scope)
x \o x [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)
'Q [not, in mathcomp.finite_group.action] (in groupAction_scope)
'U [not, in mathcomp.algebra.finalg] (in groupAction_scope)
<[ x ] > [not, in mathcomp.finite_group.action] (in groupAction_scope)
[ Aut x ] [not, in mathcomp.finite_group.action] (in groupAction_scope)
x %% x [not, in mathcomp.finite_group.action] (in groupAction_scope)
x / x [not, in mathcomp.finite_group.action] (in groupAction_scope)
x \ x [not, in mathcomp.finite_group.action] (in groupAction_scope)
x \o x [not, in mathcomp.finite_group.action] (in groupAction_scope)

group_rel_scope

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

group_scope

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

lfun_scope

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

lrfun_scope

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

matrix_set_scope

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

measure_display_scope

x .-cara [not, in mathcomp.analysis.measure_theory.measure_extension] (in measure_display_scope)
x .-ocitv [not, in mathcomp.analysis.lebesgue_stieltjes_measure] (in measure_display_scope)
x .-preimage [not, in mathcomp.analysis.measure_theory.measurable_structure] (in measure_display_scope)
x .-prod [not, in mathcomp.analysis.measure_theory.measurable_structure] (in measure_display_scope)
x .-ring [not, in mathcomp.analysis.measure_theory.measure_function] (in measure_display_scope)
x .-sigma [not, in mathcomp.analysis.measure_theory.measurable_structure] (in measure_display_scope)

measure_scope

x ^* [not, in mathcomp.analysis.measure_theory.measure_extension] (in measure_scope)

mset_scope

[ m set x in x => x ] [not, in mathcomp.finmap.multiset] (in mset_scope)
[ mset x : x ] [not, in mathcomp.finmap.multiset] (in mset_scope)
[ mset x ; x ; .. ; x ] [not, in mathcomp.finmap.multiset] (in mset_scope)
[ mset x ] [not, in mathcomp.finmap.multiset] (in mset_scope)
[ mset x in x => x ] [not, in mathcomp.finmap.multiset] (in mset_scope)
[ mset[ x ] x in x => x ] [not, in mathcomp.finmap.multiset] (in mset_scope)
{mset x } [not, in mathcomp.finmap.multiset] (in mset_scope)
x +` x [not, in mathcomp.finmap.multiset] (in mset_scope)
x `&` x [not, in mathcomp.finmap.multiset] (in mset_scope)
x `*` x [not, in mathcomp.finmap.multiset] (in mset_scope)
x `+` x [not, in mathcomp.finmap.multiset] (in mset_scope)
x `<=` x [not, in mathcomp.finmap.multiset] (in mset_scope)
x `<` x [not, in mathcomp.finmap.multiset] (in mset_scope)
x `\ x [not, in mathcomp.finmap.multiset] (in mset_scope)
x `\` x [not, in mathcomp.finmap.multiset] (in mset_scope)
x `|` x [not, in mathcomp.finmap.multiset] (in mset_scope)
x |` x [not, in mathcomp.finmap.multiset] (in mset_scope)

nat_scope

#| x | [not, in mathcomp.boot.fintype] (in nat_scope)
#|` x | [not, in mathcomp.finmap.finmap] (in nat_scope)
'C ( x , x ) [not, in mathcomp.boot.binomial] (in nat_scope)
[ Num of x ] [not, in mathcomp.boot.ssrnat] (in nat_scope)
[ arg max_ ( x > x ) x ] [not, in mathcomp.boot.fintype] (in nat_scope)
[ arg max_ ( x > x in x ) x ] [not, in mathcomp.boot.fintype] (in nat_scope)
[ arg max_ ( x > x | x ) x ] [not, in mathcomp.boot.fintype] (in nat_scope)
[ arg min_ ( x < x ) x ] [not, in mathcomp.boot.fintype] (in nat_scope)
[ arg min_ ( x < x in x ) x ] [not, in mathcomp.boot.fintype] (in nat_scope)
[ arg min_ ( x < x | x ) x ] [not, in mathcomp.boot.fintype] (in nat_scope)
[ arg[ x ]_( x < x ) x ] [not, in mathcomp.boot.fintype] (in nat_scope)
[ arg[ x ]_( x < x in x ) x ] [not, in mathcomp.boot.fintype] (in nat_scope)
[ arg[ x ]_( x < x | x ) x ] [not, in mathcomp.boot.fintype] (in nat_scope)
\dim x [not, in mathcomp.algebra.vector] (in nat_scope)
\dim_ x x [not, in mathcomp.field.falgebra] (in nat_scope)
\max_ ( x : x ) x [not, in mathcomp.boot.bigop] (in nat_scope)
\max_ ( x : x | x ) x [not, in mathcomp.boot.bigop] (in nat_scope)
\max_ ( x < x ) x [not, in mathcomp.boot.bigop] (in nat_scope)
\max_ ( x < x | x ) x [not, in mathcomp.boot.bigop] (in nat_scope)
\max_ ( x <- x ) x [not, in mathcomp.boot.bigop] (in nat_scope)
\max_ ( x <- x | x ) x [not, in mathcomp.boot.bigop] (in nat_scope)
\max_ ( x <= x < x ) x [not, in mathcomp.boot.bigop] (in nat_scope)
\max_ ( x <= x < x | x ) x [not, in mathcomp.boot.bigop] (in nat_scope)
\max_ ( x in x ) x [not, in mathcomp.boot.bigop] (in nat_scope)
\max_ ( x in x | x ) x [not, in mathcomp.boot.bigop] (in nat_scope)
\max_ ( x | x ) x [not, in mathcomp.boot.bigop] (in nat_scope)
\max_ x x [not, in mathcomp.boot.bigop] (in nat_scope)
\p i ( x ) [not, in mathcomp.boot.prime] (in nat_scope)
\pi ( x ) [not, in mathcomp.boot.prime] (in nat_scope)
\prod_ ( x : x ) x [not, in mathcomp.boot.bigop] (in nat_scope)
\prod_ ( x : x | x ) x [not, in mathcomp.boot.bigop] (in nat_scope)
\prod_ ( x < x ) x [not, in mathcomp.boot.bigop] (in nat_scope)
\prod_ ( x < x | x ) x [not, in mathcomp.boot.bigop] (in nat_scope)
\prod_ ( x <- x ) x [not, in mathcomp.boot.bigop] (in nat_scope)
\prod_ ( x <- x | x ) x [not, in mathcomp.boot.bigop] (in nat_scope)
\prod_ ( x <= x < x ) x [not, in mathcomp.boot.bigop] (in nat_scope)
\prod_ ( x <= x < x | x ) x [not, in mathcomp.boot.bigop] (in nat_scope)
\prod_ ( x in x ) x [not, in mathcomp.boot.bigop] (in nat_scope)
\prod_ ( x in x | x ) x [not, in mathcomp.boot.bigop] (in nat_scope)
\prod_ ( x | x ) x [not, in mathcomp.boot.bigop] (in nat_scope)
\prod_ x x [not, in mathcomp.boot.bigop] (in nat_scope)
\rank x [not, in mathcomp.algebra.mxalgebra] (in nat_scope)
\rank x [not, in mathcomp.algebra.mxalgebra] (in nat_scope)
\sum_ ( x : x ) x [not, in mathcomp.boot.bigop] (in nat_scope)
\sum_ ( x : x | x ) x [not, in mathcomp.boot.bigop] (in nat_scope)
\sum_ ( x < x ) x [not, in mathcomp.boot.bigop] (in nat_scope)
\sum_ ( x < x | x ) x [not, in mathcomp.boot.bigop] (in nat_scope)
\sum_ ( x <- x ) x [not, in mathcomp.boot.bigop] (in nat_scope)
\sum_ ( x <- x | x ) x [not, in mathcomp.boot.bigop] (in nat_scope)
\sum_ ( x <= x < x ) x [not, in mathcomp.boot.bigop] (in nat_scope)
\sum_ ( x <= x < x | x ) x [not, in mathcomp.boot.bigop] (in nat_scope)
\sum_ ( x in x ) x [not, in mathcomp.boot.bigop] (in nat_scope)
\sum_ ( x in x | x ) x [not, in mathcomp.boot.bigop] (in nat_scope)
\sum_ ( x | x ) x [not, in mathcomp.boot.bigop] (in nat_scope)
\sum_ x x [not, in mathcomp.boot.bigop] (in nat_scope)
`| x | [not, in mathcomp.algebra.ssrint] (in nat_scope)
`| x | [not, in mathcomp.algebra.ssrint] (in nat_scope)
x != x %[mod x ] [not, in mathcomp.boot.div] (in nat_scope)
x %% x [not, in mathcomp.boot.div] (in nat_scope)
x %/ x [not, in mathcomp.boot.div] (in nat_scope)
x %| x [not, in mathcomp.boot.div] (in nat_scope)
x * x [not, in mathcomp.boot.ssrnat] (in nat_scope)
x * x [not, in mathcomp.boot.ssrnat] (in nat_scope)
x + x [not, in mathcomp.boot.ssrnat] (in nat_scope)
x + x [not, in mathcomp.boot.ssrnat] (in nat_scope)
x - x [not, in mathcomp.boot.ssrnat] (in nat_scope)
x .*2 [not, in mathcomp.boot.ssrnat] (in nat_scope)
x .*2 [not, in mathcomp.boot.ssrnat] (in nat_scope)
x .+1 [not, in mathcomp.boot.ssrnat] (in nat_scope)
x .+2 [not, in mathcomp.boot.ssrnat] (in nat_scope)
x .+3 [not, in mathcomp.boot.ssrnat] (in nat_scope)
x .+4 [not, in mathcomp.boot.ssrnat] (in nat_scope)
x .-1 [not, in mathcomp.boot.ssrnat] (in nat_scope)
x .-2 [not, in mathcomp.boot.ssrnat] (in nat_scope)
x .-nat [not, in mathcomp.boot.prime] (in nat_scope)
x ./2 [not, in mathcomp.boot.ssrnat] (in nat_scope)
x < x [not, in mathcomp.boot.ssrnat] (in nat_scope)
x < x < x [not, in mathcomp.boot.ssrnat] (in nat_scope)
x < x <= x [not, in mathcomp.boot.ssrnat] (in nat_scope)
x <= x [not, in mathcomp.boot.ssrnat] (in nat_scope)
x <= x < x [not, in mathcomp.boot.ssrnat] (in nat_scope)
x <= x <= x [not, in mathcomp.boot.ssrnat] (in nat_scope)
x <= x ?= iff x [not, in mathcomp.boot.ssrnat] (in nat_scope)
x <> x %[mod x ] [not, in mathcomp.boot.div] (in nat_scope)
x = x %[mod x ] [not, in mathcomp.boot.div] (in nat_scope)
x == x %[mod x ] [not, in mathcomp.boot.div] (in nat_scope)
x > x [not, in mathcomp.boot.ssrnat] (in nat_scope)
x >= x [not, in mathcomp.boot.ssrnat] (in nat_scope)
x ^' [not, in mathcomp.boot.prime] (in nat_scope)
x ^ x [not, in mathcomp.boot.ssrnat] (in nat_scope)
x ^ x [not, in mathcomp.boot.ssrnat] (in nat_scope)
x ^? x :: x [not, in mathcomp.boot.prime] (in nat_scope)
x ^_ x [not, in mathcomp.boot.binomial] (in nat_scope)
x `! [not, in mathcomp.boot.ssrnat] (in nat_scope)
x `_ x [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)
< x [not, in mathcomp.order.preorder] (in order_scope)
< x :> x [not, in mathcomp.order.preorder] (in order_scope)
<= x [not, in mathcomp.order.preorder] (in order_scope)
<= x :> x [not, in mathcomp.order.preorder] (in order_scope)
<=^d x [not, in mathcomp.order.preorder] (in order_scope)
<=^d x :> x [not, in mathcomp.order.preorder] (in order_scope)
<=^l x [not, in mathcomp.order.preorder] (in order_scope)
<=^l x [not, in mathcomp.order.preorder] (in order_scope)
<=^l x :> x [not, in mathcomp.order.preorder] (in order_scope)
<=^l x :> x [not, in mathcomp.order.preorder] (in order_scope)
<=^p x [not, in mathcomp.order.preorder] (in order_scope)
<=^p x :> x [not, in mathcomp.order.preorder] (in order_scope)
<=^sp x [not, in mathcomp.order.preorder] (in order_scope)
<=^sp x :> x [not, in mathcomp.order.preorder] (in order_scope)
<^d x [not, in mathcomp.order.preorder] (in order_scope)
<^d x :> x [not, in mathcomp.order.preorder] (in order_scope)
<^l x [not, in mathcomp.order.preorder] (in order_scope)
<^l x [not, in mathcomp.order.preorder] (in order_scope)
<^l x :> x [not, in mathcomp.order.preorder] (in order_scope)
<^l x :> x [not, in mathcomp.order.preorder] (in order_scope)
<^p x [not, in mathcomp.order.preorder] (in order_scope)
<^p x :> x [not, in mathcomp.order.preorder] (in order_scope)
<^sp x [not, in mathcomp.order.preorder] (in order_scope)
<^sp x :> x [not, in mathcomp.order.preorder] (in order_scope)
> x [not, in mathcomp.order.preorder] (in order_scope)
> x :> x [not, in mathcomp.order.preorder] (in order_scope)
>< x [not, in mathcomp.order.preorder] (in order_scope)
>< x :> x [not, in mathcomp.order.preorder] (in order_scope)
><^d x [not, in mathcomp.order.preorder] (in order_scope)
><^d x :> x [not, in mathcomp.order.preorder] (in order_scope)
><^l x [not, in mathcomp.order.preorder] (in order_scope)
><^l x [not, in mathcomp.order.preorder] (in order_scope)
><^l x :> x [not, in mathcomp.order.preorder] (in order_scope)
><^l x :> x [not, in mathcomp.order.preorder] (in order_scope)
><^p x [not, in mathcomp.order.preorder] (in order_scope)
><^p x :> x [not, in mathcomp.order.preorder] (in order_scope)
><^sp x [not, in mathcomp.order.preorder] (in order_scope)
><^sp x :> x [not, in mathcomp.order.preorder] (in order_scope)
>= x [not, in mathcomp.order.preorder] (in order_scope)
>= x :> x [not, in mathcomp.order.preorder] (in order_scope)
>=< x [not, in mathcomp.order.preorder] (in order_scope)
>=< x :> x [not, in mathcomp.order.preorder] (in order_scope)
>=<^d x [not, in mathcomp.order.preorder] (in order_scope)
>=<^d x :> x [not, in mathcomp.order.preorder] (in order_scope)
>=<^l x [not, in mathcomp.order.preorder] (in order_scope)
>=<^l x [not, in mathcomp.order.preorder] (in order_scope)
>=<^l x :> x [not, in mathcomp.order.preorder] (in order_scope)
>=<^l x :> x [not, in mathcomp.order.preorder] (in order_scope)
>=<^p x [not, in mathcomp.order.preorder] (in order_scope)
>=<^p x :> x [not, in mathcomp.order.preorder] (in order_scope)
>=<^sp x [not, in mathcomp.order.preorder] (in order_scope)
>=<^sp x :> x [not, in mathcomp.order.preorder] (in order_scope)
>=^d x [not, in mathcomp.order.preorder] (in order_scope)
>=^d x :> x [not, in mathcomp.order.preorder] (in order_scope)
>=^l x [not, in mathcomp.order.preorder] (in order_scope)
>=^l x [not, in mathcomp.order.preorder] (in order_scope)
>=^l x :> x [not, in mathcomp.order.preorder] (in order_scope)
>=^l x :> x [not, in mathcomp.order.preorder] (in order_scope)
>=^p x [not, in mathcomp.order.preorder] (in order_scope)
>=^p x :> x [not, in mathcomp.order.preorder] (in order_scope)
>=^sp x [not, in mathcomp.order.preorder] (in order_scope)
>=^sp x :> x [not, in mathcomp.order.preorder] (in order_scope)
>^d x [not, in mathcomp.order.preorder] (in order_scope)
>^d x :> x [not, in mathcomp.order.preorder] (in order_scope)
>^l x [not, in mathcomp.order.preorder] (in order_scope)
>^l x [not, in mathcomp.order.preorder] (in order_scope)
>^l x :> x [not, in mathcomp.order.preorder] (in order_scope)
>^l x :> x [not, in mathcomp.order.preorder] (in order_scope)
>^p x [not, in mathcomp.order.preorder] (in order_scope)
>^p x :> x [not, in mathcomp.order.preorder] (in order_scope)
>^sp x [not, in mathcomp.order.preorder] (in order_scope)
>^sp x :> x [not, in mathcomp.order.preorder] (in order_scope)
[ arg max_ ( x > x ) x ] [not, in mathcomp.order.preorder] (in order_scope)
[ arg max_ ( x > x in x ) x ] [not, in mathcomp.order.preorder] (in order_scope)
[ arg max_ ( x > x | x ) x ] [not, in mathcomp.order.preorder] (in order_scope)
[ arg min_ ( x < x ) x ] [not, in mathcomp.order.preorder] (in order_scope)
[ arg min_ ( x < x in x ) x ] [not, in mathcomp.order.preorder] (in order_scope)
[ arg min_ ( x < x | x ) x ] [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_ ( x : x ) x [not, in mathcomp.order.order] (in order_scope)
\gcd_ ( x : x | x ) x [not, in mathcomp.order.order] (in order_scope)
\gcd_ ( x < x ) x [not, in mathcomp.order.order] (in order_scope)
\gcd_ ( x < x | x ) x [not, in mathcomp.order.order] (in order_scope)
\gcd_ ( x <- x ) x [not, in mathcomp.order.order] (in order_scope)
\gcd_ ( x <- x | x ) x [not, in mathcomp.order.order] (in order_scope)
\gcd_ ( x <= x < x ) x [not, in mathcomp.order.order] (in order_scope)
\gcd_ ( x <= x < x | x ) x [not, in mathcomp.order.order] (in order_scope)
\gcd_ ( x in x ) x [not, in mathcomp.order.order] (in order_scope)
\gcd_ ( x in x | x ) x [not, in mathcomp.order.order] (in order_scope)
\gcd_ ( x | x ) x [not, in mathcomp.order.order] (in order_scope)
\gcd_ x x [not, in mathcomp.order.order] (in order_scope)
\join^d_ ( x : x ) x [not, in mathcomp.order.order] (in order_scope)
\join^d_ ( x : x | x ) x [not, in mathcomp.order.order] (in order_scope)
\join^d_ ( x < x ) x [not, in mathcomp.order.order] (in order_scope)
\join^d_ ( x < x | x ) x [not, in mathcomp.order.order] (in order_scope)
\join^d_ ( x <- x ) x [not, in mathcomp.order.order] (in order_scope)
\join^d_ ( x <- x | x ) x [not, in mathcomp.order.order] (in order_scope)
\join^d_ ( x <= x < x ) x [not, in mathcomp.order.order] (in order_scope)
\join^d_ ( x <= x < x | x ) x [not, in mathcomp.order.order] (in order_scope)
\join^d_ ( x in x ) x [not, in mathcomp.order.order] (in order_scope)
\join^d_ ( x in x | x ) x [not, in mathcomp.order.order] (in order_scope)
\join^d_ ( x | x ) x [not, in mathcomp.order.order] (in order_scope)
\join^d_ x x [not, in mathcomp.order.order] (in order_scope)
\join^l_ ( x : x ) x [not, in mathcomp.order.order] (in order_scope)
\join^l_ ( x : x ) x [not, in mathcomp.order.order] (in order_scope)
\join^l_ ( x : x | x ) x [not, in mathcomp.order.order] (in order_scope)
\join^l_ ( x : x | x ) x [not, in mathcomp.order.order] (in order_scope)
\join^l_ ( x < x ) x [not, in mathcomp.order.order] (in order_scope)
\join^l_ ( x < x ) x [not, in mathcomp.order.order] (in order_scope)
\join^l_ ( x < x | x ) x [not, in mathcomp.order.order] (in order_scope)
\join^l_ ( x < x | x ) x [not, in mathcomp.order.order] (in order_scope)
\join^l_ ( x <- x ) x [not, in mathcomp.order.order] (in order_scope)
\join^l_ ( x <- x ) x [not, in mathcomp.order.order] (in order_scope)
\join^l_ ( x <- x | x ) x [not, in mathcomp.order.order] (in order_scope)
\join^l_ ( x <- x | x ) x [not, in mathcomp.order.order] (in order_scope)
\join^l_ ( x <= x < x ) x [not, in mathcomp.order.order] (in order_scope)
\join^l_ ( x <= x < x ) x [not, in mathcomp.order.order] (in order_scope)
\join^l_ ( x <= x < x | x ) x [not, in mathcomp.order.order] (in order_scope)
\join^l_ ( x <= x < x | x ) x [not, in mathcomp.order.order] (in order_scope)
\join^l_ ( x in x ) x [not, in mathcomp.order.order] (in order_scope)
\join^l_ ( x in x ) x [not, in mathcomp.order.order] (in order_scope)
\join^l_ ( x in x | x ) x [not, in mathcomp.order.order] (in order_scope)
\join^l_ ( x in x | x ) x [not, in mathcomp.order.order] (in order_scope)
\join^l_ ( x | x ) x [not, in mathcomp.order.order] (in order_scope)
\join^l_ ( x | x ) x [not, in mathcomp.order.order] (in order_scope)
\join^l_ x x [not, in mathcomp.order.order] (in order_scope)
\join^l_ x x [not, in mathcomp.order.order] (in order_scope)
\join^p_ ( x : x ) x [not, in mathcomp.order.order] (in order_scope)
\join^p_ ( x : x | x ) x [not, in mathcomp.order.order] (in order_scope)
\join^p_ ( x < x ) x [not, in mathcomp.order.order] (in order_scope)
\join^p_ ( x < x | x ) x [not, in mathcomp.order.order] (in order_scope)
\join^p_ ( x <- x ) x [not, in mathcomp.order.order] (in order_scope)
\join^p_ ( x <- x | x ) x [not, in mathcomp.order.order] (in order_scope)
\join^p_ ( x <= x < x ) x [not, in mathcomp.order.order] (in order_scope)
\join^p_ ( x <= x < x | x ) x [not, in mathcomp.order.order] (in order_scope)
\join^p_ ( x in x ) x [not, in mathcomp.order.order] (in order_scope)
\join^p_ ( x in x | x ) x [not, in mathcomp.order.order] (in order_scope)
\join^p_ ( x | x ) x [not, in mathcomp.order.order] (in order_scope)
\join^p_ x x [not, in mathcomp.order.order] (in order_scope)
\join^sp_ ( x : x ) x [not, in mathcomp.order.order] (in order_scope)
\join^sp_ ( x : x | x ) x [not, in mathcomp.order.order] (in order_scope)
\join^sp_ ( x < x ) x [not, in mathcomp.order.order] (in order_scope)
\join^sp_ ( x < x | x ) x [not, in mathcomp.order.order] (in order_scope)
\join^sp_ ( x <- x ) x [not, in mathcomp.order.order] (in order_scope)
\join^sp_ ( x <- x | x ) x [not, in mathcomp.order.order] (in order_scope)
\join^sp_ ( x <= x < x ) x [not, in mathcomp.order.order] (in order_scope)
\join^sp_ ( x <= x < x | x ) x [not, in mathcomp.order.order] (in order_scope)
\join^sp_ ( x in x ) x [not, in mathcomp.order.order] (in order_scope)
\join^sp_ ( x in x | x ) x [not, in mathcomp.order.order] (in order_scope)
\join^sp_ ( x | x ) x [not, in mathcomp.order.order] (in order_scope)
\join^sp_ x x [not, in mathcomp.order.order] (in order_scope)
\join_ ( x : x ) x [not, in mathcomp.order.order] (in order_scope)
\join_ ( x : x | x ) x [not, in mathcomp.order.order] (in order_scope)
\join_ ( x < x ) x [not, in mathcomp.order.order] (in order_scope)
\join_ ( x < x | x ) x [not, in mathcomp.order.order] (in order_scope)
\join_ ( x <- x ) x [not, in mathcomp.order.order] (in order_scope)
\join_ ( x <- x | x ) x [not, in mathcomp.order.order] (in order_scope)
\join_ ( x <= x < x ) x [not, in mathcomp.order.order] (in order_scope)
\join_ ( x <= x < x | x ) x [not, in mathcomp.order.order] (in order_scope)
\join_ ( x in x ) x [not, in mathcomp.order.order] (in order_scope)
\join_ ( x in x | x ) x [not, in mathcomp.order.order] (in order_scope)
\join_ ( x | x ) x [not, in mathcomp.order.order] (in order_scope)
\join_ x x [not, in mathcomp.order.order] (in order_scope)
\lcm_ ( x : x ) x [not, in mathcomp.order.order] (in order_scope)
\lcm_ ( x : x | x ) x [not, in mathcomp.order.order] (in order_scope)
\lcm_ ( x < x ) x [not, in mathcomp.order.order] (in order_scope)
\lcm_ ( x < x | x ) x [not, in mathcomp.order.order] (in order_scope)
\lcm_ ( x <- x ) x [not, in mathcomp.order.order] (in order_scope)
\lcm_ ( x <- x | x ) x [not, in mathcomp.order.order] (in order_scope)
\lcm_ ( x <= x < x ) x [not, in mathcomp.order.order] (in order_scope)
\lcm_ ( x <= x < x | x ) x [not, in mathcomp.order.order] (in order_scope)
\lcm_ ( x in x ) x [not, in mathcomp.order.order] (in order_scope)
\lcm_ ( x in x | x ) x [not, in mathcomp.order.order] (in order_scope)
\lcm_ ( x | x ) x [not, in mathcomp.order.order] (in order_scope)
\lcm_ x x [not, in mathcomp.order.order] (in order_scope)
\max^d_ ( x : x ) x [not, in mathcomp.order.preorder] (in order_scope)
\max^d_ ( x : x | x ) x [not, in mathcomp.order.preorder] (in order_scope)
\max^d_ ( x < x ) x [not, in mathcomp.order.preorder] (in order_scope)
\max^d_ ( x < x ) x [not, in mathcomp.order.preorder] (in order_scope)
\max^d_ ( x < x | x ) x [not, in mathcomp.order.preorder] (in order_scope)
\max^d_ ( x <- x | x ) x [not, in mathcomp.order.preorder] (in order_scope)
\max^d_ ( x <= x < x ) x [not, in mathcomp.order.preorder] (in order_scope)
\max^d_ ( x <= x < x | x ) x [not, in mathcomp.order.preorder] (in order_scope)
\max^d_ ( x in x ) x [not, in mathcomp.order.preorder] (in order_scope)
\max^d_ ( x in x | x ) x [not, in mathcomp.order.preorder] (in order_scope)
\max^d_ ( x | x ) x [not, in mathcomp.order.preorder] (in order_scope)
\max^d_ x x [not, in mathcomp.order.preorder] (in order_scope)
\max^l_ ( x : x ) x [not, in mathcomp.order.order] (in order_scope)
\max^l_ ( x : x ) x [not, in mathcomp.order.order] (in order_scope)
\max^l_ ( x : x | x ) x [not, in mathcomp.order.order] (in order_scope)
\max^l_ ( x : x | x ) x [not, in mathcomp.order.order] (in order_scope)
\max^l_ ( x < x ) x [not, in mathcomp.order.order] (in order_scope)
\max^l_ ( x < x ) x [not, in mathcomp.order.order] (in order_scope)
\max^l_ ( x < x ) x [not, in mathcomp.order.order] (in order_scope)
\max^l_ ( x < x ) x [not, in mathcomp.order.order] (in order_scope)
\max^l_ ( x < x | x ) x [not, in mathcomp.order.order] (in order_scope)
\max^l_ ( x < x | x ) x [not, in mathcomp.order.order] (in order_scope)
\max^l_ ( x <- x | x ) x [not, in mathcomp.order.order] (in order_scope)
\max^l_ ( x <- x | x ) x [not, in mathcomp.order.order] (in order_scope)
\max^l_ ( x <= x < x ) x [not, in mathcomp.order.order] (in order_scope)
\max^l_ ( x <= x < x ) x [not, in mathcomp.order.order] (in order_scope)
\max^l_ ( x <= x < x | x ) x [not, in mathcomp.order.order] (in order_scope)
\max^l_ ( x <= x < x | x ) x [not, in mathcomp.order.order] (in order_scope)
\max^l_ ( x in x ) x [not, in mathcomp.order.order] (in order_scope)
\max^l_ ( x in x ) x [not, in mathcomp.order.order] (in order_scope)
\max^l_ ( x in x | x ) x [not, in mathcomp.order.order] (in order_scope)
\max^l_ ( x in x | x ) x [not, in mathcomp.order.order] (in order_scope)
\max^l_ ( x | x ) x [not, in mathcomp.order.order] (in order_scope)
\max^l_ ( x | x ) x [not, in mathcomp.order.order] (in order_scope)
\max^l_ x x [not, in mathcomp.order.order] (in order_scope)
\max^l_ x x [not, in mathcomp.order.order] (in order_scope)
\max^p_ ( x : x ) x [not, in mathcomp.order.order] (in order_scope)
\max^p_ ( x : x | x ) x [not, in mathcomp.order.order] (in order_scope)
\max^p_ ( x < x ) x [not, in mathcomp.order.order] (in order_scope)
\max^p_ ( x < x ) x [not, in mathcomp.order.order] (in order_scope)
\max^p_ ( x < x | x ) x [not, in mathcomp.order.order] (in order_scope)
\max^p_ ( x <- x | x ) x [not, in mathcomp.order.order] (in order_scope)
\max^p_ ( x <= x < x ) x [not, in mathcomp.order.order] (in order_scope)
\max^p_ ( x <= x < x | x ) x [not, in mathcomp.order.order] (in order_scope)
\max^p_ ( x in x ) x [not, in mathcomp.order.order] (in order_scope)
\max^p_ ( x in x | x ) x [not, in mathcomp.order.order] (in order_scope)
\max^p_ ( x | x ) x [not, in mathcomp.order.order] (in order_scope)
\max^p_ x x [not, in mathcomp.order.order] (in order_scope)
\max^sp_ ( x : x ) x [not, in mathcomp.order.order] (in order_scope)
\max^sp_ ( x : x | x ) x [not, in mathcomp.order.order] (in order_scope)
\max^sp_ ( x < x ) x [not, in mathcomp.order.order] (in order_scope)
\max^sp_ ( x < x ) x [not, in mathcomp.order.order] (in order_scope)
\max^sp_ ( x < x | x ) x [not, in mathcomp.order.order] (in order_scope)
\max^sp_ ( x <- x | x ) x [not, in mathcomp.order.order] (in order_scope)
\max^sp_ ( x <= x < x ) x [not, in mathcomp.order.order] (in order_scope)
\max^sp_ ( x <= x < x | x ) x [not, in mathcomp.order.order] (in order_scope)
\max^sp_ ( x in x ) x [not, in mathcomp.order.order] (in order_scope)
\max^sp_ ( x in x | x ) x [not, in mathcomp.order.order] (in order_scope)
\max^sp_ ( x | x ) x [not, in mathcomp.order.order] (in order_scope)
\max^sp_ x x [not, in mathcomp.order.order] (in order_scope)
\max_ ( x : x ) x [not, in mathcomp.order.preorder] (in order_scope)
\max_ ( x : x | x ) x [not, in mathcomp.order.preorder] (in order_scope)
\max_ ( x < x ) x [not, in mathcomp.order.preorder] (in order_scope)
\max_ ( x < x ) x [not, in mathcomp.order.preorder] (in order_scope)
\max_ ( x < x | x ) x [not, in mathcomp.order.preorder] (in order_scope)
\max_ ( x <- x | x ) x [not, in mathcomp.order.preorder] (in order_scope)
\max_ ( x <= x < x ) x [not, in mathcomp.order.preorder] (in order_scope)
\max_ ( x <= x < x | x ) x [not, in mathcomp.order.preorder] (in order_scope)
\max_ ( x in x ) x [not, in mathcomp.order.preorder] (in order_scope)
\max_ ( x in x | x ) x [not, in mathcomp.order.preorder] (in order_scope)
\max_ ( x | x ) x [not, in mathcomp.order.preorder] (in order_scope)
\max_ x x [not, in mathcomp.order.preorder] (in order_scope)
\meet^d_ ( x : x ) x [not, in mathcomp.order.order] (in order_scope)
\meet^d_ ( x : x | x ) x [not, in mathcomp.order.order] (in order_scope)
\meet^d_ ( x < x ) x [not, in mathcomp.order.order] (in order_scope)
\meet^d_ ( x < x | x ) x [not, in mathcomp.order.order] (in order_scope)
\meet^d_ ( x <- x ) x [not, in mathcomp.order.order] (in order_scope)
\meet^d_ ( x <- x | x ) x [not, in mathcomp.order.order] (in order_scope)
\meet^d_ ( x <= x < x ) x [not, in mathcomp.order.order] (in order_scope)
\meet^d_ ( x <= x < x | x ) x [not, in mathcomp.order.order] (in order_scope)
\meet^d_ ( x in x ) x [not, in mathcomp.order.order] (in order_scope)
\meet^d_ ( x in x | x ) x [not, in mathcomp.order.order] (in order_scope)
\meet^d_ ( x | x ) x [not, in mathcomp.order.order] (in order_scope)
\meet^d_ x x [not, in mathcomp.order.order] (in order_scope)
\meet^l_ ( x : x ) x [not, in mathcomp.order.order] (in order_scope)
\meet^l_ ( x : x ) x [not, in mathcomp.order.order] (in order_scope)
\meet^l_ ( x : x | x ) x [not, in mathcomp.order.order] (in order_scope)
\meet^l_ ( x : x | x ) x [not, in mathcomp.order.order] (in order_scope)
\meet^l_ ( x < x ) x [not, in mathcomp.order.order] (in order_scope)
\meet^l_ ( x < x ) x [not, in mathcomp.order.order] (in order_scope)
\meet^l_ ( x < x | x ) x [not, in mathcomp.order.order] (in order_scope)
\meet^l_ ( x < x | x ) x [not, in mathcomp.order.order] (in order_scope)
\meet^l_ ( x <- x ) x [not, in mathcomp.order.order] (in order_scope)
\meet^l_ ( x <- x ) x [not, in mathcomp.order.order] (in order_scope)
\meet^l_ ( x <- x | x ) x [not, in mathcomp.order.order] (in order_scope)
\meet^l_ ( x <- x | x ) x [not, in mathcomp.order.order] (in order_scope)
\meet^l_ ( x <= x < x ) x [not, in mathcomp.order.order] (in order_scope)
\meet^l_ ( x <= x < x ) x [not, in mathcomp.order.order] (in order_scope)
\meet^l_ ( x <= x < x | x ) x [not, in mathcomp.order.order] (in order_scope)
\meet^l_ ( x <= x < x | x ) x [not, in mathcomp.order.order] (in order_scope)
\meet^l_ ( x in x ) x [not, in mathcomp.order.order] (in order_scope)
\meet^l_ ( x in x ) x [not, in mathcomp.order.order] (in order_scope)
\meet^l_ ( x in x | x ) x [not, in mathcomp.order.order] (in order_scope)
\meet^l_ ( x in x | x ) x [not, in mathcomp.order.order] (in order_scope)
\meet^l_ ( x | x ) x [not, in mathcomp.order.order] (in order_scope)
\meet^l_ ( x | x ) x [not, in mathcomp.order.order] (in order_scope)
\meet^l_ x x [not, in mathcomp.order.order] (in order_scope)
\meet^l_ x x [not, in mathcomp.order.order] (in order_scope)
\meet^p_ ( x : x ) x [not, in mathcomp.order.order] (in order_scope)
\meet^p_ ( x : x | x ) x [not, in mathcomp.order.order] (in order_scope)
\meet^p_ ( x < x ) x [not, in mathcomp.order.order] (in order_scope)
\meet^p_ ( x < x | x ) x [not, in mathcomp.order.order] (in order_scope)
\meet^p_ ( x <- x ) x [not, in mathcomp.order.order] (in order_scope)
\meet^p_ ( x <- x | x ) x [not, in mathcomp.order.order] (in order_scope)
\meet^p_ ( x <= x < x ) x [not, in mathcomp.order.order] (in order_scope)
\meet^p_ ( x <= x < x | x ) x [not, in mathcomp.order.order] (in order_scope)
\meet^p_ ( x in x ) x [not, in mathcomp.order.order] (in order_scope)
\meet^p_ ( x in x | x ) x [not, in mathcomp.order.order] (in order_scope)
\meet^p_ ( x | x ) x [not, in mathcomp.order.order] (in order_scope)
\meet^p_ x x [not, in mathcomp.order.order] (in order_scope)
\meet^sp_ ( x : x ) x [not, in mathcomp.order.order] (in order_scope)
\meet^sp_ ( x : x | x ) x [not, in mathcomp.order.order] (in order_scope)
\meet^sp_ ( x < x ) x [not, in mathcomp.order.order] (in order_scope)
\meet^sp_ ( x < x | x ) x [not, in mathcomp.order.order] (in order_scope)
\meet^sp_ ( x <- x ) x [not, in mathcomp.order.order] (in order_scope)
\meet^sp_ ( x <- x | x ) x [not, in mathcomp.order.order] (in order_scope)
\meet^sp_ ( x <= x < x ) x [not, in mathcomp.order.order] (in order_scope)
\meet^sp_ ( x <= x < x | x ) x [not, in mathcomp.order.order] (in order_scope)
\meet^sp_ ( x in x ) x [not, in mathcomp.order.order] (in order_scope)
\meet^sp_ ( x in x | x ) x [not, in mathcomp.order.order] (in order_scope)
\meet^sp_ ( x | x ) x [not, in mathcomp.order.order] (in order_scope)
\meet^sp_ x x [not, in mathcomp.order.order] (in order_scope)
\meet_ ( x : x ) x [not, in mathcomp.order.order] (in order_scope)
\meet_ ( x : x | x ) x [not, in mathcomp.order.order] (in order_scope)
\meet_ ( x < x ) x [not, in mathcomp.order.order] (in order_scope)
\meet_ ( x < x | x ) x [not, in mathcomp.order.order] (in order_scope)
\meet_ ( x <- x ) x [not, in mathcomp.order.order] (in order_scope)
\meet_ ( x <- x | x ) x [not, in mathcomp.order.order] (in order_scope)
\meet_ ( x <= x < x ) x [not, in mathcomp.order.order] (in order_scope)
\meet_ ( x <= x < x | x ) x [not, in mathcomp.order.order] (in order_scope)
\meet_ ( x in x ) x [not, in mathcomp.order.order] (in order_scope)
\meet_ ( x in x | x ) x [not, in mathcomp.order.order] (in order_scope)
\meet_ ( x | x ) x [not, in mathcomp.order.order] (in order_scope)
\meet_ x x [not, in mathcomp.order.order] (in order_scope)
\min^d_ ( x : x ) x [not, in mathcomp.order.preorder] (in order_scope)
\min^d_ ( x : x | x ) x [not, in mathcomp.order.preorder] (in order_scope)
\min^d_ ( x < x ) x [not, in mathcomp.order.preorder] (in order_scope)
\min^d_ ( x < x ) x [not, in mathcomp.order.preorder] (in order_scope)
\min^d_ ( x < x | x ) x [not, in mathcomp.order.preorder] (in order_scope)
\min^d_ ( x <- x | x ) x [not, in mathcomp.order.preorder] (in order_scope)
\min^d_ ( x <= x < x ) x [not, in mathcomp.order.preorder] (in order_scope)
\min^d_ ( x <= x < x | x ) x [not, in mathcomp.order.preorder] (in order_scope)
\min^d_ ( x in x ) x [not, in mathcomp.order.preorder] (in order_scope)
\min^d_ ( x in x | x ) x [not, in mathcomp.order.preorder] (in order_scope)
\min^d_ ( x | x ) x [not, in mathcomp.order.preorder] (in order_scope)
\min^d_ x x [not, in mathcomp.order.preorder] (in order_scope)
\min^l_ ( x : x ) x [not, in mathcomp.order.order] (in order_scope)
\min^l_ ( x : x ) x [not, in mathcomp.order.order] (in order_scope)
\min^l_ ( x : x | x ) x [not, in mathcomp.order.order] (in order_scope)
\min^l_ ( x : x | x ) x [not, in mathcomp.order.order] (in order_scope)
\min^l_ ( x < x ) x [not, in mathcomp.order.order] (in order_scope)
\min^l_ ( x < x ) x [not, in mathcomp.order.order] (in order_scope)
\min^l_ ( x < x ) x [not, in mathcomp.order.order] (in order_scope)
\min^l_ ( x < x ) x [not, in mathcomp.order.order] (in order_scope)
\min^l_ ( x < x | x ) x [not, in mathcomp.order.order] (in order_scope)
\min^l_ ( x < x | x ) x [not, in mathcomp.order.order] (in order_scope)
\min^l_ ( x <- x | x ) x [not, in mathcomp.order.order] (in order_scope)
\min^l_ ( x <- x | x ) x [not, in mathcomp.order.order] (in order_scope)
\min^l_ ( x <= x < x ) x [not, in mathcomp.order.order] (in order_scope)
\min^l_ ( x <= x < x ) x [not, in mathcomp.order.order] (in order_scope)
\min^l_ ( x <= x < x | x ) x [not, in mathcomp.order.order] (in order_scope)
\min^l_ ( x <= x < x | x ) x [not, in mathcomp.order.order] (in order_scope)
\min^l_ ( x in x ) x [not, in mathcomp.order.order] (in order_scope)
\min^l_ ( x in x ) x [not, in mathcomp.order.order] (in order_scope)
\min^l_ ( x in x | x ) x [not, in mathcomp.order.order] (in order_scope)
\min^l_ ( x in x | x ) x [not, in mathcomp.order.order] (in order_scope)
\min^l_ ( x | x ) x [not, in mathcomp.order.order] (in order_scope)
\min^l_ ( x | x ) x [not, in mathcomp.order.order] (in order_scope)
\min^l_ x x [not, in mathcomp.order.order] (in order_scope)
\min^l_ x x [not, in mathcomp.order.order] (in order_scope)
\min^p_ ( x : x ) x [not, in mathcomp.order.order] (in order_scope)
\min^p_ ( x : x | x ) x [not, in mathcomp.order.order] (in order_scope)
\min^p_ ( x < x ) x [not, in mathcomp.order.order] (in order_scope)
\min^p_ ( x < x ) x [not, in mathcomp.order.order] (in order_scope)
\min^p_ ( x < x | x ) x [not, in mathcomp.order.order] (in order_scope)
\min^p_ ( x <- x | x ) x [not, in mathcomp.order.order] (in order_scope)
\min^p_ ( x <= x < x ) x [not, in mathcomp.order.order] (in order_scope)
\min^p_ ( x <= x < x | x ) x [not, in mathcomp.order.order] (in order_scope)
\min^p_ ( x in x ) x [not, in mathcomp.order.order] (in order_scope)
\min^p_ ( x in x | x ) x [not, in mathcomp.order.order] (in order_scope)
\min^p_ ( x | x ) x [not, in mathcomp.order.order] (in order_scope)
\min^p_ x x [not, in mathcomp.order.order] (in order_scope)
\min^sp_ ( x : x ) x [not, in mathcomp.order.order] (in order_scope)
\min^sp_ ( x : x | x ) x [not, in mathcomp.order.order] (in order_scope)
\min^sp_ ( x < x ) x [not, in mathcomp.order.order] (in order_scope)
\min^sp_ ( x < x ) x [not, in mathcomp.order.order] (in order_scope)
\min^sp_ ( x < x | x ) x [not, in mathcomp.order.order] (in order_scope)
\min^sp_ ( x <- x | x ) x [not, in mathcomp.order.order] (in order_scope)
\min^sp_ ( x <= x < x ) x [not, in mathcomp.order.order] (in order_scope)
\min^sp_ ( x <= x < x | x ) x [not, in mathcomp.order.order] (in order_scope)
\min^sp_ ( x in x ) x [not, in mathcomp.order.order] (in order_scope)
\min^sp_ ( x in x | x ) x [not, in mathcomp.order.order] (in order_scope)
\min^sp_ ( x | x ) x [not, in mathcomp.order.order] (in order_scope)
\min^sp_ x x [not, in mathcomp.order.order] (in order_scope)
\min_ ( x : x ) x [not, in mathcomp.order.preorder] (in order_scope)
\min_ ( x : x | x ) x [not, in mathcomp.order.preorder] (in order_scope)
\min_ ( x < x ) x [not, in mathcomp.order.preorder] (in order_scope)
\min_ ( x < x ) x [not, in mathcomp.order.preorder] (in order_scope)
\min_ ( x < x | x ) x [not, in mathcomp.order.preorder] (in order_scope)
\min_ ( x <- x | x ) x [not, in mathcomp.order.preorder] (in order_scope)
\min_ ( x <= x < x ) x [not, in mathcomp.order.preorder] (in order_scope)
\min_ ( x <= x < x | x ) x [not, in mathcomp.order.preorder] (in order_scope)
\min_ ( x in x ) x [not, in mathcomp.order.preorder] (in order_scope)
\min_ ( x in x | x ) x [not, in mathcomp.order.preorder] (in order_scope)
\min_ ( x | x ) x [not, in mathcomp.order.preorder] (in order_scope)
\min_ x x [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)
`[ x , +oo [ [not, in mathcomp.algebra.interval] (in order_scope)
`[ x , x [ [not, in mathcomp.algebra.interval] (in order_scope)
`[ x , x ] [not, in mathcomp.algebra.interval] (in order_scope)
`] -oo , +oo [ [not, in mathcomp.algebra.interval] (in order_scope)
`] -oo , x [ [not, in mathcomp.algebra.interval] (in order_scope)
`] -oo , x ] [not, in mathcomp.algebra.interval] (in order_scope)
`] x , +oo [ [not, in mathcomp.algebra.interval] (in order_scope)
`] x , x [ [not, in mathcomp.algebra.interval] (in order_scope)
`] x , x ] [not, in mathcomp.algebra.interval] (in order_scope)
~` x [not, in mathcomp.order.order] (in order_scope)
x %<| x [not, in mathcomp.order.preorder] (in order_scope)
x %| x [not, in mathcomp.order.preorder] (in order_scope)
x < x [not, in mathcomp.order.preorder] (in order_scope)
x < x [not, in mathcomp.order.preorder] (in order_scope)
x < x :> x [not, in mathcomp.order.preorder] (in order_scope)
x < x < x [not, in mathcomp.order.preorder] (in order_scope)
x < x <= x [not, in mathcomp.order.preorder] (in order_scope)
x < x ?<= if x [not, in mathcomp.order.preorder] (in order_scope)
x < x ?<= if x :> x [not, in mathcomp.order.preorder] (in order_scope)
x <= x [not, in mathcomp.order.preorder] (in order_scope)
x <= x [not, in mathcomp.order.preorder] (in order_scope)
x <= x :> x [not, in mathcomp.order.preorder] (in order_scope)
x <= x < x [not, in mathcomp.order.preorder] (in order_scope)
x <= x <= x [not, in mathcomp.order.preorder] (in order_scope)
x <= x ?= iff x [not, in mathcomp.order.preorder] (in order_scope)
x <= x ?= iff x :> x [not, in mathcomp.order.preorder] (in order_scope)
x <=^d x [not, in mathcomp.order.preorder] (in order_scope)
x <=^d x :> x [not, in mathcomp.order.preorder] (in order_scope)
x <=^d x <=^d x [not, in mathcomp.order.preorder] (in order_scope)
x <=^d x <^d x [not, in mathcomp.order.preorder] (in order_scope)
x <=^d x ?= iff x [not, in mathcomp.order.preorder] (in order_scope)
x <=^d x ?= iff x :> x [not, in mathcomp.order.preorder] (in order_scope)
x <=^l x [not, in mathcomp.order.preorder] (in order_scope)
x <=^l x [not, in mathcomp.order.preorder] (in order_scope)
x <=^l x :> x [not, in mathcomp.order.preorder] (in order_scope)
x <=^l x :> x [not, in mathcomp.order.preorder] (in order_scope)
x <=^l x <=^l x [not, in mathcomp.order.preorder] (in order_scope)
x <=^l x <=^l x [not, in mathcomp.order.preorder] (in order_scope)
x <=^l x <^l x [not, in mathcomp.order.preorder] (in order_scope)
x <=^l x <^l x [not, in mathcomp.order.preorder] (in order_scope)
x <=^l x ?= iff x [not, in mathcomp.order.preorder] (in order_scope)
x <=^l x ?= iff x [not, in mathcomp.order.preorder] (in order_scope)
x <=^l x ?= iff x :> x [not, in mathcomp.order.preorder] (in order_scope)
x <=^l x ?= iff x :> x [not, in mathcomp.order.preorder] (in order_scope)
x <=^p x [not, in mathcomp.order.preorder] (in order_scope)
x <=^p x :> x [not, in mathcomp.order.preorder] (in order_scope)
x <=^p x <=^p x [not, in mathcomp.order.preorder] (in order_scope)
x <=^p x <^p x [not, in mathcomp.order.preorder] (in order_scope)
x <=^p x ?= iff x [not, in mathcomp.order.preorder] (in order_scope)
x <=^p x ?= iff x :> x [not, in mathcomp.order.preorder] (in order_scope)
x <=^sp x [not, in mathcomp.order.preorder] (in order_scope)
x <=^sp x :> x [not, in mathcomp.order.preorder] (in order_scope)
x <=^sp x <=^sp x [not, in mathcomp.order.preorder] (in order_scope)
x <=^sp x <^sp x [not, in mathcomp.order.preorder] (in order_scope)
x <=^sp x ?= iff x [not, in mathcomp.order.preorder] (in order_scope)
x <=^sp x ?= iff x :> x [not, in mathcomp.order.preorder] (in order_scope)
x <^d x [not, in mathcomp.order.preorder] (in order_scope)
x <^d x :> x [not, in mathcomp.order.preorder] (in order_scope)
x <^d x <=^d x [not, in mathcomp.order.preorder] (in order_scope)
x <^d x <^d x [not, in mathcomp.order.preorder] (in order_scope)
x <^d x ?<= if x [not, in mathcomp.order.preorder] (in order_scope)
x <^d x ?<= if x :> x [not, in mathcomp.order.preorder] (in order_scope)
x <^l x [not, in mathcomp.order.preorder] (in order_scope)
x <^l x [not, in mathcomp.order.preorder] (in order_scope)
x <^l x :> x [not, in mathcomp.order.preorder] (in order_scope)
x <^l x :> x [not, in mathcomp.order.preorder] (in order_scope)
x <^l x <=^l x [not, in mathcomp.order.preorder] (in order_scope)
x <^l x <=^l x [not, in mathcomp.order.preorder] (in order_scope)
x <^l x <^l x [not, in mathcomp.order.preorder] (in order_scope)
x <^l x <^l x [not, in mathcomp.order.preorder] (in order_scope)
x <^p x [not, in mathcomp.order.preorder] (in order_scope)
x <^p x :> x [not, in mathcomp.order.preorder] (in order_scope)
x <^p x <=^p x [not, in mathcomp.order.preorder] (in order_scope)
x <^p x <^p x [not, in mathcomp.order.preorder] (in order_scope)
x <^sp x [not, in mathcomp.order.preorder] (in order_scope)
x <^sp x :> x [not, in mathcomp.order.preorder] (in order_scope)
x <^sp x <=^sp x [not, in mathcomp.order.preorder] (in order_scope)
x <^sp x <^sp x [not, in mathcomp.order.preorder] (in order_scope)
x > x [not, in mathcomp.order.preorder] (in order_scope)
x > x :> x [not, in mathcomp.order.preorder] (in order_scope)
x >< x [not, in mathcomp.order.preorder] (in order_scope)
x >< x [not, in mathcomp.order.preorder] (in order_scope)
x ><^d x [not, in mathcomp.order.preorder] (in order_scope)
x ><^l x [not, in mathcomp.order.preorder] (in order_scope)
x ><^l x [not, in mathcomp.order.preorder] (in order_scope)
x ><^p x [not, in mathcomp.order.preorder] (in order_scope)
x ><^sp x [not, in mathcomp.order.preorder] (in order_scope)
x >= x [not, in mathcomp.order.preorder] (in order_scope)
x >= x :> x [not, in mathcomp.order.preorder] (in order_scope)
x >=< x [not, in mathcomp.order.preorder] (in order_scope)
x >=< x [not, in mathcomp.order.preorder] (in order_scope)
x >=<^d x [not, in mathcomp.order.preorder] (in order_scope)
x >=<^l x [not, in mathcomp.order.preorder] (in order_scope)
x >=<^l x [not, in mathcomp.order.preorder] (in order_scope)
x >=<^p x [not, in mathcomp.order.preorder] (in order_scope)
x >=<^sp x [not, in mathcomp.order.preorder] (in order_scope)
x >=^d x [not, in mathcomp.order.preorder] (in order_scope)
x >=^d x :> x [not, in mathcomp.order.preorder] (in order_scope)
x >=^l x [not, in mathcomp.order.preorder] (in order_scope)
x >=^l x [not, in mathcomp.order.preorder] (in order_scope)
x >=^l x :> x [not, in mathcomp.order.preorder] (in order_scope)
x >=^l x :> x [not, in mathcomp.order.preorder] (in order_scope)
x >=^p x [not, in mathcomp.order.preorder] (in order_scope)
x >=^p x :> x [not, in mathcomp.order.preorder] (in order_scope)
x >=^sp x [not, in mathcomp.order.preorder] (in order_scope)
x >=^sp x :> x [not, in mathcomp.order.preorder] (in order_scope)
x >^d x [not, in mathcomp.order.preorder] (in order_scope)
x >^d x :> x [not, in mathcomp.order.preorder] (in order_scope)
x >^l x [not, in mathcomp.order.preorder] (in order_scope)
x >^l x [not, in mathcomp.order.preorder] (in order_scope)
x >^l x :> x [not, in mathcomp.order.preorder] (in order_scope)
x >^l x :> x [not, in mathcomp.order.preorder] (in order_scope)
x >^p x [not, in mathcomp.order.preorder] (in order_scope)
x >^p x :> x [not, in mathcomp.order.preorder] (in order_scope)
x >^sp x [not, in mathcomp.order.preorder] (in order_scope)
x >^sp x :> x [not, in mathcomp.order.preorder] (in order_scope)
x `&^d` x [not, in mathcomp.order.order] (in order_scope)
x `&^l` x [not, in mathcomp.order.order] (in order_scope)
x `&^l` x [not, in mathcomp.order.order] (in order_scope)
x `&^p` x [not, in mathcomp.order.order] (in order_scope)
x `&^sp` x [not, in mathcomp.order.order] (in order_scope)
x `&` x [not, in mathcomp.order.order] (in order_scope)
x `\` x [not, in mathcomp.order.order] (in order_scope)
x `|^d` x [not, in mathcomp.order.order] (in order_scope)
x `|^l` x [not, in mathcomp.order.order] (in order_scope)
x `|^l` x [not, in mathcomp.order.order] (in order_scope)
x `|^p` x [not, in mathcomp.order.order] (in order_scope)
x `|^sp` x [not, in mathcomp.order.order] (in order_scope)
x `|` x [not, in mathcomp.order.order] (in order_scope)

quotient_scope

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

rat_scope

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

relation_scope

x \; x [not, in mathcomp.classical.classical_sets] (in relation_scope)
x ^-1 [not, in mathcomp.classical.classical_sets] (in relation_scope)

ring_scope

'Im x [not, in mathcomp.algebra.numeric_hierarchy.numfield] (in ring_scope)
'Im x [not, in mathcomp.algebra.numeric_hierarchy.numfield] (in ring_scope)
'Re x [not, in mathcomp.algebra.numeric_hierarchy.numfield] (in ring_scope)
'Re x [not, in mathcomp.algebra.numeric_hierarchy.numfield] (in ring_scope)
'X [not, in mathcomp.algebra.poly] (in ring_scope)
'X^ x [not, in mathcomp.algebra.poly] (in ring_scope)
'Y [not, in mathcomp.algebra.polyXY] (in ring_scope)
'[ x , x ] [not, in mathcomp.algebra.spectral] (in ring_scope)
'[ x , x ] [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
'[ x , x ] [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
'[ x , x ] [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
'[ x , x ] [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
'[ x , x ] [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
'[ x , x ] [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
'[ x , x ] [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
'[ x , x ] [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
'[ x , x ] [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
'[ x , x ] [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
'[ x , x ] [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
'[ x , x ]_1 [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
'[ x , x ]_2 [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
'[ x ] [not, in mathcomp.algebra.spectral] (in ring_scope)
'[ x ] [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
'[ x ] [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
'[ x ] [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
'[ x ] [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
'[ x ] [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
'[ x ] [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
'[ x ] [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
'[ x ] [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
'[ x ] [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
'[ x ] [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
'[ x ] [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
'[ x ]_1 [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
'[ x ]_2 [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
'e_ x [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^ x [not, in mathcomp.algebra.qpoly] (in ring_scope)
'qX [not, in mathcomp.algebra.qpoly] (in ring_scope)
+oo [not, in mathcomp.analysis.normedtype_theory.num_normedtype] (in ring_scope)
+oo_ x [not, in mathcomp.analysis.normedtype_theory.num_normedtype] (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)
- x [not, in mathcomp.boot.nmodule] (in ring_scope)
- x [not, in mathcomp.boot.nmodule] (in ring_scope)
- x [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
-oo [not, in mathcomp.analysis.normedtype_theory.num_normedtype] (in ring_scope)
-oo_ x [not, in mathcomp.analysis.normedtype_theory.num_normedtype] (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)
< x [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in ring_scope)
< x :> x [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in ring_scope)
<= x [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in ring_scope)
<= x :> x [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in ring_scope)
> x [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in ring_scope)
> x :> x [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in ring_scope)
>< x [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in ring_scope)
>< x :> x [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in ring_scope)
>= x [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in ring_scope)
>= x :> x [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in ring_scope)
>=< x [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in ring_scope)
>=< x :> x [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in ring_scope)
[ arg max_ ( x > x ) x ] [not, in mathcomp.algebra.numeric_hierarchy.numdomain] (in ring_scope)
[ arg max_ ( x > x in x ) x ] [not, in mathcomp.algebra.numeric_hierarchy.numdomain] (in ring_scope)
[ arg max_ ( x > x | x ) x ] [not, in mathcomp.algebra.numeric_hierarchy.numdomain] (in ring_scope)
[ arg min_ ( x < x ) x ] [not, in mathcomp.algebra.numeric_hierarchy.numdomain] (in ring_scope)
[ arg min_ ( x < x in x ) x ] [not, in mathcomp.algebra.numeric_hierarchy.numdomain] (in ring_scope)
[ arg min_ ( x < x | x ) x ] [not, in mathcomp.algebra.numeric_hierarchy.numdomain] (in ring_scope)
[ char x ] [not, in mathcomp.algebra.algebraic_hierarchy.ssralg] (in ring_scope)
[ itv of x ] [not, in mathcomp.algebra.interval_inference] (in ring_scope)
[ normed x ] [not, in mathcomp.analysis.sequences] (in ring_scope)
[ pchar x ] [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
[ rat x // x ] [not, in mathcomp.algebra.rat] (in ring_scope)
[ rat x // x ] [not, in mathcomp.algebra.rat] (in ring_scope)
[ sequence x ]_ x [not, in mathcomp.analysis.sequences] (in ring_scope)
[ series x ]_ x [not, in mathcomp.analysis.sequences] (in ring_scope)
[ sgn of x ] [not, in mathcomp.reals.signed] (in ring_scope)
\- x [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)
\1_ x [not, in mathcomp.analysis.numfun] (in ring_scope)
\adj x [not, in mathcomp.algebra.matrix] (in ring_scope)
\col_ ( x < x ) x [not, in mathcomp.algebra.matrix] (in ring_scope)
\col_ x x [not, in mathcomp.algebra.matrix] (in ring_scope)
\d_ x [not, in mathcomp.analysis.measure_theory.dirac_measure] (in ring_scope)
\det x [not, in mathcomp.algebra.matrix] (in ring_scope)
\esum_ ( x in x ) x [not, in mathcomp.analysis.esum] (in ring_scope)
\int [ x ]_ ( x in x ) x [not, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_Rintegral] (in ring_scope)
\int [ x ]_ x x [not, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_Rintegral] (in ring_scope)
\matrix[ x ]_ ( x , x ) x [not, in mathcomp.algebra.matrix] (in ring_scope)
\matrix_ ( x , x ) x [not, in mathcomp.algebra.matrix] (in ring_scope)
\matrix_ ( x , x < x ) x [not, in mathcomp.algebra.matrix] (in ring_scope)
\matrix_ ( x < x ) x [not, in mathcomp.algebra.matrix] (in ring_scope)
\matrix_ ( x < x , x < x ) x [not, in mathcomp.algebra.matrix] (in ring_scope)
\matrix_ x x [not, in mathcomp.algebra.matrix] (in ring_scope)
\mxblock_ ( x , x ) x [not, in mathcomp.algebra.matrix] (in ring_scope)
\mxblock_ ( x , x ) x [not, in mathcomp.algebra.matrix] (in ring_scope)
\mxblock_ ( x , x < x ) x [not, in mathcomp.algebra.matrix] (in ring_scope)
\mxblock_ ( x < x , x < x ) x [not, in mathcomp.algebra.matrix] (in ring_scope)
\mxcol_ ( x < x ) x [not, in mathcomp.algebra.matrix] (in ring_scope)
\mxcol_ x x [not, in mathcomp.algebra.matrix] (in ring_scope)
\mxcol_ x x [not, in mathcomp.algebra.matrix] (in ring_scope)
\mxdiag_ ( x < x ) x [not, in mathcomp.algebra.matrix] (in ring_scope)
\mxdiag_ x x [not, in mathcomp.algebra.matrix] (in ring_scope)
\mxdiag_ x x [not, in mathcomp.algebra.matrix] (in ring_scope)
\mxrow_ ( x < x ) x [not, in mathcomp.algebra.matrix] (in ring_scope)
\mxrow_ x x [not, in mathcomp.algebra.matrix] (in ring_scope)
\mxrow_ x x [not, in mathcomp.algebra.matrix] (in ring_scope)
\poly_ ( x < x ) x [not, in mathcomp.algebra.poly] (in ring_scope)
\prod_ ( x : x ) x [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
\prod_ ( x : x | x ) x [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
\prod_ ( x < x ) x [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
\prod_ ( x < x | x ) x [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
\prod_ ( x <- x ) x [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
\prod_ ( x <- x | x ) x [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
\prod_ ( x <= x < x ) x [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
\prod_ ( x <= x < x | x ) x [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
\prod_ ( x in x ) x [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
\prod_ ( x in x | x ) x [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
\prod_ ( x | x ) x [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
\prod_ x x [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
\row_ ( x < x ) x [not, in mathcomp.algebra.matrix] (in ring_scope)
\row_ x x [not, in mathcomp.algebra.matrix] (in ring_scope)
\sum_ ( x : x ) x [not, in mathcomp.boot.nmodule] (in ring_scope)
\sum_ ( x : x ) x [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
\sum_ ( x : x | x ) x [not, in mathcomp.boot.nmodule] (in ring_scope)
\sum_ ( x : x | x ) x [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
\sum_ ( x < x ) x [not, in mathcomp.boot.nmodule] (in ring_scope)
\sum_ ( x < x ) x [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
\sum_ ( x < x | x ) x [not, in mathcomp.boot.nmodule] (in ring_scope)
\sum_ ( x < x | x ) x [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
\sum_ ( x <- x ) x [not, in mathcomp.boot.nmodule] (in ring_scope)
\sum_ ( x <- x ) x [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
\sum_ ( x <- x | x ) x [not, in mathcomp.boot.nmodule] (in ring_scope)
\sum_ ( x <- x | x ) x [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
\sum_ ( x <= x < x ) x [not, in mathcomp.boot.nmodule] (in ring_scope)
\sum_ ( x <= x < x ) x [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
\sum_ ( x <= x < x | x ) x [not, in mathcomp.boot.nmodule] (in ring_scope)
\sum_ ( x <= x < x | x ) x [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
\sum_ ( x \in x ) x [not, in mathcomp.classical.fsbigop] (in ring_scope)
\sum_ ( x in x ) x [not, in mathcomp.boot.nmodule] (in ring_scope)
\sum_ ( x in x ) x [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
\sum_ ( x in x | x ) x [not, in mathcomp.boot.nmodule] (in ring_scope)
\sum_ ( x in x | x ) x [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
\sum_ ( x | x ) x [not, in mathcomp.boot.nmodule] (in ring_scope)
\sum_ ( x | x ) x [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
\sum_ x x [not, in mathcomp.boot.nmodule] (in ring_scope)
\sum_ x x [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
\tr x [not, in mathcomp.algebra.matrix] (in ring_scope)
\tr x [not, in mathcomp.algebra.matrix] (in ring_scope)
\tr x [not, in mathcomp.algebra.matrix] (in ring_scope)
`1- x [not, in mathcomp.classical.unstable] (in ring_scope)
`[ x , +oo [ [not, in mathcomp.algebra.interval] (in ring_scope)
`[ x , x [ [not, in mathcomp.algebra.interval] (in ring_scope)
`[ x , x ] [not, in mathcomp.algebra.interval] (in ring_scope)
`] -oo , +oo [ [not, in mathcomp.algebra.interval] (in ring_scope)
`] -oo , x [ [not, in mathcomp.algebra.interval] (in ring_scope)
`] -oo , x ] [not, in mathcomp.algebra.interval] (in ring_scope)
`] x , +oo [ [not, in mathcomp.algebra.interval] (in ring_scope)
`] x , x [ [not, in mathcomp.algebra.interval] (in ring_scope)
`] x , x ] [not, in mathcomp.algebra.interval] (in ring_scope)
`| x | [not, in mathcomp.algebra.numeric_hierarchy.numdomain] (in ring_scope)
`| x | [not, in mathcomp.algebra.numeric_hierarchy.numdomain] (in ring_scope)
`| x | [not, in mathcomp.algebra.numeric_hierarchy.numdomain] (in ring_scope)
`| x | [not, in mathcomp.algebra.numeric_hierarchy.numdomain] (in ring_scope)
`| x | [not, in mathcomp.algebra.numeric_hierarchy.numdomain] (in ring_scope)
{ additive_charge set x -> \bar x } [not, in mathcomp.analysis.charge] (in ring_scope)
{ bilinear x -> x -> x | x & x } [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
{ bilinear x -> x -> x | x } [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
{ bilinear x -> x -> x } [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
{ biscalar x } [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
{ charge set x -> \bar x } [not, in mathcomp.analysis.charge] (in ring_scope)
{ content set x -> \bar x } [not, in mathcomp.analysis.measure_theory.measure_function] (in ring_scope)
{ dot x for x } [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
{ finite_measure set x -> \bar x } [not, in mathcomp.analysis.measure_theory.measure_function] (in ring_scope)
{ hermitian x for x & x } [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
{ hermitian_sym x for x } [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
{ measure set x -> \bar x } [not, in mathcomp.analysis.measure_theory.measure_function] (in ring_scope)
{ nonneg x } [not, in mathcomp.reals.signed] (in ring_scope)
{ nonneg x } [not, in mathcomp.algebra.interval_inference] (in ring_scope)
{ num x & x & x } [not, in mathcomp.reals.signed] (in ring_scope)
{ outer_measure set x -> \bar x } [not, in mathcomp.analysis.measure_theory.measure_extension] (in ring_scope)
{ posnum x } [not, in mathcomp.reals.signed] (in ring_scope)
{ posnum x } [not, in mathcomp.algebra.interval_inference] (in ring_scope)
{ sfinite_measure set x -> \bar x } [not, in mathcomp.analysis.measure_theory.measure_function] (in ring_scope)
{ sigma_finite_content set x -> \bar x } [not, in mathcomp.analysis.measure_theory.measure_function] (in ring_scope)
{ sigma_finite_measure set x -> \bar x } [not, in mathcomp.analysis.measure_theory.measure_function] (in ring_scope)
{ skew_symmetric x } [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
{ symmetric x } [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
x != x :> int [not, in mathcomp.algebra.ssrint] (in ring_scope)
x != x :> int [not, in mathcomp.algebra.ssrint] (in ring_scope)
x %% x [not, in mathcomp.algebra.polydiv] (in ring_scope)
x %/ x [not, in mathcomp.algebra.polydiv] (in ring_scope)
x %:A [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
x %:A [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
x %:M [not, in mathcomp.algebra.matrix] (in ring_scope)
x %:M [not, in mathcomp.algebra.matrix] (in ring_scope)
x %:M [not, in mathcomp.algebra.matrix] (in ring_scope)
x %:M [not, in mathcomp.algebra.matrix] (in ring_scope)
x %:P [not, in mathcomp.algebra.poly] (in ring_scope)
x %:Q [not, in mathcomp.algebra.rat] (in ring_scope)
x %:R [not, in mathcomp.boot.nmodule] (in ring_scope)
x %:R [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
x %:R [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
x %:Z [not, in mathcomp.algebra.ssrint] (in ring_scope)
x %:i01 [not, in mathcomp.algebra.interval_inference] (in ring_scope)
x %:i01 [not, in mathcomp.algebra.interval_inference] (in ring_scope)
x %:inum [not, in mathcomp.algebra.interval_inference] (in ring_scope)
x %:itv [not, in mathcomp.algebra.interval_inference] (in ring_scope)
x %:n01 [not, in mathcomp.algebra.interval_inference] (in ring_scope)
x %:n01 [not, in mathcomp.algebra.interval_inference] (in ring_scope)
x %:nng [not, in mathcomp.reals.signed] (in ring_scope)
x %:nng [not, in mathcomp.reals.signed] (in ring_scope)
x %:nng [not, in mathcomp.algebra.interval_inference] (in ring_scope)
x %:nng [not, in mathcomp.algebra.interval_inference] (in ring_scope)
x %:nngnum [not, in mathcomp.reals.signed] (in ring_scope)
x %:nngnum [not, in mathcomp.algebra.interval_inference] (in ring_scope)
x %:num [not, in mathcomp.reals.signed] (in ring_scope)
x %:num [not, in mathcomp.algebra.interval_inference] (in ring_scope)
x %:pos [not, in mathcomp.reals.signed] (in ring_scope)
x %:pos [not, in mathcomp.reals.signed] (in ring_scope)
x %:pos [not, in mathcomp.algebra.interval_inference] (in ring_scope)
x %:pos [not, in mathcomp.algebra.interval_inference] (in ring_scope)
x %:posnat [not, in mathcomp.algebra.interval_inference] (in ring_scope)
x %:posnum [not, in mathcomp.reals.signed] (in ring_scope)
x %:posnum [not, in mathcomp.algebra.interval_inference] (in ring_scope)
x %:sgn [not, in mathcomp.reals.signed] (in ring_scope)
x %:~R [not, in mathcomp.algebra.ssrint] (in ring_scope)
x %= x [not, in mathcomp.algebra.polydiv] (in ring_scope)
x %| x [not, in mathcomp.algebra.polydiv] (in ring_scope)
x '_|_ x [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
x '_|_ x [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
x * x [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
x * x [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
x *+ x [not, in mathcomp.boot.nmodule] (in ring_scope)
x *+ x [not, in mathcomp.boot.nmodule] (in ring_scope)
x *+ x [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
x *- x [not, in mathcomp.boot.nmodule] (in ring_scope)
x *- x [not, in mathcomp.boot.nmodule] (in ring_scope)
x *- x [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
x *: x [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
x *: x [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
x *m x [not, in mathcomp.algebra.matrix] (in ring_scope)
x *m x [not, in mathcomp.algebra.matrix] (in ring_scope)
x *m: x [not, in mathcomp.algebra.matrix] (in ring_scope)
x *t x [not, in mathcomp.algebra.tensor] (in ring_scope)
x *~ x [not, in mathcomp.algebra.ssrint] (in ring_scope)
x + x [not, in mathcomp.boot.nmodule] (in ring_scope)
x + x [not, in mathcomp.boot.nmodule] (in ring_scope)
x + x [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
x - x [not, in mathcomp.boot.nmodule] (in ring_scope)
x - x [not, in mathcomp.boot.nmodule] (in ring_scope)
x - x [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
x .-lagrange [not, in mathcomp.algebra.qpoly] (in ring_scope)
x .-lagrange_ [not, in mathcomp.algebra.qpoly] (in ring_scope)
x .-primitive_root [not, in mathcomp.algebra.poly] (in ring_scope)
x .-primitive_root [not, in mathcomp.algebra.poly] (in ring_scope)
x .-root [not, in mathcomp.algebra.numeric_hierarchy.numfield] (in ring_scope)
x .-sesqui [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
x .-unity_root [not, in mathcomp.algebra.poly] (in ring_scope)
x .-unity_root [not, in mathcomp.algebra.poly] (in ring_scope)
x .[ x , x ] [not, in mathcomp.algebra.polyXY] (in ring_scope)
x .[ x ] [not, in mathcomp.algebra.poly] (in ring_scope)
x .[ x ] [not, in mathcomp.algebra.poly] (in ring_scope)
x .~ [not, in mathcomp.classical.unstable] (in ring_scope)
x / x [not, in mathcomp.algebra.algebraic_hierarchy.divalg] (in ring_scope)
x < x [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in ring_scope)
x < x [not, in mathcomp.algebra.numeric_hierarchy.numdomain] (in ring_scope)
x < x [not, in mathcomp.algebra.numeric_hierarchy.numdomain] (in ring_scope)
x < x [not, in mathcomp.algebra.numeric_hierarchy.numdomain] (in ring_scope)
x < x :> x [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in ring_scope)
x < x < x [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in ring_scope)
x < x <= x [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in ring_scope)
x < x ?<= if x [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in ring_scope)
x < x ?<= if x :> x [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in ring_scope)
x <= x [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in ring_scope)
x <= x [not, in mathcomp.algebra.numeric_hierarchy.numdomain] (in ring_scope)
x <= x [not, in mathcomp.algebra.numeric_hierarchy.numdomain] (in ring_scope)
x <= x [not, in mathcomp.algebra.numeric_hierarchy.numdomain] (in ring_scope)
x <= x :> x [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in ring_scope)
x <= x < x [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in ring_scope)
x <= x <= x [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in ring_scope)
x <= x ?= iff x [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in ring_scope)
x <= x ?= iff x :> x [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in ring_scope)
x <> x :> int [not, in mathcomp.algebra.ssrint] (in ring_scope)
x <> x :> int [not, in mathcomp.algebra.ssrint] (in ring_scope)
x = x :> int [not, in mathcomp.algebra.ssrint] (in ring_scope)
x = x :> int [not, in mathcomp.algebra.ssrint] (in ring_scope)
x == x :> int [not, in mathcomp.algebra.ssrint] (in ring_scope)
x == x :> int [not, in mathcomp.algebra.ssrint] (in ring_scope)
x > x [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in ring_scope)
x > x :> x [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in ring_scope)
x >< x [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in ring_scope)
x >= x [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in ring_scope)
x >= x :> x [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in ring_scope)
x >=< x [not, in mathcomp.algebra.numeric_hierarchy.orderedzmod] (in ring_scope)
x @`[ x , x ] [not, in mathcomp.analysis.normedtype_theory.num_normedtype] (in ring_scope)
x @`] x , x [ [not, in mathcomp.analysis.normedtype_theory.num_normedtype] (in ring_scope)
x \* x [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
x \*: x [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
x \*o x [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
x \+ x [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
x \- x [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
x \Po x [not, in mathcomp.algebra.poly] (in ring_scope)
x \Po x [not, in mathcomp.algebra.poly] (in ring_scope)
x \^-1 [not, in mathcomp.classical.unstable] (in ring_scope)
x \o* x [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
x ^%:A [not, in mathcomp.field.finfield] (in ring_scope)
x ^ x [not, in mathcomp.field.separable] (in ring_scope)
x ^ x [not, in mathcomp.field.algebraics_fundamentals] (in ring_scope)
x ^ x [not, in mathcomp.algebra.ssrint] (in ring_scope)
x ^ x [not, in mathcomp.algebra.polyXY] (in ring_scope)
x ^* [not, in mathcomp.algebra.numeric_hierarchy.numfield] (in ring_scope)
x ^+ x [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
x ^+ x [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
x ^- x [not, in mathcomp.algebra.algebraic_hierarchy.divalg] (in ring_scope)
x ^-1 [not, in mathcomp.algebra.algebraic_hierarchy.divalg] (in ring_scope)
x ^:P [not, in mathcomp.algebra.polyXY] (in ring_scope)
x ^:P [not, in mathcomp.algebra.poly] (in ring_scope)
x ^@ [not, in mathcomp.field.algebraics_fundamentals] (in ring_scope)
x ^@ x [not, in mathcomp.solvable.finmodule] (in ring_scope)
x ^@ x [not, in mathcomp.solvable.finmodule] (in ring_scope)
x ^T [not, in mathcomp.algebra.matrix] (in ring_scope)
x ^T [not, in mathcomp.algebra.matrix] (in ring_scope)
x ^\+ [not, in mathcomp.analysis.numfun] (in ring_scope)
x ^\- [not, in mathcomp.analysis.numfun] (in ring_scope)
x ^_|_ [not, in mathcomp.algebra.sesquilinear] (in ring_scope)
x ^` ( x ) [not, in mathcomp.algebra.poly] (in ring_scope)
x ^` ( x ) [not, in mathcomp.algebra.poly] (in ring_scope)
x ^` () [not, in mathcomp.algebra.poly] (in ring_scope)
x ^`N ( x ) [not, in mathcomp.algebra.poly] (in ring_scope)
x ^`N ( x ) [not, in mathcomp.algebra.poly] (in ring_scope)
x ^f [not, in mathcomp.algebra.polydiv] (in ring_scope)
x ^f [not, in mathcomp.algebra.polydiv] (in ring_scope)
x ^f [not, in mathcomp.algebra.poly] (in ring_scope)
x ^f [not, in mathcomp.algebra.poly] (in ring_scope)
x ^f [not, in mathcomp.algebra.poly] (in ring_scope)
x ^f [not, in mathcomp.algebra.poly] (in ring_scope)
x ^f [not, in mathcomp.algebra.poly] (in ring_scope)
x ^f [not, in mathcomp.algebra.mxpoly] (in ring_scope)
x ^f [not, in mathcomp.algebra.mxpoly] (in ring_scope)
x ^f [not, in mathcomp.algebra.mxpoly] (in ring_scope)
x ^f [not, in mathcomp.algebra.mxpoly] (in ring_scope)
x ^f [not, in mathcomp.algebra.mxalgebra] (in ring_scope)
x ^f [not, in mathcomp.algebra.matrix] (in ring_scope)
x ^f [not, in mathcomp.algebra.matrix] (in ring_scope)
x ^f [not, in mathcomp.algebra.matrix] (in ring_scope)
x ^f [not, in mathcomp.algebra.matrix] (in ring_scope)
x ^f [not, in mathcomp.algebra.matrix] (in ring_scope)
x ^f [not, in mathcomp.algebra.matrix] (in ring_scope)
x ^iota [not, in mathcomp.field.fieldext] (in ring_scope)
x `^ x [not, in mathcomp.analysis.exp] (in ring_scope)
x `_ x [not, in mathcomp.boot.nmodule] (in ring_scope)
x `_ x [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in ring_scope)
x ~_ x { in x } [not, in mathcomp.algebra.mxpoly] (in ring_scope)

section_scope

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

seq_scope

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

sesquilinear_scope

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

set_scope

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

signature_scope

x ++> x [not, in mathcomp.classical.unstable] (in signature_scope)
x ==> x [not, in mathcomp.classical.unstable] (in signature_scope)
x ~~> x [not, in mathcomp.classical.unstable] (in signature_scope)

snum_nullity_scope

!=0 [not, in mathcomp.reals.signed] (in snum_nullity_scope)
?=0 [not, in mathcomp.reals.signed] (in snum_nullity_scope)

snum_sign_scope

<=0 [not, in mathcomp.reals.signed] (in snum_sign_scope)
=0 [not, in mathcomp.reals.signed] (in snum_sign_scope)
>=0 [not, in mathcomp.reals.signed] (in snum_sign_scope)
>=<0 [not, in mathcomp.reals.signed] (in snum_sign_scope)
>?<0 [not, in mathcomp.reals.signed] (in snum_sign_scope)

ssr_scope

<hidden > [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_ x [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
'X_ x [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
'exists 'X_ x , x [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
'exists 'X_ x , x [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
'forall 'X_ x , x [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
'forall 'X_ x , x [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
- x [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
- x [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)
~ x [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
~ x [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
x != x [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
x != x [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
x %:R [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
x %:R [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
x %:T [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
x %:T [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
x * x [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
x * x [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
x *+ x [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
x *+ x [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
x + x [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
x + x [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
x - x [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
x - x [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
x / x [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
x / x [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
x /\ x [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
x /\ x [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
x == x [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
x == x [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
x ==> x [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
x ==> x [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
x \/ x [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
x \/ x [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
x ^+ x [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
x ^+ x [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
x ^-1 [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)
x ^-1 [not, in mathcomp.algebra.algebraic_hierarchy.decfield] (in term_scope)

type_scope

'A [ x ]_ ( x ) [not, in mathcomp.algebra.mxalgebra] (in type_scope)
'A [ x ]_ ( x , x ) [not, in mathcomp.algebra.mxalgebra] (in type_scope)
'A [ x ]_ x [not, in mathcomp.algebra.mxalgebra] (in type_scope)
'AEnd ( x ) [not, in mathcomp.field.falgebra] (in type_scope)
'AHom ( x , x ) [not, in mathcomp.field.falgebra] (in type_scope)
'A_ ( x ) [not, in mathcomp.algebra.mxalgebra] (in type_scope)
'A_ ( x , x ) [not, in mathcomp.algebra.mxalgebra] (in type_scope)
'A_ x [not, in mathcomp.algebra.mxalgebra] (in type_scope)
'D^ x [not, in mathcomp.solvable.extraspecial] (in type_scope)
'D^ x * Q [not, in mathcomp.solvable.extraspecial] (in type_scope)
'D_ x [not, in mathcomp.solvable.extremal] (in type_scope)
'End ( x ) [not, in mathcomp.algebra.vector] (in type_scope)
'F_ x [not, in mathcomp.algebra.zmodp] (in type_scope)
'Hom ( x , x ) [not, in mathcomp.algebra.vector] (in type_scope)
'M[ x ]_ ( x ) [not, in mathcomp.algebra.matrix] (in type_scope)
'M[ x ]_ ( x , x ) [not, in mathcomp.algebra.matrix] (in type_scope)
'M[ x ]_ x [not, in mathcomp.algebra.matrix] (in type_scope)
'M_ ( x ) [not, in mathcomp.algebra.matrix] (in type_scope)
'M_ ( x , x ) [not, in mathcomp.algebra.mxalgebra] (in type_scope)
'M_ ( x , x ) [not, in mathcomp.algebra.mxalgebra] (in type_scope)
'M_ ( x , x ) [not, in mathcomp.algebra.mxalgebra] (in type_scope)
'M_ ( x , x ) [not, in mathcomp.algebra.matrix] (in type_scope)
'M_ x [not, in mathcomp.algebra.mxalgebra] (in type_scope)
'M_ x [not, in mathcomp.algebra.mxalgebra] (in type_scope)
'M_ x [not, in mathcomp.algebra.mxalgebra] (in type_scope)
'M_ x [not, in mathcomp.algebra.matrix] (in type_scope)
'Mod_ x [not, in mathcomp.solvable.extremal] (in type_scope)
'Q_ x [not, in mathcomp.solvable.extremal] (in type_scope)
'SD_ x [not, in mathcomp.solvable.extremal] (in type_scope)
'T[ x ]_ ( x , x ) [not, in mathcomp.algebra.tensor] (in type_scope)
'T[ x ]_ [ x , .. , x ; x , .. , x ] [not, in mathcomp.algebra.tensor] (in type_scope)
'T_ ( x , x ) [not, in mathcomp.algebra.tensor] (in type_scope)
'Z_ x [not, in mathcomp.algebra.zmodp] (in type_scope)
'cV[ x ]_ x [not, in mathcomp.algebra.matrix] (in type_scope)
'cV_ x [not, in mathcomp.algebra.matrix] (in type_scope)
'nT[ x ]_ ( x ) [not, in mathcomp.algebra.tensor] (in type_scope)
'nT[ x ]_ [ x , .. , x ] [not, in mathcomp.algebra.tensor] (in type_scope)
'nT_ ( x ) [not, in mathcomp.algebra.tensor] (in type_scope)
'oT[ x ]_ ( x ) [not, in mathcomp.algebra.tensor] (in type_scope)
'oT[ x ]_ [ x , .. , x ] [not, in mathcomp.algebra.tensor] (in type_scope)
'oT_ ( x ) [not, in mathcomp.algebra.tensor] (in type_scope)
'rV[ x ]_ x [not, in mathcomp.algebra.matrix] (in type_scope)
'rV_ x [not, in mathcomp.algebra.matrix] (in type_scope)
'sT [not, in mathcomp.algebra.tensor] (in type_scope)
'sT[ x ] [not, in mathcomp.algebra.tensor] (in type_scope)
@ fun_adjunction x x x x x x [not, in mathcomp.boot.fingraph] (in type_scope)
@ rel_adjunction x x x x x x [not, in mathcomp.boot.fingraph] (in type_scope)
[ lipschitz x | x in x ] [not, in mathcomp.analysis.normedtype_theory.normed_module] (in type_scope)
[ subg x ] [not, in mathcomp.finite_group.fingroup] (in type_scope)
\Forall x .. x , x [not, in mathcomp.classical.contra] (in type_scope)
\bar ^d x [not, in mathcomp.reals.constructive_ereal] (in type_scope)
\bar x [not, in mathcomp.reals.constructive_ereal] (in type_scope)
\forall x & x \near x , x [not, in mathcomp.classical.filter] (in type_scope)
\forall x \ae x , x [not, in mathcomp.analysis.measure_theory.measure_negligible] (in type_scope)
\forall x \near x & x \near x , x [not, in mathcomp.classical.filter] (in type_scope)
\forall x \near x , x [not, in mathcomp.classical.filter] (in type_scope)
\near x & x , x [not, in mathcomp.classical.filter] (in type_scope)
\near x , x [not, in mathcomp.classical.filter] (in type_scope)
{ != x : x } [not, in mathcomp.reals.signed] (in type_scope)
{ != x } [not, in mathcomp.reals.signed] (in type_scope)
{ 'GL_ x ( x ) } [not, in mathcomp.algebra.matrix] (in type_scope)
{ 'GL_ x [ x ] } [not, in mathcomp.algebra.matrix] (in type_scope)
{ < x : x } [not, in mathcomp.reals.signed] (in type_scope)
{ < x } [not, in mathcomp.reals.signed] (in type_scope)
{ <= x : x } [not, in mathcomp.reals.signed] (in type_scope)
{ <= x } [not, in mathcomp.reals.signed] (in type_scope)
{ = x : x } [not, in mathcomp.reals.signed] (in type_scope)
{ = x } [not, in mathcomp.reals.signed] (in type_scope)
{ > x : x } [not, in mathcomp.reals.signed] (in type_scope)
{ > x } [not, in mathcomp.reals.signed] (in type_scope)
{ >< x : x } [not, in mathcomp.reals.signed] (in type_scope)
{ >< x } [not, in mathcomp.reals.signed] (in type_scope)
{ >= x : x } [not, in mathcomp.reals.signed] (in type_scope)
{ >= x } [not, in mathcomp.reals.signed] (in type_scope)
{ >=< x : x } [not, in mathcomp.reals.signed] (in type_scope)
{ >=< x } [not, in mathcomp.reals.signed] (in type_scope)
{ ? x : x | x } [not, in mathcomp.boot.eqtype] (in type_scope)
{ ? x in x | x } [not, in mathcomp.boot.eqtype] (in type_scope)
{ ? x in x } [not, in mathcomp.boot.eqtype] (in type_scope)
{ ? x | x } [not, in mathcomp.boot.eqtype] (in type_scope)
{ ?= x : x } [not, in mathcomp.reals.signed] (in type_scope)
{ ?= x } [not, in mathcomp.reals.signed] (in type_scope)
{ action x &-> x } [not, in mathcomp.finite_group.action] (in type_scope)
{ acts x , on group x | x } [not, in mathcomp.finite_group.action] (in type_scope)
{ acts x , on x | x } [not, in mathcomp.finite_group.action] (in type_scope)
{ additive x -> x } [not, in mathcomp.boot.nmodule] (in type_scope)
{ ae x , x } [not, in mathcomp.analysis.measure_theory.measure_negligible] (in type_scope)
{ aspace x } [not, in mathcomp.field.falgebra] (in type_scope)
{ bij x >-> x } [not, in mathcomp.classical.functions] (in type_scope)
{ blmorphism x -> x } [not, in mathcomp.order.order] (in type_scope)
{ bseq x of x } [not, in mathcomp.boot.tuple] (in type_scope)
{ compare x & x & x } [not, in mathcomp.reals.signed] (in type_scope)
{ dffun x } [not, in mathcomp.boot.finfun] (in type_scope)
{ family x , x --> x } [not, in mathcomp.analysis.topology_theory.function_spaces] (in type_scope)
{ ffun x } [not, in mathcomp.boot.finfun] (in type_scope)
{ fmap x -> x } [not, in mathcomp.finmap.finmap] (in type_scope)
{ fperm x } [not, in mathcomp.finmap.finperm] (in type_scope)
{ fsfun for x } [not, in mathcomp.finmap.finmap] (in type_scope)
{ fsfun of x : x => x } [not, in mathcomp.finmap.finmap] (in type_scope)
{ fsfun of x => x } [not, in mathcomp.finmap.finmap] (in type_scope)
{ fsfun with x } [not, in mathcomp.finmap.finmap] (in type_scope)
{ fsfun x for x } [not, in mathcomp.finmap.finmap] (in type_scope)
{ fsfun x of x => x } [not, in mathcomp.finmap.finmap] (in type_scope)
{ fsfun x with x } [not, in mathcomp.finmap.finmap] (in type_scope)
{ fsfun x } [not, in mathcomp.finmap.finmap] (in type_scope)
{ group x } [not, in mathcomp.finite_group.fingroup] (in type_scope)
{ i01 nat } [not, in mathcomp.algebra.interval_inference] (in type_scope)
{ i01 x } [not, in mathcomp.algebra.interval_inference] (in type_scope)
{ ideal_quot x } [not, in mathcomp.algebra.ring_quotient] (in type_scope)
{ in <= x , x } [not, in mathcomp.classical.wochoice] (in type_scope)
{ in x , isometry x , to x } [not, in mathcomp.algebra.sesquilinear] (in type_scope)
{ inj x >-> x } [not, in mathcomp.classical.functions] (in type_scope)
{ injfun x >-> x } [not, in mathcomp.classical.functions] (in type_scope)
{ inv x >-> x } [not, in mathcomp.classical.functions] (in type_scope)
{ invfun x >-> x } [not, in mathcomp.classical.functions] (in type_scope)
{ itv nat & x } [not, in mathcomp.algebra.interval_inference] (in type_scope)
{ itv x & x } [not, in mathcomp.algebra.interval_inference] (in type_scope)
{ jlmorphism x -> x } [not, in mathcomp.order.order] (in type_scope)
{ linear x -> x | x } [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in type_scope)
{ linear x -> x } [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in type_scope)
{ lmorphism x -> x } [not, in mathcomp.order.order] (in type_scope)
{ lrmorphism x -> x | x } [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in type_scope)
{ lrmorphism x -> x } [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in type_scope)
{ mlmorphism x -> x } [not, in mathcomp.order.order] (in type_scope)
{ morphism x >-> x } [not, in mathcomp.finite_group.morphism] (in type_scope)
{ multiplicative x -> x } [not, in mathcomp.boot.monoid] (in type_scope)
{ near x & x , x } [not, in mathcomp.classical.filter] (in type_scope)
{ near x , x } [not, in mathcomp.classical.filter] (in type_scope)
{ nonneg \bar x } [not, in mathcomp.reals.constructive_ereal] (in type_scope)
{ oinv x >-> x } [not, in mathcomp.classical.functions] (in type_scope)
{ oinvfun x >-> x } [not, in mathcomp.classical.functions] (in type_scope)
{ omorphism x -> x } [not, in mathcomp.order.preorder] (in type_scope)
{ path x from x to x in x } [not, in mathcomp.analysis.homotopy_theory.continuous_path] (in type_scope)
{ path x from x to x } [not, in mathcomp.analysis.homotopy_theory.continuous_path] (in type_scope)
{ perm x } [not, in mathcomp.finite_group.perm] (in type_scope)
{ poly %/ x } [not, in mathcomp.algebra.qpoly] (in type_scope)
{ poly x } [not, in mathcomp.algebra.poly] (in type_scope)
{ posnum \bar x } [not, in mathcomp.reals.constructive_ereal] (in type_scope)
{ posnum nat } [not, in mathcomp.algebra.interval_inference] (in type_scope)
{ ptws x -> x } [not, in mathcomp.analysis.topology_theory.function_spaces] (in type_scope)
{ quot x } [not, in mathcomp.algebra.ring_quotient] (in type_scope)
{ ratio x } [not, in mathcomp.algebra.fraction] (in type_scope)
{ rmorphism x -> x } [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in type_scope)
{ scalar x } [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in type_scope)
{ set x } [not, in mathcomp.boot.finset] (in type_scope)
{ splitbij x >-> x } [not, in mathcomp.classical.functions] (in type_scope)
{ splitinj x >-> x } [not, in mathcomp.classical.functions] (in type_scope)
{ splitinjfun x >-> x } [not, in mathcomp.classical.functions] (in type_scope)
{ splitsurj x >-> x } [not, in mathcomp.classical.functions] (in type_scope)
{ splitsurjfun x >-> x } [not, in mathcomp.classical.functions] (in type_scope)
{ subfield x } [not, in mathcomp.field.fieldext] (in type_scope)
{ subset [ x ] x } [not, in mathcomp.order.preorder] (in type_scope)
{ subset x } [not, in mathcomp.order.preorder] (in type_scope)
{ surj x >-> x } [not, in mathcomp.classical.functions] (in type_scope)
{ surjfun x >-> x } [not, in mathcomp.classical.functions] (in type_scope)
{ tblmorphism x -> x } [not, in mathcomp.order.order] (in type_scope)
{ tlmorphism x -> x } [not, in mathcomp.order.order] (in type_scope)
{ tuple x of x } [not, in mathcomp.boot.tuple] (in type_scope)
{ uniform x -> x } [not, in mathcomp.analysis.topology_theory.function_spaces] (in type_scope)
{ uniform` x -> x } [not, in mathcomp.analysis.topology_theory.function_spaces] (in type_scope)
{ unit x } [not, in mathcomp.algebra.finalg] (in type_scope)
{ vspace x } [not, in mathcomp.algebra.vector] (in type_scope)
{ x in x | x } [not, in mathcomp.boot.eqtype] (in type_scope)
{ x in x } [not, in mathcomp.boot.eqtype] (in type_scope)
{classic x } [not, in mathcomp.classical.boolp] (in type_scope)
{eclassic x } [not, in mathcomp.classical.boolp] (in type_scope)
{fset x } [not, in mathcomp.finmap.finmap] (in type_scope)
{poly_ x x } [not, in mathcomp.algebra.qpoly] (in type_scope)
x %:posnat [not, in mathcomp.algebra.interval_inference] (in type_scope)
x * x [not, in mathcomp.order.preorder] (in type_scope)
x * x [not, in mathcomp.order.preorder] (in type_scope)
x * x [not, in mathcomp.order.preorder] (in type_scope)
x * x [not, in mathcomp.order.preorder] (in type_scope)
x * x [not, in mathcomp.order.preorder] (in type_scope)
x * x [not, in mathcomp.order.preorder] (in type_scope)
x * x [not, in mathcomp.order.preorder] (in type_scope)
x * x [not, in mathcomp.order.preorder] (in type_scope)
x * x [not, in mathcomp.order.preorder] (in type_scope)
x * x [not, in mathcomp.order.preorder] (in type_scope)
x * x [not, in mathcomp.order.order] (in type_scope)
x * x [not, in mathcomp.order.order] (in type_scope)
x * x [not, in mathcomp.order.order] (in type_scope)
x * x [not, in mathcomp.order.order] (in type_scope)
x * x [not, in mathcomp.order.order] (in type_scope)
x * x [not, in mathcomp.order.order] (in type_scope)
x * x [not, in mathcomp.order.order] (in type_scope)
x * x [not, in mathcomp.order.order] (in type_scope)
x * x [not, in mathcomp.order.order] (in type_scope)
x * x [not, in mathcomp.order.order] (in type_scope)
x * x [not, in mathcomp.order.order] (in type_scope)
x * x [not, in mathcomp.order.order] (in type_scope)
x * x [not, in mathcomp.order.order] (in type_scope)
x * x [not, in mathcomp.order.order] (in type_scope)
x * x [not, in mathcomp.order.order] (in type_scope)
x *l x [not, in mathcomp.order.preorder] (in type_scope)
x *lexi[ x ] x [not, in mathcomp.order.preorder] (in type_scope)
x *p x [not, in mathcomp.order.preorder] (in type_scope)
x *prod[ x ] x [not, in mathcomp.order.preorder] (in type_scope)
x .-Lspace x [not, in mathcomp.analysis.hoelder] (in type_scope)
x .-bseq [not, in mathcomp.boot.tuple] (in type_scope)
x .-integrable [not, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integrable] (in type_scope)
x .-lipschitz x [not, in mathcomp.analysis.normedtype_theory.normed_module] (in type_scope)
x .-lipschitz_ x x [not, in mathcomp.analysis.normedtype_theory.normed_module] (in type_scope)
x .-lipschitz_on x [not, in mathcomp.analysis.normedtype_theory.normed_module] (in type_scope)
x .-negligible [not, in mathcomp.analysis.measure_theory.measure_negligible] (in type_scope)
x .-tuple [not, in mathcomp.order.preorder] (in type_scope)
x .-tuple [not, in mathcomp.order.preorder] (in type_scope)
x .-tuple [not, in mathcomp.order.order] (in type_scope)
x .-tuple [not, in mathcomp.order.order] (in type_scope)
x .-tuple [not, in mathcomp.boot.tuple] (in type_scope)
x .-tuplelexi [not, in mathcomp.order.preorder] (in type_scope)
x .-tuplelexi[ x ] [not, in mathcomp.order.preorder] (in type_scope)
x .-tupleprod [not, in mathcomp.order.preorder] (in type_scope)
x .-tupleprod[ x ] [not, in mathcomp.order.preorder] (in type_scope)
x <<=> x [not, in mathcomp.classical.functions] (in type_scope)
x <<~ x [not, in mathcomp.classical.functions] (in type_scope)
x <<~> x [not, in mathcomp.classical.functions] (in type_scope)
x <=> x [not, in mathcomp.classical.functions] (in type_scope)
x <~ x [not, in mathcomp.classical.functions] (in type_scope)
x <~> x [not, in mathcomp.classical.functions] (in type_scope)
x ==>> x [not, in mathcomp.classical.functions] (in type_scope)
x =>> x [not, in mathcomp.classical.functions] (in type_scope)
x >=> x [not, in mathcomp.classical.functions] (in type_scope)
x >>=> x [not, in mathcomp.classical.functions] (in type_scope)
x >>~> x [not, in mathcomp.classical.functions] (in type_scope)
x >~> x [not, in mathcomp.classical.functions] (in type_scope)
x ^ x [not, in mathcomp.boot.finfun] (in type_scope)
x ^c [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in type_scope)
x ^c [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in type_scope)
x ^d [not, in mathcomp.order.preorder] (in type_scope)
x ^nat [not, in mathcomp.analysis.sequences] (in type_scope)
x ^o [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in type_scope)
x ^o [not, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras] (in type_scope)
x ^z [not, in mathcomp.algebra.ssrint] (in type_scope)
x ^{1+2* x } [not, in mathcomp.solvable.extraspecial] (in type_scope)
x ^{1+2} [not, in mathcomp.solvable.extraspecial] (in type_scope)
x ~> x [not, in mathcomp.classical.functions] (in type_scope)
x ~>> x [not, in mathcomp.classical.functions] (in type_scope)
x ~~>> x [not, in mathcomp.classical.functions] (in type_scope)

unity_root_scope

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

vspace_scope

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