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 | _ | (6599 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 | _ | (86 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 | _ | (57 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 | _ | (3455 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 | _ | (290 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 | _ | (147 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 | _ | (148 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 | _ | (53 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 | _ | (1466 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 | _ | (28 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 | _ | (53 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 | _ | (788 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 | _ | (28 entries) |

## O

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

ocancel [definition, in ssrfun]

odd [definition, in ssrnat]

oddb [lemma, in ssrnat]

odd_add [lemma, in ssrnat]

odd_double [lemma, in ssrnat]

odd_double_half [lemma, in ssrnat]

odd_exp [lemma, in ssrnat]

odd_lift_perm [lemma, in matrix]

odd_mod [lemma, in div]

odd_mul [lemma, in ssrnat]

odd_mul_tperm [lemma, in perm]

odd_opp [lemma, in ssrnat]

odd_perm [definition, in perm]

odd_permJ [lemma, in perm]

odd_permM [lemma, in perm]

odd_permV [lemma, in perm]

odd_perm1 [lemma, in perm]

odd_perm_prod [lemma, in perm]

odd_sub [lemma, in ssrnat]

odd_tperm [lemma, in perm]

odd_2'nat [lemma, in prime]

odflt [abbreviation, in ssrfun]

ohead [definition, in seq]

omap [abbreviation, in ssrfun]

onA_bij [lemma, in ssrbool]

oneg [definition, in groups]

one_group [definition, in groups]

onPhantom [definition, in ssrbool]

onW_bij [lemma, in ssrbool]

on1A [lemma, in ssrbool]

on1lA [lemma, in ssrbool]

on1lW [lemma, in ssrbool]

on1W [lemma, in ssrbool]

on2A [lemma, in ssrbool]

on2W [lemma, in ssrbool]

on_can_inj [lemma, in ssrbool]

on_card_preimset [lemma, in finset]

op [definition, in finset]

op [definition, in finset]

OperationProperties [section, in ssrfun]

OperationProperties.add [variable, in ssrfun]

OperationProperties.inv [variable, in ssrfun]

OperationProperties.mul [variable, in ssrfun]

OperationProperties.one [variable, in ssrfun]

OperationProperties.T [variable, in ssrfun]

OperationProperties.zero [variable, in ssrfun]

oppmx [definition, in matrix]

opp_poly [definition, in poly]

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.apply [definition, in ssrfun]

Option.bind [definition, in ssrfun]

Option.default [definition, in ssrfun]

Option.map [definition, in ssrfun]

option_choiceMixin [definition, in choice]

option_choiceType [definition, in choice]

option_countMixin [definition, in choice]

option_countType [definition, in choice]

option_enum [definition, in fintype]

option_enumP [lemma, in fintype]

option_eqMixin [definition, in eqtype]

option_eqType [definition, in eqtype]

option_finMixin [definition, in fintype]

option_finType [definition, in fintype]

opt_eq [definition, in eqtype]

opt_eqP [lemma, in eqtype]

orbA [lemma, in ssrbool]

orbAC [lemma, in ssrbool]

orbb [lemma, in ssrbool]

orbC [lemma, in ssrbool]

orbCA [lemma, in ssrbool]

orbF [lemma, in ssrbool]

Orbit [section, in connect]

orbit [definition, in connect]

Orbit.f [variable, in connect]

Orbit.Hf [variable, in connect]

Orbit.Loop [section, in connect]

Orbit.Loop.Hp [variable, in connect]

Orbit.Loop.Hx [variable, in connect]

Orbit.Loop.p [variable, in connect]

Orbit.Loop.Up [variable, in connect]

Orbit.Loop.x [variable, in connect]

Orbit.T [variable, in connect]

orbit_rot_cycle [lemma, in connect]

orbit_uniq [lemma, in connect]

orbK [lemma, in ssrbool]

orbN [lemma, in ssrbool]

orbT [lemma, in ssrbool]

orb_addoid [definition, in bigops]

orb_andl [lemma, in ssrbool]

orb_andr [lemma, in ssrbool]

orb_comoid [definition, in bigops]

orb_monoid [definition, in bigops]

orb_muloid [definition, in bigops]

order [definition, in groups]

order [definition, in connect]

orderJ [lemma, in groups]

orderM [lemma, in cyclic]

orderSpred [lemma, in connect]

orderV [lemma, in groups]

orderXdiv [lemma, in cyclic]

orderXdvd [lemma, in cyclic]

orderXgcd [lemma, in cyclic]

order1 [lemma, in groups]

order_cycle [lemma, in connect]

order_div_card [lemma, in connect]

order_dvdG [lemma, in cyclic]

order_dvdn [lemma, in cyclic]

order_eq1 [lemma, in cyclic]

order_finv [lemma, in connect]

order_gt0 [lemma, in groups]

order_inf [lemma, in cyclic]

order_inj_cyclic [lemma, in cyclic]

order_path_min [lemma, in paths]

order_pos_nat [definition, in groups]

order_set [definition, in connect]

order_set_finv [lemma, in connect]

Ordinal [constructor, in fintype]

ordinal [inductive, 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_choiceType [definition, in fintype]

ordinal_countMixin [definition, in fintype]

ordinal_countType [definition, in fintype]

ordinal_eqMixin [definition, in fintype]

ordinal_eqType [definition, in fintype]

ordinal_finMixin [definition, in fintype]

ordinal_finType [definition, in fintype]

ordinal_subCountType [definition, in fintype]

ordinal_subFinType [definition, in fintype]

ordinal_subType [definition, in fintype]

ord0 [definition, in fintype]

ord1 [lemma, in zmodp]

ord_enum [definition, in fintype]

ord_enum_uniq [lemma, in fintype]

ord_inj [lemma, in fintype]

ord_max [definition, in fintype]

ord_maxP [lemma, in fintype]

ord_opp [definition, in fintype]

ord_oppK [lemma, in fintype]

ord_sub [definition, in fintype]

ord_subP [lemma, in fintype]

ord_tuple [definition, in tuple]

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]

out_Aut [lemma, in automorphism]

out_perm [lemma, 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 | _ | (6599 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 | _ | (86 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 | _ | (57 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 | _ | (3455 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 | _ | (290 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 | _ | (147 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 | _ | (148 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 | _ | (53 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 | _ | (1466 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 | _ | (28 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 | _ | (53 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 | _ | (788 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 | _ | (28 entries) |