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)