| Global Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(23836 entries) | -
| Notation Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(1409 entries) | -
| Module Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(221 entries) | -
| Variable Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(3574 entries) | -
| Library Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(90 entries) | -
| Lemma Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(12096 entries) | -
| Constructor Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(368 entries) | -
| Axiom Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(45 entries) | -
| Inductive Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(107 entries) | -
| Projection Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(273 entries) | -
| Section Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(1140 entries) | -
| Abbreviation Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(728 entries) | -
| Definition Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(3596 entries) | -
| Record Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(189 entries) | -
N (notation)
-_ .*2 (nat_scope) [in mathcomp.ssreflect.ssrnat]-_ ^ _ (nat_scope) [in mathcomp.ssreflect.ssrnat]
-_ * _ (nat_scope) [in mathcomp.ssreflect.ssrnat]
-_ + _ (nat_scope) [in mathcomp.ssreflect.ssrnat]
-[ archiFieldType of _ ] (form_scope) [in mathcomp.algebra.ssrnum]
-[ archiFieldType of _ for _ ] (form_scope) [in mathcomp.algebra.ssrnum]
-[ numClosedFieldType of _ ] (form_scope) [in mathcomp.algebra.ssrnum]
-[ numClosedFieldType of _ for _ ] (form_scope) [in mathcomp.algebra.ssrnum]
-_ < _ (ring_scope) [in mathcomp.algebra.ssrnum]
-_ <= _ (ring_scope) [in mathcomp.algebra.ssrnum]
-[ numDomainType of _ ] (form_scope) [in mathcomp.algebra.ssrnum]
-[ numDomainType of _ for _ ] (form_scope) [in mathcomp.algebra.ssrnum]
-[ numFieldType of _ ] (form_scope) [in mathcomp.algebra.ssrnum]
-[ rcfType of _ ] (form_scope) [in mathcomp.algebra.ssrnum]
-[ rcfType of _ for _ ] (form_scope) [in mathcomp.algebra.ssrnum]
-[ realDomainType of _ ] (form_scope) [in mathcomp.algebra.ssrnum]
-[ realDomainType of _ for _ ] (form_scope) [in mathcomp.algebra.ssrnum]
-[ realFieldType of _ ] (form_scope) [in mathcomp.algebra.ssrnum]
-`| _ | (ring_scope) [in mathcomp.algebra.ssrnum]
-_ < _ [in mathcomp.algebra.ssrnum]
-_ <= _ [in mathcomp.algebra.ssrnum]
-_ <= _ ?= iff _ :> _ (ring_scope) [in mathcomp.algebra.ssrnum]
-_ <= _ ?= iff _ (ring_scope) [in mathcomp.algebra.ssrnum]
-_ < _ < _ (ring_scope) [in mathcomp.algebra.ssrnum]
-_ <= _ < _ (ring_scope) [in mathcomp.algebra.ssrnum]
-_ < _ <= _ (ring_scope) [in mathcomp.algebra.ssrnum]
-_ <= _ <= _ (ring_scope) [in mathcomp.algebra.ssrnum]
-_ >= _ :> _ (ring_scope) [in mathcomp.algebra.ssrnum]
-_ >= _ (ring_scope) [in mathcomp.algebra.ssrnum]
-_ <= _ :> _ (ring_scope) [in mathcomp.algebra.ssrnum]
-_ <= _ (ring_scope) [in mathcomp.algebra.ssrnum]
-_ > _ :> _ (ring_scope) [in mathcomp.algebra.ssrnum]
-_ > _ (ring_scope) [in mathcomp.algebra.ssrnum]
-_ < _ :> _ (ring_scope) [in mathcomp.algebra.ssrnum]
-_ < _ (ring_scope) [in mathcomp.algebra.ssrnum]
->= _ :> _ (ring_scope) [in mathcomp.algebra.ssrnum]
->= _ (ring_scope) [in mathcomp.algebra.ssrnum]
-<= _ :> _ (ring_scope) [in mathcomp.algebra.ssrnum]
-<= _ (ring_scope) [in mathcomp.algebra.ssrnum]
-> _ :> _ (ring_scope) [in mathcomp.algebra.ssrnum]
-> _ (ring_scope) [in mathcomp.algebra.ssrnum]
-< _ :> _ (ring_scope) [in mathcomp.algebra.ssrnum]
-< _ (ring_scope) [in mathcomp.algebra.ssrnum]
-=%R (ring_scope) [in mathcomp.algebra.ssrnum]
->=%R (ring_scope) [in mathcomp.algebra.ssrnum]
-<=%R (ring_scope) [in mathcomp.algebra.ssrnum]
->%R (ring_scope) [in mathcomp.algebra.ssrnum]
-<%R (ring_scope) [in mathcomp.algebra.ssrnum]
-`| _ | (ring_scope) [in mathcomp.algebra.ssrnum]
-'Im _ (ring_scope) [in mathcomp.algebra.ssrnum]
-'Re _ (ring_scope) [in mathcomp.algebra.ssrnum]
-_ .-root (ring_scope) [in mathcomp.algebra.ssrnum]
-_ .-root (ring_core_scope) [in mathcomp.algebra.ssrnum]
-[ arg maxr_ ( _ > _ ) _ ] (form_scope) [in mathcomp.algebra.ssrnum]
-[ arg maxr_ ( _ > _ in _ ) _ ] (form_scope) [in mathcomp.algebra.ssrnum]
-[ arg maxr_ ( _ > _ | _ ) _ ] (form_scope) [in mathcomp.algebra.ssrnum]
-[ arg minr_ ( _ < _ ) _ ] (form_scope) [in mathcomp.algebra.ssrnum]
-[ arg minr_ ( _ < _ in _ ) _ ] (form_scope) [in mathcomp.algebra.ssrnum]
-[ arg minr_ ( _ < _ | _ ) _ ] (form_scope) [in mathcomp.algebra.ssrnum]
-'Im _ (ring_scope) [in mathcomp.algebra.ssrnum]
-'Re _ (ring_scope) [in mathcomp.algebra.ssrnum]
-'i (ring_scope) [in mathcomp.algebra.ssrnum]
-_ .-root (ring_scope) [in mathcomp.algebra.ssrnum]
-'i (ring_scope) [in mathcomp.algebra.ssrnum]
-_ ^* (ring_scope) [in mathcomp.algebra.ssrnum]
-
| Global Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(23836 entries) | -
| Notation Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(1409 entries) | -
| Module Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(221 entries) | -
| Variable Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(3574 entries) | -
| Library Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(90 entries) | -
| Lemma Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(12096 entries) | -
| Constructor Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(368 entries) | -
| Axiom Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(45 entries) | -
| Inductive Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(107 entries) | -
| Projection Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(273 entries) | -
| Section Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(1140 entries) | -
| Abbreviation Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(728 entries) | -
| Definition Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(3596 entries) | -
| Record Index | -A | -B | -C | -D | -E | -F | -G | -H | -I | -J | -K | -L | -M | -N | -O | -P | -Q | -R | -S | -T | -U | -V | -W | -X | -Y | -Z | -_ | -other | -(189 entries) | -