U (Abbreviations)
| 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 (Abbreviations)
u_cons [abbrev, in mathcomp.algebra.tensor]u_cons [abbrev, in mathcomp.algebra.tensor]
ub_ereal_sup [abbrev, in mathcomp.analysis.ereal]
ufcycle [abbrev, in mathcomp.boot.path]
UMagma [abbrev, in mathcomp.boot.monoid]
UMagma.clone [abbrev, in mathcomp.boot.monoid]
UMagma.copy [abbrev, in mathcomp.boot.monoid]
UMagma.Exports.umagmaType [abbrev, in mathcomp.boot.monoid]
UMagma.on [abbrev, in mathcomp.boot.monoid]
UMagma.on_ [abbrev, in mathcomp.boot.monoid]
UMagma_isMonoid [abbrev, in mathcomp.boot.monoid]
UMagma_isMonoid.axioms [abbrev, in mathcomp.boot.monoid]
UMagma_isMonoid.Build [abbrev, in mathcomp.boot.monoid]
UMagmaClosed [abbrev, in mathcomp.boot.monoid]
UMagmaClosed.clone [abbrev, in mathcomp.boot.monoid]
UMagmaClosed.copy [abbrev, in mathcomp.boot.monoid]
UMagmaClosed.Exports.umagmaClosed [abbrev, in mathcomp.boot.monoid]
UMagmaClosed.on [abbrev, in mathcomp.boot.monoid]
UMagmaClosed.on_ [abbrev, in mathcomp.boot.monoid]
UMagmaMorphism [abbrev, in mathcomp.boot.monoid]
UMagmaMorphism.clone [abbrev, in mathcomp.boot.monoid]
UMagmaMorphism.copy [abbrev, in mathcomp.boot.monoid]
UMagmaMorphism.on [abbrev, in mathcomp.boot.monoid]
UMagmaMorphism.on_ [abbrev, in mathcomp.boot.monoid]
Uniform [abbrev, in mathcomp.analysis.topology_theory.uniform_structure]
Uniform.clone [abbrev, in mathcomp.analysis.topology_theory.uniform_structure]
Uniform.copy [abbrev, in mathcomp.analysis.topology_theory.uniform_structure]
Uniform.Exports.uniformType [abbrev, in mathcomp.analysis.topology_theory.uniform_structure]
Uniform.on [abbrev, in mathcomp.analysis.topology_theory.uniform_structure]
Uniform.on_ [abbrev, in mathcomp.analysis.topology_theory.uniform_structure]
Uniform_isComplete [abbrev, in mathcomp.analysis.topology_theory.uniform_structure]
Uniform_isComplete.axioms [abbrev, in mathcomp.analysis.topology_theory.uniform_structure]
Uniform_isComplete.Build [abbrev, in mathcomp.analysis.topology_theory.uniform_structure]
Uniform_isPseudoMetric [abbrev, in mathcomp.analysis.topology_theory.pseudometric_structure]
Uniform_isPseudoMetric.axioms [abbrev, in mathcomp.analysis.topology_theory.pseudometric_structure]
Uniform_isPseudoMetric.Build [abbrev, in mathcomp.analysis.topology_theory.pseudometric_structure]
Uniform_isTvs [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
Uniform_isTvs.axioms [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
Uniform_isTvs.Build [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
UniformLmodule [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
UniformLmodule.clone [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
UniformLmodule.copy [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
UniformLmodule.on [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
UniformLmodule.on_ [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
UniformNmodule [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
UniformNmodule.clone [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
UniformNmodule.copy [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
UniformNmodule.on [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
UniformNmodule.on_ [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
UniformNmodule_isUniformLmodule [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
UniformNmodule_isUniformLmodule.axioms [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
UniformNmodule_isUniformLmodule.Build [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
UniformNmodule_isUniformZmodule [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
UniformNmodule_isUniformZmodule.axioms [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
UniformNmodule_isUniformZmodule.Build [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
UniformZmodule [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
UniformZmodule.clone [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
UniformZmodule.copy [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
UniformZmodule.on [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
UniformZmodule.on_ [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
unify_itv [abbrev, in mathcomp.algebra.interval_inference]
unify_nz [abbrev, in mathcomp.reals.signed]
unify_r [abbrev, in mathcomp.reals.signed]
UnitAlgebra_isFalgebra [abbrev, in mathcomp.field.falgebra]
UnitAlgebra_isFalgebra.axioms [abbrev, in mathcomp.field.falgebra]
UnitAlgebra_isFalgebra.Build [abbrev, in mathcomp.field.falgebra]
UnitRingQuotient [abbrev, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.clone [abbrev, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.copy [abbrev, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports.unitRingQuotType [abbrev, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.on [abbrev, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.on_ [abbrev, in mathcomp.algebra.ring_quotient]
UnityRootTheory.prim_expr_order [abbrev, in mathcomp.algebra.poly]
UnityRootTheory.prim_order_gt0 [abbrev, in mathcomp.algebra.poly]