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 (24947 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 (1496 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 (216 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 (3586 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 (84 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 (11878 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 (389 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 (49 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 (119 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 (272 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 (1128 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 (701 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 (4837 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 (192 entries)

O (definition)

ocancel [in mathcomp.ssreflect.ssrfun]
odd [in mathcomp.ssreflect.ssrnat]
odd_perm [in mathcomp.fingroup.perm]
of_irr [in mathcomp.character.vcharacter]
ohead [in mathcomp.ssreflect.seq]
Ohm [in mathcomp.solvable.abelian]
Ohm_mgFun [in mathcomp.solvable.abelian]
Ohm_gFun [in mathcomp.solvable.abelian]
Ohm_igFun [in mathcomp.solvable.abelian]
Ohm_group [in mathcomp.solvable.abelian]
oneg [in mathcomp.fingroup.fingroup]
oneq [in mathcomp.algebra.rat]
one_group [in mathcomp.fingroup.fingroup]
onPhantom [in mathcomp.ssreflect.ssrbool]
opair_of_sum [in mathcomp.ssreflect.choice]
oppmx [in mathcomp.algebra.matrix]
opppT [in mathcomp.field.closed_field]
oppq [in mathcomp.algebra.rat]
oppq_subdef [in mathcomp.algebra.rat]
oppz_add [in mathcomp.algebra.ssrint]
opp_pair [in mathcomp.algebra.ssralg]
opp_lfun [in mathcomp.algebra.vector]
opp_poly_unlockable [in mathcomp.algebra.poly]
opp_poly [in mathcomp.algebra.poly]
opp_poly_def [in mathcomp.algebra.poly]
option_countType [in mathcomp.ssreflect.choice]
option_countMixin [in mathcomp.ssreflect.choice]
option_choiceType [in mathcomp.ssreflect.choice]
option_choiceMixin [in mathcomp.ssreflect.choice]
option_finType [in mathcomp.ssreflect.fintype]
option_finMixin [in mathcomp.ssreflect.fintype]
option_enum [in mathcomp.ssreflect.fintype]
option_eqType [in mathcomp.ssreflect.eqtype]
option_eqMixin [in mathcomp.ssreflect.eqtype]
Option.apply [in mathcomp.ssreflect.ssrfun]
Option.bind [in mathcomp.ssreflect.ssrfun]
Option.default [in mathcomp.ssreflect.ssrfun]
Option.map [in mathcomp.ssreflect.ssrfun]
opt_eq [in mathcomp.ssreflect.eqtype]
orbit [in mathcomp.fingroup.action]
orbit [in mathcomp.ssreflect.fingraph]
orbit_transversal [in mathcomp.fingroup.action]
orb_addoid [in mathcomp.ssreflect.bigop]
orb_muloid [in mathcomp.ssreflect.bigop]
orb_comoid [in mathcomp.ssreflect.bigop]
orb_monoid [in mathcomp.ssreflect.bigop]
order [in mathcomp.fingroup.fingroup]
order [in mathcomp.ssreflect.fingraph]
orderC [in mathcomp.field.algnum]
order_set [in mathcomp.ssreflect.fingraph]
ordinal_subFinType [in mathcomp.ssreflect.fintype]
ordinal_finType [in mathcomp.ssreflect.fintype]
ordinal_finMixin [in mathcomp.ssreflect.fintype]
ordinal_subCountType [in mathcomp.ssreflect.fintype]
ordinal_countType [in mathcomp.ssreflect.fintype]
ordinal_countMixin [in mathcomp.ssreflect.fintype]
ordinal_choiceType [in mathcomp.ssreflect.fintype]
ordinal_choiceMixin [in mathcomp.ssreflect.fintype]
ordinal_eqType [in mathcomp.ssreflect.fintype]
ordinal_eqMixin [in mathcomp.ssreflect.fintype]
ordinal_subType [in mathcomp.ssreflect.fintype]
ord_tuple [in mathcomp.ssreflect.tuple]
ord_max [in mathcomp.ssreflect.fintype]
ord_enum [in mathcomp.ssreflect.fintype]
ord0 [in mathcomp.ssreflect.fintype]
orthogonal [in mathcomp.character.classfun]
orthonormal [in mathcomp.character.classfun]
ortho_rec [in mathcomp.character.classfun]



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 (24947 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 (1496 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 (216 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 (3586 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 (84 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 (11878 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 (389 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 (49 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 (119 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 (272 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 (1128 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 (701 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 (4837 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 (192 entries)