U (Global Index)

Files

Definitions

Lemmas

Abbreviations

Global Index

U

u_cons [abbrev, in mathcomp.algebra.tensor]
u_cons [abbrev, in mathcomp.algebra.tensor]
ubn_eq_spec [ind, in mathcomp.boot.ssrnat]
ubn_geq_spec [ind, in mathcomp.boot.ssrnat]
ubn_leq_spec [ind, in mathcomp.boot.ssrnat]
UbnEq [constr, in mathcomp.boot.ssrnat]
UbnGeq [constr, in mathcomp.boot.ssrnat]
UbnLeq [constr, in mathcomp.boot.ssrnat]
ubnP [prf, in mathcomp.boot.ssrnat]
ubnPeq [prf, in mathcomp.boot.ssrnat]
ubnPgeq [prf, in mathcomp.boot.ssrnat]
ubnPleq [prf, in mathcomp.boot.ssrnat]
ucn0 [prf, in mathcomp.solvable.nilpotent]
ucn1 [prf, in mathcomp.solvable.nilpotent]
ucn_bigcprod [prf, in mathcomp.solvable.nilpotent]
ucn_bigdprod [prf, in mathcomp.solvable.nilpotent]
ucn_central [prf, in mathcomp.solvable.nilpotent]
ucn_char [prf, in mathcomp.solvable.nilpotent]
ucn_comm [prf, in mathcomp.solvable.nilpotent]
ucn_cprod [prf, in mathcomp.solvable.nilpotent]
ucn_dprod [prf, in mathcomp.solvable.nilpotent]
ucn_gFun [def, in mathcomp.solvable.nilpotent]
ucn_group_set [prf, in mathcomp.solvable.nilpotent]
ucn_id [prf, in mathcomp.solvable.nilpotent]
ucn_igFun [def, in mathcomp.solvable.nilpotent]
ucn_lcnP [prf, in mathcomp.solvable.nilpotent]
ucn_nil_classP [prf, in mathcomp.solvable.nilpotent]
ucn_nilpotent [prf, in mathcomp.solvable.nilpotent]
ucn_norm [prf, in mathcomp.solvable.nilpotent]
ucn_normal [prf, in mathcomp.solvable.nilpotent]
ucn_normalS [prf, in mathcomp.solvable.nilpotent]
ucn_pgFun [def, in mathcomp.solvable.nilpotent]
ucn_pmap [prf, in mathcomp.solvable.nilpotent]
ucn_sub [prf, in mathcomp.solvable.nilpotent]
ucn_sub_geq [prf, in mathcomp.solvable.nilpotent]
ucn_subS [prf, in mathcomp.solvable.nilpotent]
ucnE [prf, in mathcomp.solvable.nilpotent]
ucnP [prf, in mathcomp.solvable.nilpotent]
ucnSn [prf, in mathcomp.solvable.nilpotent]
ucnSnR [prf, in mathcomp.solvable.nilpotent]
ucycle [def, in mathcomp.boot.path]
ucycle_cycle [prf, in mathcomp.boot.path]
ucycle_uniq [prf, in mathcomp.boot.path]
ucycleb [def, in mathcomp.boot.path]
ufcycle [abbrev, in mathcomp.boot.path]
ulsubmx [def, in mathcomp.algebra.matrix]
ulsubmx_diag [prf, in mathcomp.algebra.matrix]
ulsubmx_trig [prf, in mathcomp.algebra.matrix]
ulsubmxEsub [prf, in mathcomp.algebra.matrix]
UMagma [abbrev, in mathcomp.boot.monoid]
UMagma [mod, in mathcomp.boot.monoid]
UMagma.axioms_ [rec, in mathcomp.boot.monoid]
UMagma.choice_hasChoice_mixin [proj, in mathcomp.boot.monoid]
UMagma.class [proj, in mathcomp.boot.monoid]
UMagma.clone [abbrev, in mathcomp.boot.monoid]
UMagma.copy [abbrev, in mathcomp.boot.monoid]
UMagma.eqtype_hasDecEq_mixin [proj, in mathcomp.boot.monoid]
UMagma.Exports [mod, in mathcomp.boot.monoid]
UMagma.Exports.umagmaType [abbrev, in mathcomp.boot.monoid]
UMagma.monoid_BaseUMagma_isUMagma_mixin [proj, in mathcomp.boot.monoid]
UMagma.monoid_hasMul_mixin [proj, in mathcomp.boot.monoid]
UMagma.monoid_hasOne_mixin [proj, in mathcomp.boot.monoid]
UMagma.on [abbrev, in mathcomp.boot.monoid]
UMagma.on_ [abbrev, in mathcomp.boot.monoid]
UMagma.pack_ [def, in mathcomp.boot.monoid]
UMagma.phant_clone [def, in mathcomp.boot.monoid]
UMagma.phant_on_ [def, in mathcomp.boot.monoid]
UMagma.sort [proj, in mathcomp.boot.monoid]
UMagma.type [rec, in mathcomp.boot.monoid]
umagma_closed [def, in mathcomp.boot.monoid]
UMagma_isMonoid [abbrev, in mathcomp.boot.monoid]
UMagma_isMonoid [mod, in mathcomp.boot.monoid]
UMagma_isMonoid.axioms [abbrev, in mathcomp.boot.monoid]
UMagma_isMonoid.axioms_ [rec, in mathcomp.boot.monoid]
UMagma_isMonoid.Build [abbrev, in mathcomp.boot.monoid]
UMagma_isMonoid.Exports [mod, in mathcomp.boot.monoid]
UMagma_isMonoid.mulgA [proj, in mathcomp.boot.monoid]
UMagma_isMonoid.phant_axioms [def, in mathcomp.boot.monoid]
UMagma_isMonoid.phant_Build [def, in mathcomp.boot.monoid]
UMagmaClosed [abbrev, in mathcomp.boot.monoid]
UMagmaClosed [mod, in mathcomp.boot.monoid]
UMagmaClosed.axioms_ [rec, in mathcomp.boot.monoid]
UMagmaClosed.class [proj, in mathcomp.boot.monoid]
UMagmaClosed.clone [abbrev, in mathcomp.boot.monoid]
UMagmaClosed.copy [abbrev, in mathcomp.boot.monoid]
UMagmaClosed.Exports [mod, in mathcomp.boot.monoid]
UMagmaClosed.Exports.umagmaClosed [abbrev, in mathcomp.boot.monoid]
UMagmaClosed.monoid_isMul1Closed_mixin [proj, in mathcomp.boot.monoid]
UMagmaClosed.monoid_isMulClosed_mixin [proj, in mathcomp.boot.monoid]
UMagmaClosed.on [abbrev, in mathcomp.boot.monoid]
UMagmaClosed.on_ [abbrev, in mathcomp.boot.monoid]
UMagmaClosed.pack_ [def, in mathcomp.boot.monoid]
UMagmaClosed.phant_clone [def, in mathcomp.boot.monoid]
UMagmaClosed.phant_on_ [def, in mathcomp.boot.monoid]
UMagmaClosed.sort [proj, in mathcomp.boot.monoid]
UMagmaClosed.type [rec, in mathcomp.boot.monoid]
UMagmaClosedElpiOperations [mod, in mathcomp.boot.monoid]
UMagmaElpiOperations [mod, in mathcomp.boot.monoid]
UMagmaMorphism [abbrev, in mathcomp.boot.monoid]
UMagmaMorphism [mod, in mathcomp.boot.monoid]
UMagmaMorphism.axioms_ [rec, in mathcomp.boot.monoid]
UMagmaMorphism.class [proj, in mathcomp.boot.monoid]
UMagmaMorphism.clone [abbrev, in mathcomp.boot.monoid]
UMagmaMorphism.copy [abbrev, in mathcomp.boot.monoid]
UMagmaMorphism.Exports [mod, in mathcomp.boot.monoid]
UMagmaMorphism.monoid_isMultiplicative_mixin [proj, in mathcomp.boot.monoid]
UMagmaMorphism.monoid_Multiplicative_isUMagmaMorphism_mixin [proj, in mathcomp.boot.monoid]
UMagmaMorphism.on [abbrev, in mathcomp.boot.monoid]
UMagmaMorphism.on_ [abbrev, in mathcomp.boot.monoid]
UMagmaMorphism.pack_ [def, in mathcomp.boot.monoid]
UMagmaMorphism.phant_clone [def, in mathcomp.boot.monoid]
UMagmaMorphism.phant_on_ [def, in mathcomp.boot.monoid]
UMagmaMorphism.sort [proj, in mathcomp.boot.monoid]
UMagmaMorphism.type [rec, in mathcomp.boot.monoid]
UMagmaMorphismElpiOperations [mod, in mathcomp.boot.monoid]
unbump [def, in mathcomp.boot.fintype]
unbumpDl [prf, in mathcomp.boot.fintype]
unbumpK [prf, in mathcomp.boot.fintype]
unbumpKcond [prf, in mathcomp.boot.fintype]
unbumpS [prf, in mathcomp.boot.fintype]
undup [def, in mathcomp.boot.seq]
undup_cat [prf, in mathcomp.boot.seq]
undup_cycle_cons [prf, in mathcomp.boot.fingraph]
undup_flatten_nseq [prf, in mathcomp.boot.seq]
undup_id [prf, in mathcomp.boot.seq]
undup_map_inj [prf, in mathcomp.boot.seq]
undup_nil [prf, in mathcomp.boot.seq]
undup_path [prf, in mathcomp.boot.path]
undup_rcons [prf, in mathcomp.boot.seq]
undup_sorted [prf, in mathcomp.boot.path]
undup_subseq [prf, in mathcomp.boot.seq]
undup_uniq [prf, in mathcomp.boot.seq]
Unify [proj, in mathcomp.algebra.interval_inference]
Unify [constr, in mathcomp.algebra.interval_inference]
unify [rec, in mathcomp.algebra.interval_inference]
unify [ind, in mathcomp.algebra.interval_inference]
Unify' [proj, in mathcomp.algebra.interval_inference]
Unify' [constr, in mathcomp.algebra.interval_inference]
unify' [rec, in mathcomp.algebra.interval_inference]
unify' [ind, in mathcomp.algebra.interval_inference]
unify'P [inst, in mathcomp.algebra.interval_inference]
unify_itv [abbrev, in mathcomp.algebra.interval_inference]
uniq [def, in mathcomp.boot.seq]
uniq4_uniq6 [prf, in mathcomp.solvable.burnside_app]
uniq_cat_inLR [prf, in mathcomp.boot.seq]
uniq_cat_inRL [prf, in mathcomp.boot.seq]
uniq_catC [prf, in mathcomp.boot.seq]
uniq_catCA [prf, in mathcomp.boot.seq]
uniq_eqseq_pivotl [prf, in mathcomp.boot.seq]
uniq_eqseq_pivotr [prf, in mathcomp.boot.seq]
uniq_leq_size [prf, in mathcomp.boot.seq]
uniq_map_inj_in [prf, in mathcomp.boot.seq]
uniq_min_size [prf, in mathcomp.boot.seq]
uniq_normal_Hall [prf, in mathcomp.solvable.pgroup]
uniq_pairwise [prf, in mathcomp.boot.seq]
uniq_perm [prf, in mathcomp.boot.seq]
uniq_roots [def, in mathcomp.algebra.poly]
uniq_roots_prod_XsubC [prf, in mathcomp.algebra.poly]
uniq_rootsE [prf, in mathcomp.algebra.poly]
uniq_size_uniq [prf, in mathcomp.boot.seq]
uniq_sub_le_big [prf, in mathcomp.boot.bigop]
uniq_sub_le_big_cond [prf, in mathcomp.boot.bigop]
uniq_subseq_pivot [prf, in mathcomp.boot.seq]
uniq_traject_porbit [prf, in mathcomp.finite_group.perm]
uniqP [prf, in mathcomp.boot.seq]
uniqPn [prf, in mathcomp.boot.seq]
unit_enumP [prf, in mathcomp.boot.fintype]
unit_eqP [prf, in mathcomp.boot.eqtype]
unit_Zp_expg [prf, in mathcomp.algebra.zmodp]
unit_Zp_mulgC [prf, in mathcomp.algebra.zmodp]
UnitAlgebra_isFalgebra [abbrev, in mathcomp.field.falgebra]
UnitAlgebra_isFalgebra [mod, in mathcomp.field.falgebra]
UnitAlgebra_isFalgebra.axioms [abbrev, in mathcomp.field.falgebra]
UnitAlgebra_isFalgebra.axioms_ [rec, in mathcomp.field.falgebra]
UnitAlgebra_isFalgebra.Build [abbrev, in mathcomp.field.falgebra]
UnitAlgebra_isFalgebra.Exports [mod, in mathcomp.field.falgebra]
UnitAlgebra_isFalgebra.phant_axioms [def, in mathcomp.field.falgebra]
UnitAlgebra_isFalgebra.phant_Build [def, in mathcomp.field.falgebra]
unitarymx [def, in mathcomp.algebra.spectral]
unitarymx_key [prf, in mathcomp.algebra.spectral]
unitarymx_keyed [def, in mathcomp.algebra.spectral]
unitarymx_unit [prf, in mathcomp.algebra.spectral]
unitarymxP [prf, in mathcomp.algebra.spectral]
unitFpE [prf, in mathcomp.algebra.zmodp]
unitmx [def, in mathcomp.algebra.matrix]
unitmx1 [prf, in mathcomp.algebra.matrix]
unitmx_inv [prf, in mathcomp.algebra.matrix]
unitmx_mul [prf, in mathcomp.algebra.matrix]
unitmx_perm [prf, in mathcomp.algebra.matrix]
unitmx_tr [prf, in mathcomp.algebra.matrix]
unitmxE [prf, in mathcomp.algebra.matrix]
unitmxZ [prf, in mathcomp.algebra.matrix]
unitr_algid1 [prf, in mathcomp.field.falgebra]
unitr_n0expz [prf, in mathcomp.algebra.ssrint]
unitr_trmx [prf, in mathcomp.algebra.matrix]
UnitRingQuotient [abbrev, in mathcomp.algebra.ring_quotient]
UnitRingQuotient [mod, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Algebra_AddMagma_isAddSemigroup_mixin [proj, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Algebra_BaseAddMagma_isAddMagma_mixin [proj, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Algebra_BaseAddUMagma_isAddUMagma_mixin [proj, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Algebra_BaseZmoduleNmodule_isZmodule_mixin [proj, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Algebra_hasAdd_mixin [proj, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Algebra_hasOpp_mixin [proj, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Algebra_hasZero_mixin [proj, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.axioms_ [rec, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.choice_hasChoice_mixin [proj, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.class [proj, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.clone [abbrev, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.copy [abbrev, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.eqtype_hasDecEq_mixin [proj, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports [mod, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports.join_ring_quotient_UnitRingQuotient_between_generic_quotient_EqQuotient_and_GRing_UnitRing [def, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports.join_ring_quotient_UnitRingQuotient_between_generic_quotient_Quotient_and_GRing_UnitRing [def, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports.join_ring_quotient_UnitRingQuotient_between_GRing_UnitRing_and_ring_quotient_ZmodQuotient [def, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports.join_ring_quotient_UnitRingQuotient_between_ring_quotient_NzRingQuotient_and_GRing_UnitRing [def, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports.unitRingQuotType [abbrev, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.generic_quotient_isEqQuotient_mixin [proj, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.generic_quotient_isQuotient_mixin [proj, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.GRing_Nmodule_isPzSemiRing_mixin [proj, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.GRing_NzRing_hasMulInverse_mixin [proj, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.GRing_PzSemiRing_isNonZero_mixin [proj, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.on [abbrev, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.on_ [abbrev, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.pack_ [def, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.phant_clone [def, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.phant_on_ [def, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.ring_quotient_isNzRingQuotient_mixin [proj, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.ring_quotient_isUnitRingQuotient_mixin [proj, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.ring_quotient_isZmodQuotient_mixin [proj, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.sort [proj, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.type [rec, in mathcomp.algebra.ring_quotient]
UnitRingQuotientElpiOperations [mod, in mathcomp.algebra.ring_quotient]
unitrXz [prf, in mathcomp.algebra.ssrint]
units_Zp [def, in mathcomp.algebra.zmodp]
units_Zp_abelian [prf, in mathcomp.algebra.zmodp]
units_Zp_cyclic [prf, in mathcomp.solvable.cyclic]
units_Zp_group [def, in mathcomp.algebra.zmodp]
unitt [def, in mathcomp.algebra.tensor]
unity_rootE [prf, in mathcomp.algebra.poly]
unity_rootP [prf, in mathcomp.algebra.poly]
UnityRootTheory [mod, in mathcomp.algebra.poly]
UnityRootTheory.eq_prim_root_expr [def, in mathcomp.algebra.poly]
UnityRootTheory.fmorph_primitive_root [def, in mathcomp.algebra.poly]
UnityRootTheory.fmorph_unity_root [def, in mathcomp.algebra.poly]
UnityRootTheory.max_unity_roots [def, in mathcomp.algebra.poly]
UnityRootTheory.mem_unity_roots [def, in mathcomp.algebra.poly]
UnityRootTheory.prim_expr_mod [def, in mathcomp.algebra.poly]
UnityRootTheory.prim_expr_order [abbrev, in mathcomp.algebra.poly]
UnityRootTheory.prim_order_dvd [def, in mathcomp.algebra.poly]
UnityRootTheory.prim_order_exists [def, in mathcomp.algebra.poly]
UnityRootTheory.prim_order_gt0 [abbrev, in mathcomp.algebra.poly]
UnityRootTheory.prim_rootP [def, in mathcomp.algebra.poly]
UnityRootTheory.rmorph_unity_root [def, in mathcomp.algebra.poly]
UnityRootTheory.unity_rootE [def, in mathcomp.algebra.poly]
UnityRootTheory.unity_rootP [def, in mathcomp.algebra.poly]
unitZpE [prf, in mathcomp.algebra.zmodp]
unlift [def, in mathcomp.boot.fintype]
unlift_none [prf, in mathcomp.boot.fintype]
unlift_some [prf, in mathcomp.boot.fintype]
unlift_spec [ind, in mathcomp.boot.fintype]
UnliftNone [constr, in mathcomp.boot.fintype]
unliftP [prf, in mathcomp.boot.fintype]
UnliftSome [constr, in mathcomp.boot.fintype]
unlockable_enum_rank_in [def, in mathcomp.boot.fintype]
unpickle [def, in mathcomp.boot.choice]
unpickle_seq [def, in mathcomp.boot.choice]
unpickle_tagged [def, in mathcomp.boot.choice]
unset1 [def, in mathcomp.boot.finset]
unset10 [prf, in mathcomp.boot.finset]
unset1K [prf, in mathcomp.boot.finset]
unset1N1 [prf, in mathcomp.boot.finset]
unsplit [def, in mathcomp.boot.fintype]
unsplitK [prf, in mathcomp.boot.fintype]
untag [def, in mathcomp.boot.eqtype]
untag_cst [prf, in mathcomp.boot.eqtype]
untag_dflt [prf, in mathcomp.boot.eqtype]
untag_with [def, in mathcomp.boot.eqtype]
untag_with_bij [prf, in mathcomp.boot.eqtype]
untag_withK [prf, in mathcomp.boot.eqtype]
untagE [prf, in mathcomp.boot.eqtype]
unzip1 [def, in mathcomp.boot.seq]
unzip1_map_nth_zip [prf, in mathcomp.boot.seq]
unzip1_zip [prf, in mathcomp.boot.seq]
unzip2 [def, in mathcomp.boot.seq]
unzip2_map_nth_zip [prf, in mathcomp.boot.seq]
unzip2_zip [prf, in mathcomp.boot.seq]
up_expnK [prf, in mathcomp.boot.prime]
up_log [def, in mathcomp.boot.prime]
up_log0 [prf, in mathcomp.boot.prime]
up_log1 [prf, in mathcomp.boot.prime]
up_log2_double [prf, in mathcomp.boot.prime]
up_log2S [prf, in mathcomp.boot.prime]
up_log_bounds [prf, in mathcomp.boot.prime]
up_log_eq [prf, in mathcomp.boot.prime]
up_log_eq0 [prf, in mathcomp.boot.prime]
up_log_gt0 [prf, in mathcomp.boot.prime]
up_log_gtn [prf, in mathcomp.boot.prime]
up_log_min [prf, in mathcomp.boot.prime]
up_log_trunc_log [prf, in mathcomp.boot.prime]
up_logMp [prf, in mathcomp.boot.prime]
up_lognn [prf, in mathcomp.boot.prime]
up_logP [prf, in mathcomp.boot.prime]
uphalf [def, in mathcomp.boot.ssrnat]
uphalf_double [prf, in mathcomp.boot.ssrnat]
uphalf_gt0 [prf, in mathcomp.boot.ssrnat]
uphalf_half [prf, in mathcomp.boot.ssrnat]
uphalf_leq [prf, in mathcomp.boot.ssrnat]
uphalfE [prf, in mathcomp.boot.ssrnat]
uphalfK [prf, in mathcomp.boot.ssrnat]
upper_central_at [def, in mathcomp.solvable.nilpotent]
upper_central_at_group [def, in mathcomp.solvable.nilpotent]
ursubmx [def, in mathcomp.algebra.matrix]
ursubmx_trig [prf, in mathcomp.algebra.matrix]
ursubmxEsub [prf, in mathcomp.algebra.matrix]
usubmx [def, in mathcomp.algebra.matrix]
usubmx_key [prf, in mathcomp.algebra.matrix]
usubmxEsub [prf, in mathcomp.algebra.matrix]
usumx_mul [prf, in mathcomp.group_representation.character]