| 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) | -
C (notation)
-_ ^f (ring_scope) [in mathcomp.character.mxrepresentation]-_ ^f (ring_scope) [in mathcomp.character.mxrepresentation]
-_ \char _ [in mathcomp.fingroup.automorphism]
-[ choiceType of _ ] (form_scope) [in mathcomp.ssreflect.choice]
-[ choiceType of _ for _ ] (form_scope) [in mathcomp.ssreflect.choice]
-'1_ _ [in mathcomp.character.classfun]
-_ ->_ _ _ [in mathcomp.field.closed_field]
-'if _ then _ else _ [in mathcomp.field.closed_field]
-'let _ <- _ ; _ [in mathcomp.field.closed_field]
-<< _ ; _ >> (vspace_scope) [in mathcomp.field.falgebra]
-<< _ & _ >> (vspace_scope) [in mathcomp.field.falgebra]
-[ rec _ , _ , _ ] [in mathcomp.ssreflect.choice]
-` T (group_scope) [in mathcomp.character.inertia]
-_ / _ (Group_scope) [in mathcomp.fingroup.quotient]
-_ %% B (cfun_scope) [in mathcomp.character.classfun]
-_ / B (cfun_scope) [in mathcomp.character.classfun]
-[ countType of _ ] (form_scope) [in mathcomp.ssreflect.choice]
-[ countType of _ for _ ] (form_scope) [in mathcomp.ssreflect.choice]
-[ countClosedFieldType of _ ] (form_scope) [in mathcomp.algebra.countalg]
-[ countComRingType of _ ] (form_scope) [in mathcomp.algebra.countalg]
-[ countComUnitRingType of _ ] (form_scope) [in mathcomp.algebra.countalg]
-[ countDecFieldType of _ ] (form_scope) [in mathcomp.algebra.countalg]
-[ countFieldType of _ ] (form_scope) [in mathcomp.algebra.countalg]
-[ countIdomainType of _ ] (form_scope) [in mathcomp.algebra.countalg]
-[ countRingType of _ ] (form_scope) [in mathcomp.algebra.countalg]
-[ countUnitRingType of _ ] (form_scope) [in mathcomp.algebra.countalg]
-[ countZmodType of _ ] (form_scope) [in mathcomp.algebra.countalg]
-