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

## U

ucycle [definition, in paths]ucycleb [definition, in paths]

ucycle_cycle [lemma, in paths]

ucycle_rot [lemma, in paths]

ucycle_rotr [lemma, in paths]

ucycle_uniq [lemma, in paths]

ulsubmx [definition, in matrix]

unbump [definition, in fintype]

unbumpK [lemma, in fintype]

undup [definition, in seq]

undup_id [lemma, in seq]

undup_uniq [lemma, in seq]

uniq [definition, in seq]

UniqCycle [section, in paths]

UniqCycleRev [section, in paths]

UniqCycleRev.T [variable, in paths]

UniqCycle.e [variable, in paths]

UniqCycle.n0 [variable, in paths]

UniqCycle.p [variable, in paths]

UniqCycle.T [variable, in paths]

UniqCycle.Up [variable, in paths]

UniqFinMixin [abbreviation, in fintype]

UniqRotrCycle [section, in paths]

UniqRotrCycle.n0 [variable, in paths]

UniqRotrCycle.p [variable, in paths]

UniqRotrCycle.T [variable, in paths]

UniqRotrCycle.Up [variable, in paths]

uniq_catC [lemma, in seq]

uniq_catCA [lemma, in seq]

uniq_leq_size [lemma, in seq]

uniq_perm_eq [lemma, in seq]

uniq_roots [definition, in poly]

uniq_size_uniq [lemma, in seq]

UnitRing [module, in ssralg]

UnitRingMixin [abbreviation, in ssralg]

UnitRingType [abbreviation, in ssralg]

unitRingType [abbreviation, in ssralg]

unit_choiceMixin [definition, in choice]

unit_choiceType [definition, in choice]

unit_countMixin [definition, in choice]

unit_countType [definition, in choice]

unit_enumP [lemma, in fintype]

unit_eqMixin [definition, in eqtype]

unit_eqP [lemma, in eqtype]

unit_eqType [definition, in eqtype]

unit_finMixin [definition, in fintype]

unit_finType [definition, in fintype]

unit_mx [definition, in matrix]

unit_pickleK [lemma, in choice]

unlift [definition, in fintype]

UnliftNone [constructor, in fintype]

unliftP [lemma, in fintype]

UnliftSome [constructor, in fintype]

unlift_none [lemma, in fintype]

unlift_some [lemma, in fintype]

unlift_spec [inductive, in fintype]

unlift_subproof [lemma, in fintype]

unlock [lemma, in ssreflect]

Unlockable [constructor, in ssreflect]

unlockable [record, in ssreflect]

unlocked [projection, in ssreflect]

unpickle [definition, in choice]

unsplit [definition, in fintype]

unsplitK [lemma, in fintype]

unzip1 [definition, in seq]

unzip1_zip [lemma, in seq]

unzip2 [definition, in seq]

unzip2_zip [lemma, in seq]

uphalf [definition, in ssrnat]

uphalf_double [lemma, in ssrnat]

uphalf_half [lemma, in ssrnat]

ursubmx [definition, in matrix]

UseFinTuple [section, in tuple]

UseFinTuple.n [variable, in tuple]

UseFinTuple.T [variable, in tuple]

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