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 | (14626 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 | (165 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 | (112 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 | (7292 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 | (761 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 | (250 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 | (390 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 | (84 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 | (3144 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 | (126 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 | (28 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 | (2221 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 | (53 entries) |

## O

oapp [abbreviation, in ssrfun]obind [abbreviation, in ssrfun]

ocancel [definition, in ssrfun]

odd [definition, in ssrnat]

oddb [lemma, in ssrnat]

oddSg [lemma, in pgroup]

odd_perm [definition, in perm]

odd_mul [lemma, in ssrnat]

odd_permM [lemma, in perm]

odd_opp [lemma, in ssrnat]

odd_double_half [lemma, in ssrnat]

odd_pgroup_odd [lemma, in pgroup]

odd_sub [lemma, in ssrnat]

odd_add [lemma, in ssrnat]

odd_mul_tperm [lemma, in perm]

odd_tperm [lemma, in perm]

odd_double [lemma, in ssrnat]

odd_permV [lemma, in perm]

odd_exp [lemma, in ssrnat]

odd_not_extremal2 [lemma, in extremal]

odd_pgroup_rank1_cyclic [lemma, in extremal]

odd_2'nat [lemma, in prime]

odd_mod [lemma, in div]

odd_perm_prod [lemma, in perm]

odd_lift_perm [lemma, in perm]

odd_permJ [lemma, in perm]

odd_perm1 [lemma, in perm]

odflt [abbreviation, in ssrfun]

ohead [definition, in seq]

Ohm [definition, in abelian]

OhmE [lemma, in abelian]

OhmEabelian [lemma, in abelian]

OhmJ [lemma, in abelian]

OhmPredP [lemma, in abelian]

OhmProps [section, in abelian]

OhmProps.char [section, in abelian]

OhmProps.char.D [variable, in abelian]

OhmProps.char.G [variable, in abelian]

OhmProps.char.gT [variable, in abelian]

OhmProps.char.n [variable, in abelian]

OhmProps.char.rT [variable, in abelian]

OhmProps.Generic [section, in abelian]

OhmProps.Generic.gT [variable, in abelian]

OhmProps.Generic.n [variable, in abelian]

OhmProps.gT [variable, in abelian]

OhmS [lemma, in abelian]

Ohm_mgFun [definition, in abelian]

Ohm_gFun [definition, in abelian]

Ohm_igFun [definition, in abelian]

Ohm_group [definition, in abelian]

Ohm_char [lemma, in abelian]

Ohm_p_cycle [lemma, in abelian]

Ohm_cont [lemma, in abelian]

Ohm_Mho_homocyclic [lemma, in abelian]

Ohm_id [lemma, in abelian]

Ohm_sub [lemma, in abelian]

Ohm_normal [lemma, in abelian]

Ohm_dprod [lemma, in abelian]

Ohm_leq [lemma, in abelian]

Ohm0 [lemma, in abelian]

Ohm1 [lemma, in abelian]

Ohm1Eexponent [lemma, in abelian]

Ohm1Eprime [lemma, in abelian]

Ohm1_cent_max [lemma, in abelian]

Ohm1_cyclic_pgroup_prime [lemma, in abelian]

Ohm1_id [lemma, in abelian]

Ohm1_cent_max_normal_abelem [lemma, in maximal]

Ohm1_homocyclicP [lemma, in abelian]

Ohm1_stab_Ohm1_SCN_series [lemma, in maximal]

Ohm1_extraspecial_odd [lemma, in extraspecial]

Ohm1_eq1 [lemma, in abelian]

Ohm1_abelem [lemma, in abelian]

omap [abbreviation, in ssrfun]

oneg [definition, in fingroup]

one_group [definition, in fingroup]

onPhantom [definition, in ssrbool]

onT_bij [lemma, in ssrbool]

onW_bij [lemma, in ssrbool]

on_can_inj [lemma, in ssrbool]

on_card_preimset [lemma, in finset]

on1lT [lemma, in ssrbool]

on1lW [lemma, in ssrbool]

on1T [lemma, in ssrbool]

on1W [lemma, in ssrbool]

on2T [lemma, in ssrbool]

on2W [lemma, in ssrbool]

opair_of_injK [lemma, in choice]

opair_of_inj [definition, in choice]

OperationProperties [section, in ssrfun]

OperationProperties.R [variable, in ssrfun]

OperationProperties.S [variable, in ssrfun]

OperationProperties.SopSisS [section, in ssrfun]

OperationProperties.SopSisT [section, in ssrfun]

OperationProperties.SopTisR [section, in ssrfun]

OperationProperties.SopTisS [section, in ssrfun]

OperationProperties.SopTisT [section, in ssrfun]

OperationProperties.T [variable, in ssrfun]

oppmx [definition, in matrix]

opp_poly [definition, in poly]

opp_lapp [definition, in vector]

opp_row_mx [lemma, in matrix]

opp_col_mx [lemma, in matrix]

opp_block_mx [lemma, in matrix]

opp_lappE [lemma, in vector]

OpsTheory [section, in fintype]

OpsTheory.EnumPick [section, in fintype]

OpsTheory.EnumPick.P [variable, in fintype]

OpsTheory.T [variable, in fintype]

Option [module, in ssrfun]

OptionEqType [section, in eqtype]

OptionEqType.T [variable, in eqtype]

OptionFinType [section, in fintype]

OptionFinType.T [variable, in fintype]

option_finMixin [definition, in fintype]

option_countMixin [definition, in choice]

option_finType [definition, in fintype]

option_enumP [lemma, in fintype]

option_eqType [definition, in eqtype]

option_eqMixin [definition, in eqtype]

option_countType [definition, in choice]

option_choiceType [definition, in choice]

option_enum [definition, in fintype]

option_choiceMixin [definition, in choice]

Option.apply [definition, in ssrfun]

Option.bind [definition, in ssrfun]

Option.default [definition, in ssrfun]

Option.map [definition, in ssrfun]

opt_eqP [lemma, in eqtype]

opt_eq [definition, in eqtype]

orbA [lemma, in ssrbool]

orbAC [lemma, in ssrbool]

orbb [lemma, in ssrbool]

orbb_idr [lemma, in ssrbool]

orbC [lemma, in ssrbool]

orbCA [lemma, in ssrbool]

orbF [lemma, in ssrbool]

Orbit [section, in fingraph]

orbit [definition, in action]

orbit [definition, in fingraph]

orbitE [lemma, in action]

orbitJ [lemma, in action]

orbitJs [lemma, in action]

orbitP [lemma, in action]

orbitR [lemma, in action]

orbitRs [lemma, in action]

orbit_conjsg_in [lemma, in action]

orbit_inv_in [lemma, in action]

orbit_in_trans [lemma, in action]

orbit_in_sym [lemma, in action]

orbit_trans [lemma, in action]

orbit_transr [lemma, in action]

orbit_in_transr [lemma, in action]

orbit_refl [lemma, in action]

orbit_rcoset [lemma, in action]

orbit_rel [abbreviation, in action]

orbit_morphim_actperm [lemma, in action]

orbit_uniq [lemma, in fingraph]

orbit_lcoset_in [lemma, in action]

orbit_stabilizer [lemma, in action]

orbit_eq_mem [lemma, in action]

orbit_inv [lemma, in action]

orbit_rot_cycle [lemma, in fingraph]

orbit_sym [lemma, in action]

orbit_transl [lemma, in action]

orbit_rcoset_in [lemma, in action]

orbit_in_transl [lemma, in action]

orbit_lcoset [lemma, in action]

orbit_conjsg [lemma, in action]

Orbit.f [variable, in fingraph]

Orbit.Hf [variable, in fingraph]

Orbit.Loop [section, in fingraph]

Orbit.Loop.Hp [variable, in fingraph]

Orbit.Loop.Hx [variable, in fingraph]

Orbit.Loop.p [variable, in fingraph]

Orbit.Loop.Up [variable, in fingraph]

Orbit.Loop.x [variable, in fingraph]

Orbit.T [variable, in fingraph]

orbit1P [lemma, in action]

orbK [lemma, in ssrbool]

orbN [lemma, in ssrbool]

orbT [lemma, in ssrbool]

orb_id2l [lemma, in ssrbool]

orb_id2r [lemma, in ssrbool]

orb_andr [lemma, in ssrbool]

orb_addoid [definition, in bigop]

orb_muloid [definition, in bigop]

orb_comoid [definition, in bigop]

orb_monoid [definition, in bigop]

orb_andl [lemma, in ssrbool]

orb_idl [lemma, in ssrbool]

order [definition, in fingraph]

order [definition, in fingroup]

orderE [lemma, in fingroup]

orderJ [lemma, in fingroup]

orderM [lemma, in cyclic]

orderSpred [lemma, in fingraph]

orderV [lemma, in fingroup]

orderXdiv [lemma, in cyclic]

orderXdvd [lemma, in cyclic]

orderXexp [lemma, in cyclic]

orderXgcd [lemma, in cyclic]

orderXpfactor [lemma, in cyclic]

orderXpnat [lemma, in cyclic]

orderXprime [lemma, in cyclic]

order_inf [lemma, in cyclic]

order_gt0 [lemma, in fingroup]

order_set_finv [lemma, in fingraph]

order_set [definition, in fingraph]

order_gt1 [lemma, in fingroup]

order_inj_cyclic [lemma, in cyclic]

order_Zp1 [lemma, in zmodp]

order_div_card [lemma, in fingraph]

order_finv [lemma, in fingraph]

order_injm [lemma, in morphism]

order_path_min [lemma, in path]

order_cycle [lemma, in fingraph]

order_eq1 [lemma, in fingroup]

order_dvdn [lemma, in cyclic]

order_dvdG [lemma, in cyclic]

order_constt [lemma, in pgroup]

order1 [lemma, in fingroup]

ordinal [inductive, in fintype]

Ordinal [constructor, in fintype]

OrdinalEnum [section, in fintype]

OrdinalEnum.n [variable, in fintype]

OrdinalPos [section, in fintype]

OrdinalPos.n' [variable, in fintype]

OrdinalSub [section, in fintype]

OrdinalSub.n [variable, in fintype]

ordinal_choiceMixin [definition, in fintype]

ordinal_finMixin [definition, in fintype]

ordinal_subFinType [definition, in fintype]

ordinal_finType [definition, in fintype]

ordinal_subCountType [definition, in fintype]

ordinal_countType [definition, in fintype]

ordinal_choiceType [definition, in fintype]

ordinal_eqType [definition, in fintype]

ordinal_subType [definition, in fintype]

ordinal_eqMixin [definition, in fintype]

ordinal_countMixin [definition, in fintype]

ord_enum_uniq [lemma, in fintype]

ord_enum [definition, in fintype]

ord_tuple [definition, in tuple]

ord_max [definition, in fintype]

ord_inj [lemma, in fintype]

ord0 [definition, in fintype]

ord1 [lemma, in zmodp]

orFb [lemma, in ssrbool]

orKb [lemma, in ssrbool]

orNb [lemma, in ssrbool]

orP [lemma, in ssrbool]

orTb [lemma, in ssrbool]

or3 [inductive, in ssrbool]

or3P [lemma, in ssrbool]

Or31 [constructor, in ssrbool]

Or32 [constructor, in ssrbool]

Or33 [constructor, in ssrbool]

or4 [inductive, in ssrbool]

or4P [lemma, in ssrbool]

Or41 [constructor, in ssrbool]

Or42 [constructor, in ssrbool]

Or43 [constructor, in ssrbool]

Or44 [constructor, in ssrbool]

OtherEncodings [section, in choice]

OtherEncodings.T [variable, in choice]

OtherEncodings.T1 [variable, in choice]

OtherEncodings.T2 [variable, in choice]

out_Aut [lemma, in automorphism]

out_perm [lemma, in perm]

oZ [definition, in maximal]

oZ [definition, in maximal]

oZp [definition, in mxabelem]

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 | (14626 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 | (165 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 | (112 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 | (7292 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 | (761 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 | (250 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 | (390 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 | (84 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 | (3144 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 | (126 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 | (28 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 | (2221 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 | (53 entries) |