| 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 | -(23836 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 | -(1409 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 | -(221 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 | -(3574 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 | -(90 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 | -(12096 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 | -(368 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 | -(45 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 | -(107 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 | -(273 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 | -(1140 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 | -(728 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 | -(3596 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 | -(189 entries) | -
U
-ucnE [lemma, in mathcomp.solvable.nilpotent]-ucnP [lemma, in mathcomp.solvable.nilpotent]
-ucnSn [lemma, in mathcomp.solvable.nilpotent]
-ucnSnR [lemma, in mathcomp.solvable.nilpotent]
-ucn_nilpotent [lemma, in mathcomp.solvable.nilpotent]
-ucn_id [lemma, in mathcomp.solvable.nilpotent]
-ucn_nil_classP [lemma, in mathcomp.solvable.nilpotent]
-ucn_lcnP [lemma, in mathcomp.solvable.nilpotent]
-ucn_bigdprod [lemma, in mathcomp.solvable.nilpotent]
-ucn_bigcprod [lemma, in mathcomp.solvable.nilpotent]
-ucn_dprod [lemma, in mathcomp.solvable.nilpotent]
-ucn_cprod [lemma, in mathcomp.solvable.nilpotent]
-ucn_comm [lemma, in mathcomp.solvable.nilpotent]
-ucn_normalS [lemma, in mathcomp.solvable.nilpotent]
-ucn_central [lemma, in mathcomp.solvable.nilpotent]
-ucn_sub_geq [lemma, in mathcomp.solvable.nilpotent]
-ucn_subS [lemma, in mathcomp.solvable.nilpotent]
-ucn_normal [lemma, in mathcomp.solvable.nilpotent]
-ucn_norm [lemma, in mathcomp.solvable.nilpotent]
-ucn_char [lemma, in mathcomp.solvable.nilpotent]
-ucn_sub [lemma, in mathcomp.solvable.nilpotent]
-ucn_group_set [lemma, in mathcomp.solvable.nilpotent]
-ucn_pmap [lemma, in mathcomp.solvable.nilpotent]
-ucn0 [lemma, in mathcomp.solvable.nilpotent]
-ucn1 [lemma, in mathcomp.solvable.nilpotent]
-ucycle [definition, in mathcomp.ssreflect.path]
-ucycleb [definition, in mathcomp.ssreflect.path]
-ucycle_uniq [lemma, in mathcomp.ssreflect.path]
-ucycle_cycle [lemma, in mathcomp.ssreflect.path]
-ufcycle [abbreviation, in mathcomp.ssreflect.path]
-ulsubmx [definition, in mathcomp.algebra.matrix]
-unbump [definition, in mathcomp.ssreflect.fintype]
-unbumpK [lemma, in mathcomp.ssreflect.fintype]
-unbumpKcond [lemma, in mathcomp.ssreflect.fintype]
-unbumpS [lemma, in mathcomp.ssreflect.fintype]
-unbump_addl [lemma, in mathcomp.ssreflect.fintype]
-undup [definition, in mathcomp.ssreflect.seq]
-undup_nil [lemma, in mathcomp.ssreflect.seq]
-undup_id [lemma, in mathcomp.ssreflect.seq]
-undup_uniq [lemma, in mathcomp.ssreflect.seq]
-uniq [definition, in mathcomp.ssreflect.seq]
-UniqCycle [section, in mathcomp.ssreflect.path]
-UniqCycleRev [section, in mathcomp.ssreflect.path]
-UniqCycleRev.T [variable, in mathcomp.ssreflect.path]
-UniqCycle.e [variable, in mathcomp.ssreflect.path]
-UniqCycle.n0 [variable, in mathcomp.ssreflect.path]
-UniqCycle.p [variable, in mathcomp.ssreflect.path]
-UniqCycle.T [variable, in mathcomp.ssreflect.path]
-UniqCycle.Up [variable, in mathcomp.ssreflect.path]
-uniqP [lemma, in mathcomp.ssreflect.seq]
-uniqPn [lemma, in mathcomp.ssreflect.seq]
-UniqRotrCycle [section, in mathcomp.ssreflect.path]
-UniqRotrCycle.n0 [variable, in mathcomp.ssreflect.path]
-UniqRotrCycle.p [variable, in mathcomp.ssreflect.path]
-UniqRotrCycle.T [variable, in mathcomp.ssreflect.path]
-UniqRotrCycle.Up [variable, in mathcomp.ssreflect.path]
-uniq_normal_Hall [lemma, in mathcomp.solvable.pgroup]
-uniq_traject_pcycle [lemma, in mathcomp.fingroup.perm]
-uniq_perm_eq [abbreviation, in mathcomp.ssreflect.seq]
-uniq_perm [lemma, in mathcomp.ssreflect.seq]
-uniq_min_size [lemma, in mathcomp.ssreflect.seq]
-uniq_size_uniq [lemma, in mathcomp.ssreflect.seq]
-uniq_leq_size [lemma, in mathcomp.ssreflect.seq]
-uniq_catCA [lemma, in mathcomp.ssreflect.seq]
-uniq_catC [lemma, in mathcomp.ssreflect.seq]
-uniq_rootsE [lemma, in mathcomp.algebra.poly]
-uniq_roots_prod_XsubC [lemma, in mathcomp.algebra.poly]
-uniq_roots [definition, in mathcomp.algebra.poly]
-uniq4_uniq6 [lemma, in mathcomp.solvable.burnside_app]
-unitFpE [lemma, in mathcomp.algebra.zmodp]
-unitmx [definition, in mathcomp.algebra.matrix]
-unitmxE [lemma, in mathcomp.algebra.matrix]
-unitmxZ [lemma, in mathcomp.algebra.matrix]
-unitmx_mul [lemma, in mathcomp.algebra.matrix]
-unitmx_inv [lemma, in mathcomp.algebra.matrix]
-unitmx_tr [lemma, in mathcomp.algebra.matrix]
-unitmx_perm [lemma, in mathcomp.algebra.matrix]
-unitmx1 [lemma, in mathcomp.algebra.matrix]
-UnitRingQuot [section, in mathcomp.algebra.ring_quotient]
-UnitRingQuotClass [constructor, in mathcomp.algebra.ring_quotient]
-UnitRingQuotMixin [abbreviation, in mathcomp.algebra.ring_quotient]
-UnitRingQuotMixinPack [constructor, in mathcomp.algebra.ring_quotient]
-UnitRingQuotMixin_pack [definition, in mathcomp.algebra.ring_quotient]
-UnitRingQuotType [abbreviation, in mathcomp.algebra.ring_quotient]
-unitRingQuotType [record, in mathcomp.algebra.ring_quotient]
-UnitRingQuotTypePack [constructor, in mathcomp.algebra.ring_quotient]
-UnitRingQuotType_clone [definition, in mathcomp.algebra.ring_quotient]
-UnitRingQuotType_pack [definition, in mathcomp.algebra.ring_quotient]
-UnitRingQuot.addT [variable, in mathcomp.algebra.ring_quotient]
-UnitRingQuot.eqT [variable, in mathcomp.algebra.ring_quotient]
-UnitRingQuot.invT [variable, in mathcomp.algebra.ring_quotient]
-UnitRingQuot.mulT [variable, in mathcomp.algebra.ring_quotient]
-UnitRingQuot.oneT [variable, in mathcomp.algebra.ring_quotient]
-UnitRingQuot.oppT [variable, in mathcomp.algebra.ring_quotient]
-UnitRingQuot.T [variable, in mathcomp.algebra.ring_quotient]
-UnitRingQuot.unitT [variable, in mathcomp.algebra.ring_quotient]
-UnitRingQuot.zeroT [variable, in mathcomp.algebra.ring_quotient]
-unitrXz [lemma, in mathcomp.algebra.ssrint]
-unitr_trmx [lemma, in mathcomp.algebra.matrix]
-unitr_n0expz [lemma, in mathcomp.algebra.ssrint]
-unitr_algid1 [lemma, in mathcomp.field.falgebra]
-units_Zp_abelian [lemma, in mathcomp.algebra.zmodp]
-units_Zp [definition, in mathcomp.algebra.zmodp]
-UnityRootTheory [module, in mathcomp.algebra.poly]
-UnityRootTheory.eq_prim_root_expr [definition, in mathcomp.algebra.poly]
-UnityRootTheory.fmorph_primitive_root [definition, in mathcomp.algebra.poly]
-UnityRootTheory.fmorph_unity_root [definition, in mathcomp.algebra.poly]
-UnityRootTheory.max_unity_roots [definition, in mathcomp.algebra.poly]
-UnityRootTheory.mem_unity_roots [definition, in mathcomp.algebra.poly]
-UnityRootTheory.prim_rootP [definition, in mathcomp.algebra.poly]
-UnityRootTheory.prim_order_dvd [definition, in mathcomp.algebra.poly]
-UnityRootTheory.prim_expr_mod [definition, in mathcomp.algebra.poly]
-UnityRootTheory.prim_expr_order [abbreviation, in mathcomp.algebra.poly]
-UnityRootTheory.prim_order_gt0 [abbreviation, in mathcomp.algebra.poly]
-UnityRootTheory.prim_order_exists [definition, in mathcomp.algebra.poly]
-UnityRootTheory.rmorph_unity_root [definition, in mathcomp.algebra.poly]
-UnityRootTheory.unity_rootP [definition, in mathcomp.algebra.poly]
-UnityRootTheory.unity_rootE [definition, in mathcomp.algebra.poly]
-_ .-primitive_root (unity_root_scope) [notation, in mathcomp.algebra.poly]
-_ .-unity_root (unity_root_scope) [notation, in mathcomp.algebra.poly]
-unity_rootP [lemma, in mathcomp.algebra.poly]
-unity_rootE [lemma, in mathcomp.algebra.poly]
-unitZpE [lemma, in mathcomp.algebra.zmodp]
-unit_ring_quot_mixinP [lemma, in mathcomp.algebra.ring_quotient]
-unit_ring_eq_quot_class [definition, in mathcomp.algebra.ring_quotient]
-unit_ring_zmod_quot_class [definition, in mathcomp.algebra.ring_quotient]
-unit_ring_ring_quot_class [definition, in mathcomp.algebra.ring_quotient]
-unit_ring_quot_class [definition, in mathcomp.algebra.ring_quotient]
-unit_ring_quot_sort [projection, in mathcomp.algebra.ring_quotient]
-unit_ring_quot_mixin [projection, in mathcomp.algebra.ring_quotient]
-unit_ring_quot_ring_class [projection, in mathcomp.algebra.ring_quotient]
-unit_ring_quot_quot_class [projection, in mathcomp.algebra.ring_quotient]
-unit_ring_quot_class_of [record, in mathcomp.algebra.ring_quotient]
-unit_ring_zmod_quot_mixin [projection, in mathcomp.algebra.ring_quotient]
-unit_ring_quot_mixin_of [record, in mathcomp.algebra.ring_quotient]
-unit_countMixin [definition, in mathcomp.ssreflect.choice]
-unit_choiceMixin [definition, in mathcomp.ssreflect.choice]
-unit_finMixin [definition, in mathcomp.ssreflect.fintype]
-unit_enumP [lemma, in mathcomp.ssreflect.fintype]
-unit_eqMixin [definition, in mathcomp.ssreflect.eqtype]
-unit_eqP [lemma, in mathcomp.ssreflect.eqtype]
-unit_Zp_expg [lemma, in mathcomp.algebra.zmodp]
-unit_Zp_mulgC [lemma, in mathcomp.algebra.zmodp]
-unlift [definition, in mathcomp.ssreflect.fintype]
-UnliftNone [constructor, in mathcomp.ssreflect.fintype]
-unliftP [lemma, in mathcomp.ssreflect.fintype]
-UnliftSome [constructor, in mathcomp.ssreflect.fintype]
-unlift_some [lemma, in mathcomp.ssreflect.fintype]
-unlift_none [lemma, in mathcomp.ssreflect.fintype]
-unlift_spec [inductive, in mathcomp.ssreflect.fintype]
-unlift_subproof [lemma, in mathcomp.ssreflect.fintype]
-unpickle [definition, in mathcomp.ssreflect.choice]
-unpickle_tagged [definition, in mathcomp.ssreflect.choice]
-unpickle_seq [definition, in mathcomp.ssreflect.choice]
-unsplit [definition, in mathcomp.ssreflect.fintype]
-unsplitK [lemma, in mathcomp.ssreflect.fintype]
-unzip1 [definition, in mathcomp.ssreflect.seq]
-unzip1_zip [lemma, in mathcomp.ssreflect.seq]
-unzip2 [definition, in mathcomp.ssreflect.seq]
-unzip2_zip [lemma, in mathcomp.ssreflect.seq]
-uphalf [definition, in mathcomp.ssreflect.ssrnat]
-uphalf_half [lemma, in mathcomp.ssreflect.ssrnat]
-uphalf_double [lemma, in mathcomp.ssreflect.ssrnat]
-UpperCentral [section, in mathcomp.solvable.nilpotent]
-UpperCentralFunctor [section, in mathcomp.solvable.nilpotent]
-UpperCentralFunctor.G [variable, in mathcomp.solvable.nilpotent]
-UpperCentralFunctor.gT [variable, in mathcomp.solvable.nilpotent]
-UpperCentralFunctor.n [variable, in mathcomp.solvable.nilpotent]
-UpperCentral.gT [variable, in mathcomp.solvable.nilpotent]
-upper_central_at [definition, in mathcomp.solvable.nilpotent]
-upper_central_at_rec [definition, in mathcomp.solvable.nilpotent]
-ursubmx [definition, in mathcomp.algebra.matrix]
-UseFinTuple [section, in mathcomp.ssreflect.tuple]
-UseFinTuple.ImageTuple [section, in mathcomp.ssreflect.tuple]
-UseFinTuple.ImageTuple.A [variable, in mathcomp.ssreflect.tuple]
-UseFinTuple.ImageTuple.f [variable, in mathcomp.ssreflect.tuple]
-UseFinTuple.ImageTuple.T' [variable, in mathcomp.ssreflect.tuple]
-UseFinTuple.MkTuple [section, in mathcomp.ssreflect.tuple]
-UseFinTuple.MkTuple.f [variable, in mathcomp.ssreflect.tuple]
-UseFinTuple.MkTuple.T' [variable, in mathcomp.ssreflect.tuple]
-UseFinTuple.n [variable, in mathcomp.ssreflect.tuple]
-UseFinTuple.T [variable, in mathcomp.ssreflect.tuple]
-usubmx [definition, in mathcomp.algebra.matrix]
-usubmx_key [lemma, in mathcomp.algebra.matrix]
-usumx_mul [lemma, in mathcomp.character.character]
-
| 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 | -(23836 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 | -(1409 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 | -(221 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 | -(3574 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 | -(90 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 | -(12096 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 | -(368 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 | -(45 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 | -(107 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 | -(273 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 | -(1140 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 | -(728 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 | -(3596 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 | -(189 entries) | -