| 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) | -
O (lemma)
-oddb [in mathcomp.ssreflect.ssrnat]-oddSg [in mathcomp.solvable.pgroup]
-odd_pgroup_odd [in mathcomp.solvable.pgroup]
-odd_lift_perm [in mathcomp.fingroup.perm]
-odd_permJ [in mathcomp.fingroup.perm]
-odd_permV [in mathcomp.fingroup.perm]
-odd_permM [in mathcomp.fingroup.perm]
-odd_perm_prod [in mathcomp.fingroup.perm]
-odd_tperm [in mathcomp.fingroup.perm]
-odd_mul_tperm [in mathcomp.fingroup.perm]
-odd_perm1 [in mathcomp.fingroup.perm]
-odd_2'nat [in mathcomp.ssreflect.prime]
-odd_prime_gt2 [in mathcomp.ssreflect.prime]
-odd_mod [in mathcomp.ssreflect.div]
-odd_pgroup_rank1_cyclic [in mathcomp.solvable.extremal]
-odd_not_extremal2 [in mathcomp.solvable.extremal]
-odd_gt2 [in mathcomp.ssreflect.ssrnat]
-odd_gt0 [in mathcomp.ssreflect.ssrnat]
-odd_ltn [in mathcomp.ssreflect.ssrnat]
-odd_geq [in mathcomp.ssreflect.ssrnat]
-odd_double_half [in mathcomp.ssreflect.ssrnat]
-odd_double [in mathcomp.ssreflect.ssrnat]
-odd_exp [in mathcomp.ssreflect.ssrnat]
-odd_mul [in mathcomp.ssreflect.ssrnat]
-odd_opp [in mathcomp.ssreflect.ssrnat]
-odd_sub [in mathcomp.ssreflect.ssrnat]
-odd_add [in mathcomp.ssreflect.ssrnat]
-of_irrK [in mathcomp.character.vcharacter]
-OhmE [in mathcomp.solvable.abelian]
-OhmEabelian [in mathcomp.solvable.abelian]
-OhmJ [in mathcomp.solvable.abelian]
-OhmPredP [in mathcomp.solvable.abelian]
-OhmS [in mathcomp.solvable.abelian]
-Ohm_Mho_homocyclic [in mathcomp.solvable.abelian]
-Ohm_leq [in mathcomp.solvable.abelian]
-Ohm_normal [in mathcomp.solvable.abelian]
-Ohm_char [in mathcomp.solvable.abelian]
-Ohm_dprod [in mathcomp.solvable.abelian]
-Ohm_p_cycle [in mathcomp.solvable.abelian]
-Ohm_cont [in mathcomp.solvable.abelian]
-Ohm_id [in mathcomp.solvable.abelian]
-Ohm_sub [in mathcomp.solvable.abelian]
-Ohm0 [in mathcomp.solvable.abelian]
-Ohm1 [in mathcomp.solvable.abelian]
-Ohm1Eexponent [in mathcomp.solvable.abelian]
-Ohm1Eprime [in mathcomp.solvable.abelian]
-Ohm1_extraspecial_odd [in mathcomp.solvable.extraspecial]
-Ohm1_homocyclicP [in mathcomp.solvable.abelian]
-Ohm1_cyclic_pgroup_prime [in mathcomp.solvable.abelian]
-Ohm1_cent_max [in mathcomp.solvable.abelian]
-Ohm1_eq1 [in mathcomp.solvable.abelian]
-Ohm1_id [in mathcomp.solvable.abelian]
-Ohm1_abelem [in mathcomp.solvable.abelian]
-Ohm1_cent_max_normal_abelem [in mathcomp.solvable.maximal]
-Ohm1_stab_Ohm1_SCN_series [in mathcomp.solvable.maximal]
-on_card_preimset [in mathcomp.ssreflect.finset]
-opair_of_sumK [in mathcomp.ssreflect.choice]
-oppmx_key [in mathcomp.algebra.matrix]
-oppq_frac [in mathcomp.algebra.rat]
-oppr_itvcc [in mathcomp.algebra.interval]
-oppr_itvoc [in mathcomp.algebra.interval]
-oppr_itvco [in mathcomp.algebra.interval]
-oppr_itvoo [in mathcomp.algebra.interval]
-oppr_itv [in mathcomp.algebra.interval]
-opp_lfunE [in mathcomp.algebra.vector]
-opp_block_mx [in mathcomp.algebra.matrix]
-opp_col_mx [in mathcomp.algebra.matrix]
-opp_row_mx [in mathcomp.algebra.matrix]
-opp_isometry [in mathcomp.character.classfun]
-opp_poly_key [in mathcomp.algebra.poly]
-option_enumP [in mathcomp.ssreflect.fintype]
-opt_eqP [in mathcomp.ssreflect.eqtype]
-op_Wedderburn_id [in mathcomp.character.mxrepresentation]
-orbitE [in mathcomp.fingroup.action]
-orbitJ [in mathcomp.fingroup.action]
-orbitJs [in mathcomp.fingroup.action]
-orbitP [in mathcomp.fingroup.action]
-orbitR [in mathcomp.fingroup.action]
-orbitRs [in mathcomp.fingroup.action]
-orbit_morphim_actperm [in mathcomp.fingroup.action]
-orbit_conjsg [in mathcomp.fingroup.action]
-orbit_rcoset [in mathcomp.fingroup.action]
-orbit_lcoset [in mathcomp.fingroup.action]
-orbit_inv [in mathcomp.fingroup.action]
-orbit_eq_mem [in mathcomp.fingroup.action]
-orbit_actr [in mathcomp.fingroup.action]
-orbit_act [in mathcomp.fingroup.action]
-orbit_transl [in mathcomp.fingroup.action]
-orbit_eqP [in mathcomp.fingroup.action]
-orbit_trans [in mathcomp.fingroup.action]
-orbit_sym [in mathcomp.fingroup.action]
-orbit_stabilizer [in mathcomp.fingroup.action]
-orbit_transversalP [in mathcomp.fingroup.action]
-orbit_partition [in mathcomp.fingroup.action]
-orbit_conjsg_in [in mathcomp.fingroup.action]
-orbit_rcoset_in [in mathcomp.fingroup.action]
-orbit_lcoset_in [in mathcomp.fingroup.action]
-orbit_inv_in [in mathcomp.fingroup.action]
-orbit_actr_in [in mathcomp.fingroup.action]
-orbit_act_in [in mathcomp.fingroup.action]
-orbit_in_transl [in mathcomp.fingroup.action]
-orbit_in_eqP [in mathcomp.fingroup.action]
-orbit_in_trans [in mathcomp.fingroup.action]
-orbit_in_sym [in mathcomp.fingroup.action]
-orbit_refl [in mathcomp.fingroup.action]
-orbit_id [in mathcomp.ssreflect.fingraph]
-orbit_rot_cycle [in mathcomp.ssreflect.fingraph]
-orbit_uniq [in mathcomp.ssreflect.fingraph]
-orbit1P [in mathcomp.fingroup.action]
-orderE [in mathcomp.fingroup.fingroup]
-orderJ [in mathcomp.fingroup.fingroup]
-orderM [in mathcomp.solvable.cyclic]
-orderSpred [in mathcomp.ssreflect.fingraph]
-orderV [in mathcomp.fingroup.fingroup]
-orderXdiv [in mathcomp.solvable.cyclic]
-orderXdvd [in mathcomp.solvable.cyclic]
-orderXexp [in mathcomp.solvable.cyclic]
-orderXgcd [in mathcomp.solvable.cyclic]
-orderXpfactor [in mathcomp.solvable.cyclic]
-orderXpnat [in mathcomp.solvable.cyclic]
-orderXprime [in mathcomp.solvable.cyclic]
-order_constt [in mathcomp.solvable.pgroup]
-order_path_min [in mathcomp.ssreflect.path]
-order_primeChar [in mathcomp.field.finfield]
-order_injm [in mathcomp.fingroup.morphism]
-order_gt1 [in mathcomp.fingroup.fingroup]
-order_eq1 [in mathcomp.fingroup.fingroup]
-order_gt0 [in mathcomp.fingroup.fingroup]
-order_set_finv [in mathcomp.ssreflect.fingraph]
-order_finv [in mathcomp.ssreflect.fingraph]
-order_id [in mathcomp.ssreflect.fingraph]
-order_cycle [in mathcomp.ssreflect.fingraph]
-order_Zp1 [in mathcomp.algebra.zmodp]
-order_inj_cyclic [in mathcomp.solvable.cyclic]
-order_dvdG [in mathcomp.solvable.cyclic]
-order_inf [in mathcomp.solvable.cyclic]
-order_dvdn [in mathcomp.solvable.cyclic]
-order1 [in mathcomp.fingroup.fingroup]
-ord_enum_uniq [in mathcomp.ssreflect.fintype]
-ord_inj [in mathcomp.ssreflect.fintype]
-ord_enum4 [in mathcomp.solvable.burnside_app]
-ord1 [in mathcomp.algebra.zmodp]
-orthogonalP [in mathcomp.character.classfun]
-orthogonal_span [in mathcomp.character.vcharacter]
-orthogonal_free [in mathcomp.character.classfun]
-orthogonal_oppl [in mathcomp.character.classfun]
-orthogonal_oppr [in mathcomp.character.classfun]
-orthogonal_split [in mathcomp.character.classfun]
-orthogonal_catr [in mathcomp.character.classfun]
-orthogonal_catl [in mathcomp.character.classfun]
-orthogonal_sym [in mathcomp.character.classfun]
-orthogonal_cons [in mathcomp.character.classfun]
-orthonormalE [in mathcomp.character.classfun]
-orthonormalP [in mathcomp.character.classfun]
-orthonormal_span [in mathcomp.character.vcharacter]
-orthonormal_free [in mathcomp.character.classfun]
-orthonormal_cat [in mathcomp.character.classfun]
-orthonormal_orthogonal [in mathcomp.character.classfun]
-orthonormal_not0 [in mathcomp.character.classfun]
-orthonormal2P [in mathcomp.character.classfun]
-orthoP [in mathcomp.character.classfun]
-orthoPl [in mathcomp.character.classfun]
-orthoPr [in mathcomp.character.classfun]
-out_perm [in mathcomp.fingroup.perm]
-out_Aut [in mathcomp.fingroup.automorphism]
-
| 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) | -