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 (76754 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 (1892 entries)
Binder 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 (49588 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 (305 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 (4034 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 (94 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 (14802 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 (222 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 (9 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 (131 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 (43 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 (1392 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 (1140 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 (3066 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 (36 entries)

O (binder)

offset:108 [in mathcomp.ssreflect.div]
offset:89 [in mathcomp.ssreflect.div]
ofs:1976 [in mathcomp.algebra.ssralg]
oi:22 [in mathcomp.ssreflect.ssrAC]
ok_proj:1993 [in mathcomp.algebra.ssralg]
omorphI_subproof:3167 [in mathcomp.ssreflect.order]
omorphI_subproof:3127 [in mathcomp.ssreflect.order]
omorphU_subproof:3168 [in mathcomp.ssreflect.order]
omorphU_subproof:3138 [in mathcomp.ssreflect.order]
omorph_le_subproof:3071 [in mathcomp.ssreflect.order]
omorph0_subproof:3213 [in mathcomp.ssreflect.order]
omorph1_subproof:3224 [in mathcomp.ssreflect.order]
oneg_subdef:3 [in mathcomp.fingroup.fingroup]
oneg:26 [in mathcomp.fingroup.fingroup]
oner_neq0:1278 [in mathcomp.algebra.ssralg]
oner_neq0:1224 [in mathcomp.algebra.ssralg]
oner_neq0:537 [in mathcomp.algebra.ssralg]
oner_neq0:518 [in mathcomp.algebra.ssralg]
oner_neq0:239 [in mathcomp.algebra.ssralg]
oner_neq0:220 [in mathcomp.algebra.ssralg]
oneT:116 [in mathcomp.algebra.ring_quotient]
oneT:46 [in mathcomp.algebra.ring_quotient]
oneT:68 [in mathcomp.algebra.ring_quotient]
oneT:90 [in mathcomp.algebra.ring_quotient]
one:1217 [in mathcomp.algebra.ssralg]
one:1272 [in mathcomp.algebra.ssralg]
one:211 [in mathcomp.algebra.ssralg]
one:227 [in mathcomp.algebra.ssralg]
one:511 [in mathcomp.algebra.ssralg]
one:526 [in mathcomp.algebra.ssralg]
one:921 [in mathcomp.ssreflect.finset]
opA:19 [in mathcomp.ssreflect.bigop]
opA:3 [in mathcomp.ssreflect.bigop]
opA:45 [in mathcomp.ssreflect.bigop]
opA:64 [in mathcomp.ssreflect.bigop]
opC:11 [in mathcomp.ssreflect.bigop]
opC:20 [in mathcomp.ssreflect.bigop]
opC:65 [in mathcomp.ssreflect.bigop]
opm1:34 [in mathcomp.ssreflect.bigop]
opm1:47 [in mathcomp.ssreflect.bigop]
opm:975 [in mathcomp.algebra.matrix]
opm:976 [in mathcomp.algebra.matrix]
opm:977 [in mathcomp.algebra.matrix]
opm:978 [in mathcomp.algebra.matrix]
opm:979 [in mathcomp.algebra.matrix]
opm:980 [in mathcomp.algebra.matrix]
opm:981 [in mathcomp.algebra.matrix]
opm:982 [in mathcomp.algebra.matrix]
opm:983 [in mathcomp.algebra.matrix]
oppT:114 [in mathcomp.algebra.ring_quotient]
oppT:25 [in mathcomp.algebra.ring_quotient]
oppT:4 [in mathcomp.algebra.ring_quotient]
oppT:44 [in mathcomp.algebra.ring_quotient]
oppT:66 [in mathcomp.algebra.ring_quotient]
oppT:88 [in mathcomp.algebra.ring_quotient]
opp:105 [in mathcomp.algebra.ssralg]
opp:524 [in mathcomp.algebra.ssralg]
opp:98 [in mathcomp.algebra.ssralg]
opredI_subproof:3862 [in mathcomp.ssreflect.order]
opredI_subproof:3806 [in mathcomp.ssreflect.order]
opredI_subproof:3719 [in mathcomp.ssreflect.order]
opredI_subproof:3633 [in mathcomp.ssreflect.order]
opredI_subproof:3599 [in mathcomp.ssreflect.order]
opredI:3284 [in mathcomp.ssreflect.order]
opredI:3344 [in mathcomp.ssreflect.order]
opredI:3358 [in mathcomp.ssreflect.order]
opredU_subproof:3863 [in mathcomp.ssreflect.order]
opredU_subproof:3807 [in mathcomp.ssreflect.order]
opredU_subproof:3720 [in mathcomp.ssreflect.order]
opredU_subproof:3634 [in mathcomp.ssreflect.order]
opredU_subproof:3600 [in mathcomp.ssreflect.order]
opredU:3291 [in mathcomp.ssreflect.order]
opredU:3345 [in mathcomp.ssreflect.order]
opredU:3359 [in mathcomp.ssreflect.order]
opred0_subproof:3864 [in mathcomp.ssreflect.order]
opred0_subproof:3840 [in mathcomp.ssreflect.order]
opred0_subproof:3721 [in mathcomp.ssreflect.order]
opred0_subproof:3695 [in mathcomp.ssreflect.order]
opred0:3298 [in mathcomp.ssreflect.order]
opred0:3360 [in mathcomp.ssreflect.order]
opred1_subproof:3865 [in mathcomp.ssreflect.order]
opred1_subproof:3841 [in mathcomp.ssreflect.order]
opred1_subproof:3808 [in mathcomp.ssreflect.order]
opred1_subproof:3782 [in mathcomp.ssreflect.order]
opred1:3305 [in mathcomp.ssreflect.order]
opred1:3361 [in mathcomp.ssreflect.order]
op_additive_subproof:1016 [in mathcomp.algebra.ssralg]
op':535 [in mathcomp.ssreflect.ssrnat]
op1m:33 [in mathcomp.ssreflect.bigop]
op1m:46 [in mathcomp.ssreflect.bigop]
op1m:66 [in mathcomp.ssreflect.bigop]
op:10 [in mathcomp.ssreflect.bigop]
op:1013 [in mathcomp.algebra.ssralg]
op:1022 [in mathcomp.algebra.ssralg]
op:1024 [in mathcomp.ssreflect.bigop]
op:15 [in mathcomp.ssreflect.bigop]
op:170 [in mathcomp.character.inertia]
op:18 [in mathcomp.ssreflect.bigop]
op:195 [in mathcomp.algebra.ssrnum]
op:2 [in mathcomp.ssreflect.bigop]
op:24 [in mathcomp.ssreflect.bigop]
op:2743 [in mathcomp.ssreflect.bigop]
op:28 [in mathcomp.algebra.zmodp]
op:293 [in mathcomp.ssreflect.bigop]
op:32 [in mathcomp.ssreflect.bigop]
op:35 [in mathcomp.algebra.zmodp]
op:40 [in mathcomp.ssreflect.bigop]
op:44 [in mathcomp.ssreflect.bigop]
op:476 [in mathcomp.character.character]
op:501 [in mathcomp.ssreflect.ssrnat]
op:522 [in mathcomp.ssreflect.ssrnat]
op:53 [in mathcomp.ssreflect.bigop]
op:534 [in mathcomp.ssreflect.ssrnat]
op:59 [in mathcomp.ssreflect.bigop]
op:63 [in mathcomp.ssreflect.bigop]
op:7 [in mathcomp.ssreflect.bigop]
op:72 [in mathcomp.ssreflect.bigop]
op:721 [in mathcomp.character.classfun]
op:822 [in mathcomp.ssreflect.order]
op:835 [in mathcomp.ssreflect.order]
op:90 [in mathcomp.ssreflect.bigop]
op:99 [in mathcomp.ssreflect.ssrAC]
ord:769 [in mathcomp.ssreflect.fintype]
ord:778 [in mathcomp.ssreflect.fintype]
ord:788 [in mathcomp.ssreflect.fintype]
ord:800 [in mathcomp.ssreflect.fintype]



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 (76754 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 (1892 entries)
Binder 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 (49588 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 (305 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 (4034 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 (94 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 (14802 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 (222 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 (9 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 (131 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 (43 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 (1392 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 (1140 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 (3066 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 (36 entries)