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 (lemma)

oddb [in ssrnat]oddSg [in pgroup]

odd_mul [in ssrnat]

odd_permM [in perm]

odd_opp [in ssrnat]

odd_double_half [in ssrnat]

odd_pgroup_odd [in pgroup]

odd_sub [in ssrnat]

odd_add [in ssrnat]

odd_mul_tperm [in perm]

odd_tperm [in perm]

odd_double [in ssrnat]

odd_permV [in perm]

odd_exp [in ssrnat]

odd_not_extremal2 [in extremal]

odd_pgroup_rank1_cyclic [in extremal]

odd_2'nat [in prime]

odd_mod [in div]

odd_perm_prod [in perm]

odd_lift_perm [in perm]

odd_permJ [in perm]

odd_perm1 [in perm]

OhmE [in abelian]

OhmEabelian [in abelian]

OhmJ [in abelian]

OhmPredP [in abelian]

OhmS [in abelian]

Ohm_char [in abelian]

Ohm_p_cycle [in abelian]

Ohm_cont [in abelian]

Ohm_Mho_homocyclic [in abelian]

Ohm_id [in abelian]

Ohm_sub [in abelian]

Ohm_normal [in abelian]

Ohm_dprod [in abelian]

Ohm_leq [in abelian]

Ohm0 [in abelian]

Ohm1 [in abelian]

Ohm1Eexponent [in abelian]

Ohm1Eprime [in abelian]

Ohm1_cent_max [in abelian]

Ohm1_cyclic_pgroup_prime [in abelian]

Ohm1_id [in abelian]

Ohm1_cent_max_normal_abelem [in maximal]

Ohm1_homocyclicP [in abelian]

Ohm1_stab_Ohm1_SCN_series [in maximal]

Ohm1_extraspecial_odd [in extraspecial]

Ohm1_eq1 [in abelian]

Ohm1_abelem [in abelian]

onT_bij [in ssrbool]

onW_bij [in ssrbool]

on_can_inj [in ssrbool]

on_card_preimset [in finset]

on1lT [in ssrbool]

on1lW [in ssrbool]

on1T [in ssrbool]

on1W [in ssrbool]

on2T [in ssrbool]

on2W [in ssrbool]

opair_of_injK [in choice]

opp_row_mx [in matrix]

opp_col_mx [in matrix]

opp_block_mx [in matrix]

opp_lappE [in vector]

option_enumP [in fintype]

opt_eqP [in eqtype]

orbA [in ssrbool]

orbAC [in ssrbool]

orbb [in ssrbool]

orbb_idr [in ssrbool]

orbC [in ssrbool]

orbCA [in ssrbool]

orbF [in ssrbool]

orbitE [in action]

orbitJ [in action]

orbitJs [in action]

orbitP [in action]

orbitR [in action]

orbitRs [in action]

orbit_conjsg_in [in action]

orbit_inv_in [in action]

orbit_in_trans [in action]

orbit_in_sym [in action]

orbit_trans [in action]

orbit_transr [in action]

orbit_in_transr [in action]

orbit_refl [in action]

orbit_rcoset [in action]

orbit_morphim_actperm [in action]

orbit_uniq [in fingraph]

orbit_lcoset_in [in action]

orbit_stabilizer [in action]

orbit_eq_mem [in action]

orbit_inv [in action]

orbit_rot_cycle [in fingraph]

orbit_sym [in action]

orbit_transl [in action]

orbit_rcoset_in [in action]

orbit_in_transl [in action]

orbit_lcoset [in action]

orbit_conjsg [in action]

orbit1P [in action]

orbK [in ssrbool]

orbN [in ssrbool]

orbT [in ssrbool]

orb_id2l [in ssrbool]

orb_id2r [in ssrbool]

orb_andr [in ssrbool]

orb_andl [in ssrbool]

orb_idl [in ssrbool]

orderE [in fingroup]

orderJ [in fingroup]

orderM [in cyclic]

orderSpred [in fingraph]

orderV [in fingroup]

orderXdiv [in cyclic]

orderXdvd [in cyclic]

orderXexp [in cyclic]

orderXgcd [in cyclic]

orderXpfactor [in cyclic]

orderXpnat [in cyclic]

orderXprime [in cyclic]

order_inf [in cyclic]

order_gt0 [in fingroup]

order_set_finv [in fingraph]

order_gt1 [in fingroup]

order_inj_cyclic [in cyclic]

order_Zp1 [in zmodp]

order_div_card [in fingraph]

order_finv [in fingraph]

order_injm [in morphism]

order_path_min [in path]

order_cycle [in fingraph]

order_eq1 [in fingroup]

order_dvdn [in cyclic]

order_dvdG [in cyclic]

order_constt [in pgroup]

order1 [in fingroup]

ord_enum_uniq [in fintype]

ord_inj [in fintype]

ord1 [in zmodp]

orFb [in ssrbool]

orKb [in ssrbool]

orNb [in ssrbool]

orP [in ssrbool]

orTb [in ssrbool]

or3P [in ssrbool]

or4P [in ssrbool]

out_Aut [in automorphism]

out_perm [in perm]

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) |