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 | (23233 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 | (1373 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 | (213 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 | (3475 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 | (89 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 | (11853 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 | (359 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 | (47 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 | (103 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 | (266 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 | (1118 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 | (691 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 | (3461 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 | (185 entries) |

## U (definition)

ucycle [in mathcomp.ssreflect.path]ucycleb [in mathcomp.ssreflect.path]

ulsubmx [in mathcomp.algebra.matrix]

unbump [in mathcomp.ssreflect.fintype]

undup [in mathcomp.ssreflect.seq]

uniq [in mathcomp.ssreflect.seq]

uniq_roots [in mathcomp.algebra.poly]

unitmx [in mathcomp.algebra.matrix]

UnitRingQuotMixin_pack [in mathcomp.algebra.ring_quotient]

UnitRingQuotType_clone [in mathcomp.algebra.ring_quotient]

UnitRingQuotType_pack [in mathcomp.algebra.ring_quotient]

units_Zp [in mathcomp.algebra.zmodp]

UnityRootTheory.eq_prim_root_expr [in mathcomp.algebra.poly]

UnityRootTheory.fmorph_primitive_root [in mathcomp.algebra.poly]

UnityRootTheory.fmorph_unity_root [in mathcomp.algebra.poly]

UnityRootTheory.max_unity_roots [in mathcomp.algebra.poly]

UnityRootTheory.mem_unity_roots [in mathcomp.algebra.poly]

UnityRootTheory.prim_rootP [in mathcomp.algebra.poly]

UnityRootTheory.prim_order_dvd [in mathcomp.algebra.poly]

UnityRootTheory.prim_expr_mod [in mathcomp.algebra.poly]

UnityRootTheory.prim_order_exists [in mathcomp.algebra.poly]

UnityRootTheory.rmorph_unity_root [in mathcomp.algebra.poly]

UnityRootTheory.unity_rootP [in mathcomp.algebra.poly]

UnityRootTheory.unity_rootE [in mathcomp.algebra.poly]

unit_ring_eq_quot_class [in mathcomp.algebra.ring_quotient]

unit_ring_zmod_quot_class [in mathcomp.algebra.ring_quotient]

unit_ring_ring_quot_class [in mathcomp.algebra.ring_quotient]

unit_ring_quot_class [in mathcomp.algebra.ring_quotient]

unit_countMixin [in mathcomp.ssreflect.choice]

unit_choiceMixin [in mathcomp.ssreflect.choice]

unit_finMixin [in mathcomp.ssreflect.fintype]

unit_eqMixin [in mathcomp.ssreflect.eqtype]

unlift [in mathcomp.ssreflect.fintype]

unpickle [in mathcomp.ssreflect.choice]

unpickle_tagged [in mathcomp.ssreflect.choice]

unpickle_seq [in mathcomp.ssreflect.choice]

unsplit [in mathcomp.ssreflect.fintype]

unzip1 [in mathcomp.ssreflect.seq]

unzip2 [in mathcomp.ssreflect.seq]

uphalf [in mathcomp.ssreflect.ssrnat]

upper_central_at [in mathcomp.solvable.nilpotent]

upper_central_at_rec [in mathcomp.solvable.nilpotent]

ursubmx [in mathcomp.algebra.matrix]

usubmx [in mathcomp.algebra.matrix]

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 | (23233 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 | (1373 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 | (213 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 | (3475 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 | (89 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 | (11853 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 | (359 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 | (47 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 | (103 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 | (266 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 | (1118 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 | (691 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 | (3461 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 | (185 entries) |