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

## U

u [definition, in mxrepresentation]ucnE [lemma, in nilpotent]

ucnP [lemma, in nilpotent]

ucnSn [lemma, in nilpotent]

ucnSnR [lemma, in nilpotent]

ucn_normal [lemma, in nilpotent]

ucn_id [lemma, in nilpotent]

ucn_lcnP [lemma, in nilpotent]

ucn_char [lemma, in nilpotent]

ucn_normalS [lemma, in nilpotent]

ucn_pmap [lemma, in nilpotent]

ucn_sub_geq [lemma, in nilpotent]

ucn_central [lemma, in nilpotent]

ucn_group_set [lemma, in nilpotent]

ucn_comm [lemma, in nilpotent]

ucn_nilpotent [lemma, in nilpotent]

ucn_pgFun [definition, in nilpotent]

ucn_gFun [definition, in nilpotent]

ucn_igFun [definition, in nilpotent]

ucn_norm [lemma, in nilpotent]

ucn_nil_classP [lemma, in nilpotent]

ucn_subS [lemma, in nilpotent]

ucn_sub [lemma, in nilpotent]

ucn0 [lemma, in nilpotent]

ucn1 [lemma, in nilpotent]

ucycle [definition, in path]

ucycleb [definition, in path]

ucycle_uniq [lemma, in path]

ucycle_rot [lemma, in path]

ucycle_rotr [lemma, in path]

ucycle_cycle [lemma, in path]

ufcycle [abbreviation, in path]

ulsubmx [definition, in matrix]

unbump [definition, in fintype]

unbumpK [lemma, in fintype]

unbumpKcond [lemma, in fintype]

unbumpS [lemma, in fintype]

unbump_addl [lemma, in fintype]

undup [definition, in seq]

undup_id [lemma, in seq]

undup_uniq [lemma, in seq]

uniq [definition, in seq]

UniqCycle [section, in path]

UniqCycleRev [section, in path]

UniqCycleRev.T [variable, in path]

UniqCycle.e [variable, in path]

UniqCycle.n0 [variable, in path]

UniqCycle.p [variable, in path]

UniqCycle.T [variable, in path]

UniqCycle.Up [variable, in path]

UniqRotrCycle [section, in path]

UniqRotrCycle.n0 [variable, in path]

UniqRotrCycle.p [variable, in path]

UniqRotrCycle.T [variable, in path]

UniqRotrCycle.Up [variable, in path]

uniq_traject_pcycle [lemma, in perm]

uniq_leq_size [lemma, in seq]

uniq_size_uniq [lemma, in seq]

uniq_roots [definition, in poly]

uniq_catC [lemma, in seq]

uniq_catCA [lemma, in seq]

uniq_rootsE [lemma, in poly]

uniq_normal_Hall [lemma, in pgroup]

uniq_perm_eq [lemma, in seq]

uniq_roots_dvdp [lemma, in poly]

UnitAlgebra [module, in ssralg]

UnitAlgebra [module, in finalg]

UnitApp [section, in vector]

UnitApp.R [variable, in vector]

UnitApp.V [variable, in vector]

UnitApp.vdim_nz [variable, in vector]

unitE [lemma, in ssrfun]

unitFpE [lemma, in zmodp]

UnitImage [section, in vector]

UnitImage.K [variable, in vector]

UnitImage.V [variable, in vector]

unitmx [definition, in matrix]

unitmxE [lemma, in matrix]

unitmx_inv [lemma, in matrix]

unitmx_mul [lemma, in matrix]

unitmx_tr [lemma, in matrix]

unitmx_perm [lemma, in matrix]

unitmx1 [lemma, in matrix]

unitmx1F [definition, in mxalgebra]

UnitRing [module, in finalg]

UnitRing [module, in ssralg]

unitr_trmx [lemma, in matrix]

UnitsGroupExports [module, in finalg]

units_Zp [definition, in zmodp]

units_Zp_group [definition, in zmodp]

units_Zp_abelian [lemma, in zmodp]

UnityRootTheory [module, in poly]

UnityRootTheory.eq_prim_root_expr [definition, in poly]

UnityRootTheory.fmorph_primitive_root [definition, in poly]

UnityRootTheory.fmorph_unity_root [definition, in poly]

UnityRootTheory.max_unity_roots [definition, in poly]

UnityRootTheory.mem_unity_roots [definition, in poly]

UnityRootTheory.prim_order_exists [definition, in poly]

UnityRootTheory.prim_order_gt0 [abbreviation, in poly]

UnityRootTheory.prim_order_dvd [definition, in poly]

UnityRootTheory.prim_expr_order [abbreviation, in poly]

UnityRootTheory.prim_rootP [definition, in poly]

UnityRootTheory.prim_expr_mod [definition, in poly]

UnityRootTheory.rmorph_unity_root [definition, in poly]

UnityRootTheory.unity_rootE [definition, in poly]

UnityRootTheory.unity_rootP [definition, in poly]

unity_rootP [lemma, in poly]

unity_rootE [lemma, in poly]

unitZpE [lemma, in zmodp]

unit_lapp [definition, in vector]

unit_eqMixin [definition, in eqtype]

unit_lappE [lemma, in vector]

unit_finType [definition, in fintype]

unit_enumP [lemma, in fintype]

unit_finMixin [definition, in fintype]

unit_eqType [definition, in eqtype]

unit_pickleK [lemma, in choice]

unit_countType [definition, in choice]

unit_choiceType [definition, in choice]

unit_Zp_mulgC [lemma, in zmodp]

unit_Zp_expgn [lemma, in zmodp]

unit_eqP [lemma, in eqtype]

unit_countMixin [definition, in choice]

unit_choiceMixin [definition, in choice]

unit_nonzero_lapp [lemma, in vector]

unlift [definition, in fintype]

UnliftNone [constructor, in fintype]

unliftP [lemma, in fintype]

UnliftSome [constructor, in fintype]

unlift_spec [inductive, in fintype]

unlift_subproof [lemma, in fintype]

unlift_some [lemma, in fintype]

unlift_none [lemma, in fintype]

unlock [lemma, in ssreflect]

unlockable [record, in ssreflect]

Unlockable [constructor, in ssreflect]

unlocked [projection, in ssreflect]

unpickle [definition, in choice]

unsplit [definition, in fintype]

unsplitK [lemma, in fintype]

unwrap [projection, in ssrfun]

unwrap_pi_arg [definition, in prime]

unzip1 [definition, in seq]

unzip1_zip [lemma, in seq]

unzip2 [definition, in seq]

unzip2_zip [lemma, in seq]

uphalf [definition, in ssrnat]

uphalf_half [lemma, in ssrnat]

uphalf_double [lemma, in ssrnat]

UpperCentral [section, in nilpotent]

UpperCentralFunctor [section, in nilpotent]

UpperCentralFunctor.G [variable, in nilpotent]

UpperCentralFunctor.gT [variable, in nilpotent]

UpperCentralFunctor.n [variable, in nilpotent]

UpperCentral.gT [variable, in nilpotent]

upper_central_at_rec [definition, in nilpotent]

upper_central_at_group [definition, in nilpotent]

upper_central_at [definition, in nilpotent]

ursubmx [definition, in matrix]

UseFinTuple [section, in tuple]

UseFinTuple.n [variable, in tuple]

UseFinTuple.T [variable, in tuple]

usubmx [definition, in matrix]

usubmx_linear [definition, in matrix]

usubmx_additive [definition, in matrix]

Uu [definition, in mxrepresentation]

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