U (Definitions)
| Files | 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 | _ |
| Definitions | 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 | _ |
| Lemmas | 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 | _ |
| Abbreviations | 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 | _ |
| 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 | _ |
| Notations |
U (Definitions)
ubound [def, in mathcomp.classical.classical_sets]ucn_gFun [def, in mathcomp.solvable.nilpotent]
ucn_igFun [def, in mathcomp.solvable.nilpotent]
ucn_pgFun [def, in mathcomp.solvable.nilpotent]
ucycle [def, in mathcomp.boot.path]
ucycleb [def, in mathcomp.boot.path]
ulsubmx [def, in mathcomp.algebra.matrix]
UMagma.pack_ [def, in mathcomp.boot.monoid]
UMagma.phant_clone [def, in mathcomp.boot.monoid]
UMagma.phant_on_ [def, in mathcomp.boot.monoid]
umagma_closed [def, in mathcomp.boot.monoid]
UMagma_isMonoid.phant_axioms [def, in mathcomp.boot.monoid]
UMagma_isMonoid.phant_Build [def, 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]
UMagmaMorphism.pack_ [def, in mathcomp.boot.monoid]
UMagmaMorphism.phant_clone [def, in mathcomp.boot.monoid]
UMagmaMorphism.phant_on_ [def, in mathcomp.boot.monoid]
unbind [def, in mathcomp.classical.functions]
unbump [def, in mathcomp.boot.fintype]
undup [def, in mathcomp.boot.seq]
unif_continuous [def, in mathcomp.analysis.topology_theory.uniform_structure]
Uniform.pack_ [def, in mathcomp.analysis.topology_theory.uniform_structure]
Uniform.phant_clone [def, in mathcomp.analysis.topology_theory.uniform_structure]
Uniform.phant_on_ [def, in mathcomp.analysis.topology_theory.uniform_structure]
uniform_bounded [def, in mathcomp.analysis.sequences]
uniform_discrete [def, in mathcomp.analysis.topology_theory.discrete_topology]
uniform_fun [def, in mathcomp.analysis.topology_theory.function_spaces]
uniform_fun_family [def, in mathcomp.analysis.topology_theory.function_spaces]
Uniform_isComplete.identity_builder [def, in mathcomp.analysis.topology_theory.uniform_structure]
Uniform_isComplete.phant_axioms [def, in mathcomp.analysis.topology_theory.uniform_structure]
Uniform_isComplete.phant_Build [def, in mathcomp.analysis.topology_theory.uniform_structure]
Uniform_isPseudoMetric.identity_builder [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
Uniform_isPseudoMetric.phant_axioms [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
Uniform_isPseudoMetric.phant_Build [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
Uniform_isTvs.identity_builder [def, in mathcomp.analysis.normedtype_theory.tvs]
Uniform_isTvs.phant_axioms [def, in mathcomp.analysis.normedtype_theory.tvs]
Uniform_isTvs.phant_Build [def, in mathcomp.analysis.normedtype_theory.tvs]
uniform_pdf [def, in mathcomp.analysis.probability_theory.uniform_distribution]
uniform_prob [def, in mathcomp.analysis.probability_theory.uniform_distribution]
uniform_separator [def, in mathcomp.analysis.normedtype_theory.urysohn]
UniformLmodule.Exports.join_tvs_UniformLmodule_between_GRing_Lmodule_and_tvs_UniformNmodule [def, in mathcomp.analysis.normedtype_theory.tvs]
UniformLmodule.Exports.join_tvs_UniformLmodule_between_GRing_Lmodule_and_tvs_UniformZmodule [def, in mathcomp.analysis.normedtype_theory.tvs]
UniformLmodule.Exports.join_tvs_UniformLmodule_between_GRing_LSemiModule_and_tvs_UniformNmodule [def, in mathcomp.analysis.normedtype_theory.tvs]
UniformLmodule.Exports.join_tvs_UniformLmodule_between_GRing_LSemiModule_and_tvs_UniformZmodule [def, in mathcomp.analysis.normedtype_theory.tvs]
UniformLmodule.Exports.join_tvs_UniformLmodule_between_tvs_NbhsLmodule_and_tvs_UniformNmodule [def, in mathcomp.analysis.normedtype_theory.tvs]
UniformLmodule.Exports.join_tvs_UniformLmodule_between_tvs_NbhsLmodule_and_tvs_UniformZmodule [def, in mathcomp.analysis.normedtype_theory.tvs]
UniformLmodule.Exports.join_tvs_UniformLmodule_between_tvs_PreTopologicalLmodule_and_tvs_UniformNmodule [def, in mathcomp.analysis.normedtype_theory.tvs]
UniformLmodule.Exports.join_tvs_UniformLmodule_between_tvs_PreTopologicalLmodule_and_tvs_UniformZmodule [def, in mathcomp.analysis.normedtype_theory.tvs]
UniformLmodule.Exports.join_tvs_UniformLmodule_between_tvs_PreUniformLmodule_and_tvs_UniformNmodule [def, in mathcomp.analysis.normedtype_theory.tvs]
UniformLmodule.Exports.join_tvs_UniformLmodule_between_tvs_PreUniformLmodule_and_tvs_UniformZmodule [def, in mathcomp.analysis.normedtype_theory.tvs]
UniformLmodule.pack_ [def, in mathcomp.analysis.normedtype_theory.tvs]
UniformLmodule.phant_clone [def, in mathcomp.analysis.normedtype_theory.tvs]
UniformLmodule.phant_on_ [def, in mathcomp.analysis.normedtype_theory.tvs]
UniformNmodule.pack_ [def, in mathcomp.analysis.normedtype_theory.tvs]
UniformNmodule.phant_clone [def, in mathcomp.analysis.normedtype_theory.tvs]
UniformNmodule.phant_on_ [def, in mathcomp.analysis.normedtype_theory.tvs]
UniformNmodule_isUniformLmodule.phant_axioms [def, in mathcomp.analysis.normedtype_theory.tvs]
UniformNmodule_isUniformLmodule.phant_Build [def, in mathcomp.analysis.normedtype_theory.tvs]
UniformNmodule_isUniformZmodule.identity_builder [def, in mathcomp.analysis.normedtype_theory.tvs]
UniformNmodule_isUniformZmodule.phant_axioms [def, in mathcomp.analysis.normedtype_theory.tvs]
UniformNmodule_isUniformZmodule.phant_Build [def, in mathcomp.analysis.normedtype_theory.tvs]
UniformZmodule.Exports.join_tvs_UniformZmodule_between_Algebra_BaseZmodule_and_tvs_UniformNmodule [def, in mathcomp.analysis.normedtype_theory.tvs]
UniformZmodule.Exports.join_tvs_UniformZmodule_between_pseudometric_normed_Zmodule_NbhsZmodule_and_tvs_UniformNmodule [def, in mathcomp.analysis.normedtype_theory.tvs]
UniformZmodule.Exports.join_tvs_UniformZmodule_between_pseudometric_normed_Zmodule_PreTopologicalZmodule_and_tvs_UniformNmodule [def, in mathcomp.analysis.normedtype_theory.tvs]
UniformZmodule.Exports.join_tvs_UniformZmodule_between_pseudometric_normed_Zmodule_PreUniformZmodule_and_tvs_UniformNmodule [def, in mathcomp.analysis.normedtype_theory.tvs]
UniformZmodule.Exports.join_tvs_UniformZmodule_between_tvs_UniformNmodule_and_Algebra_Zmodule [def, in mathcomp.analysis.normedtype_theory.tvs]
UniformZmodule.pack_ [def, in mathcomp.analysis.normedtype_theory.tvs]
UniformZmodule.phant_clone [def, in mathcomp.analysis.normedtype_theory.tvs]
UniformZmodule.phant_on_ [def, in mathcomp.analysis.normedtype_theory.tvs]
uniq [def, in mathcomp.boot.seq]
uniq_roots [def, in mathcomp.algebra.poly]
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_keyed [def, in mathcomp.algebra.spectral]
unitmx [def, in mathcomp.algebra.matrix]
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.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]
units_Zp [def, in mathcomp.algebra.zmodp]
units_Zp_group [def, in mathcomp.algebra.zmodp]
unitt [def, in mathcomp.algebra.tensor]
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_order_dvd [def, in mathcomp.algebra.poly]
UnityRootTheory.prim_order_exists [def, 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]
unlift [def, in mathcomp.boot.fintype]
unlockable_enum_rank_in [def, in mathcomp.boot.fintype]
unpickle [def, in mathcomp.finmap.finmap]
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]
unsplit [def, in mathcomp.boot.fintype]
unsquash [def, in mathcomp.classical.classical_sets]
untag [def, in mathcomp.boot.eqtype]
untag_with [def, in mathcomp.boot.eqtype]
unzip1 [def, in mathcomp.boot.seq]
unzip2 [def, in mathcomp.boot.seq]
up_log [def, in mathcomp.boot.prime]
uphalf [def, in mathcomp.boot.ssrnat]
upper_bound [def, in mathcomp.classical.wochoice]
upper_central_at [def, in mathcomp.solvable.nilpotent]
upper_central_at_group [def, in mathcomp.solvable.nilpotent]
ursubmx [def, in mathcomp.algebra.matrix]
Urysohn [def, in mathcomp.analysis.normedtype_theory.urysohn]
urysohnType [def, in mathcomp.analysis.normedtype_theory.urysohn]
usubmx [def, in mathcomp.algebra.matrix]