| 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 | (72861 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 | (2184 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 | (2366 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 | (9859 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 | (106 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 | (15730 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 | (72 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 | (239 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 | (139 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 | (3716 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 | (2702 entries) |
| Instance 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 | (3 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 | (1171 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 | (33700 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 | (874 entries) |
U
UbnEq [constructor, in mathcomp.boot.ssrnat]UbnGeq [constructor, in mathcomp.boot.ssrnat]
UbnLeq [constructor, in mathcomp.boot.ssrnat]
ubnP [lemma, in mathcomp.boot.ssrnat]
ubnPeq [lemma, in mathcomp.boot.ssrnat]
ubnPgeq [lemma, in mathcomp.boot.ssrnat]
ubnPleq [lemma, in mathcomp.boot.ssrnat]
ubn_eq_spec [inductive, in mathcomp.boot.ssrnat]
ubn_geq_spec [inductive, in mathcomp.boot.ssrnat]
ubn_leq_spec [inductive, in mathcomp.boot.ssrnat]
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_pgFun [definition, in mathcomp.solvable.nilpotent]
ucn_gFun [definition, in mathcomp.solvable.nilpotent]
ucn_igFun [definition, 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.boot.path]
ucycleb [definition, in mathcomp.boot.path]
ucycle_uniq [lemma, in mathcomp.boot.path]
ucycle_cycle [lemma, in mathcomp.boot.path]
ufcycle [abbreviation, in mathcomp.boot.path]
ulsubmx [definition, in mathcomp.algebra.matrix]
ulsubmxEsub [lemma, in mathcomp.algebra.matrix]
ulsubmx_diag [lemma, in mathcomp.algebra.matrix]
ulsubmx_trig [lemma, in mathcomp.algebra.matrix]
UMagma [module, in mathcomp.boot.monoid]
UMagmaClosed [module, in mathcomp.boot.monoid]
UMagmaClosedElpiOperations [module, in mathcomp.boot.monoid]
UMagmaClosed.axioms_ [record, in mathcomp.boot.monoid]
UMagmaClosed.class [projection, in mathcomp.boot.monoid]
UMagmaClosed.Exports [module, in mathcomp.boot.monoid]
UMagmaClosed.Exports.monoid_UMagmaClosed__to__monoid_MulClosed [definition, in mathcomp.boot.monoid]
UMagmaClosed.Exports.monoid_UMagmaClosed_class__to__monoid_MulClosed_class [definition, in mathcomp.boot.monoid]
UMagmaClosed.monoid_isMulClosed_mixin [projection, in mathcomp.boot.monoid]
UMagmaClosed.monoid_isMul1Closed_mixin [projection, in mathcomp.boot.monoid]
UMagmaClosed.pack_ [definition, in mathcomp.boot.monoid]
UMagmaClosed.phant_on_ [definition, in mathcomp.boot.monoid]
UMagmaClosed.phant_clone [definition, in mathcomp.boot.monoid]
UMagmaClosed.sort [projection, in mathcomp.boot.monoid]
UMagmaClosed.type [record, in mathcomp.boot.monoid]
UMagmaElpiOperations [module, in mathcomp.boot.monoid]
UMagmaMorphism [module, in mathcomp.boot.monoid]
UMagmaMorphismElpiOperations [module, in mathcomp.boot.monoid]
UMagmaMorphism.axioms_ [record, in mathcomp.boot.monoid]
UMagmaMorphism.class [projection, in mathcomp.boot.monoid]
UMagmaMorphism.Exports [module, in mathcomp.boot.monoid]
UMagmaMorphism.Exports.monoid_UMagmaMorphism__to__monoid_Multiplicative [definition, in mathcomp.boot.monoid]
UMagmaMorphism.Exports.monoid_UMagmaMorphism_class__to__monoid_Multiplicative_class [definition, in mathcomp.boot.monoid]
UMagmaMorphism.monoid_isMultiplicative_mixin [projection, in mathcomp.boot.monoid]
UMagmaMorphism.monoid_Multiplicative_isUMagmaMorphism_mixin [projection, in mathcomp.boot.monoid]
UMagmaMorphism.pack_ [definition, in mathcomp.boot.monoid]
UMagmaMorphism.phant_on_ [definition, in mathcomp.boot.monoid]
UMagmaMorphism.phant_clone [definition, in mathcomp.boot.monoid]
UMagmaMorphism.sort [projection, in mathcomp.boot.monoid]
UMagmaMorphism.type [record, in mathcomp.boot.monoid]
UMagmaPred [section, in mathcomp.boot.monoid]
UMagmaPred.G [variable, in mathcomp.boot.monoid]
UMagmaPred.UMagma [section, in mathcomp.boot.monoid]
UMagmaPred.UMagma.S [variable, in mathcomp.boot.monoid]
UMagmaTheory [section, in mathcomp.boot.monoid]
UMagmaTheory.G [variable, in mathcomp.boot.monoid]
UMagma_isMonoid.Exports [module, in mathcomp.boot.monoid]
UMagma_isMonoid.phant_axioms [definition, in mathcomp.boot.monoid]
UMagma_isMonoid.phant_Build [definition, in mathcomp.boot.monoid]
UMagma_isMonoid.mulgA [projection, in mathcomp.boot.monoid]
UMagma_isMonoid.axioms_ [record, in mathcomp.boot.monoid]
UMagma_isMonoid.UMagma_isMonoid_G__canonical__monoid_UMagma [definition, in mathcomp.boot.monoid]
UMagma_isMonoid.UMagma_isMonoid.local_mixin_monoid_BaseUMagma_isUMagma [variable, in mathcomp.boot.monoid]
UMagma_isMonoid.UMagma_isMonoid_G__canonical__monoid_ChoiceBaseUMagma [definition, in mathcomp.boot.monoid]
UMagma_isMonoid.UMagma_isMonoid_G__canonical__monoid_BaseUMagma [definition, in mathcomp.boot.monoid]
UMagma_isMonoid.UMagma_isMonoid_G__canonical__monoid_ChoiceMagma [definition, in mathcomp.boot.monoid]
UMagma_isMonoid.UMagma_isMonoid_G__canonical__monoid_Magma [definition, in mathcomp.boot.monoid]
UMagma_isMonoid.UMagma_isMonoid.local_mixin_monoid_hasMul [variable, in mathcomp.boot.monoid]
UMagma_isMonoid.UMagma_isMonoid_G__canonical__choice_Choice [definition, in mathcomp.boot.monoid]
UMagma_isMonoid.UMagma_isMonoid_G__canonical__eqtype_Equality [definition, in mathcomp.boot.monoid]
UMagma_isMonoid.UMagma_isMonoid.local_mixin_eqtype_hasDecEq [variable, in mathcomp.boot.monoid]
UMagma_isMonoid.UMagma_isMonoid.local_mixin_choice_hasChoice [variable, in mathcomp.boot.monoid]
UMagma_isMonoid.UMagma_isMonoid.local_mixin_monoid_hasOne [variable, in mathcomp.boot.monoid]
UMagma_isMonoid.UMagma_isMonoid.G [variable, in mathcomp.boot.monoid]
UMagma_isMonoid.UMagma_isMonoid.UMagma_isMonoid [section, in mathcomp.boot.monoid]
UMagma_isMonoid [module, in mathcomp.boot.monoid]
umagma_closed [definition, in mathcomp.boot.monoid]
UMagma.axioms_ [record, in mathcomp.boot.monoid]
UMagma.choice_hasChoice_mixin [projection, in mathcomp.boot.monoid]
UMagma.class [projection, in mathcomp.boot.monoid]
UMagma.eqtype_hasDecEq_mixin [projection, in mathcomp.boot.monoid]
UMagma.Exports [module, in mathcomp.boot.monoid]
UMagma.Exports.monoid_UMagma__to__monoid_ChoiceBaseUMagma [definition, in mathcomp.boot.monoid]
UMagma.Exports.monoid_UMagma_class__to__monoid_ChoiceBaseUMagma_class [definition, in mathcomp.boot.monoid]
UMagma.Exports.monoid_UMagma__to__monoid_ChoiceMagma [definition, in mathcomp.boot.monoid]
UMagma.Exports.monoid_UMagma_class__to__monoid_ChoiceMagma_class [definition, in mathcomp.boot.monoid]
UMagma.Exports.monoid_UMagma__to__choice_Choice [definition, in mathcomp.boot.monoid]
UMagma.Exports.monoid_UMagma_class__to__choice_Choice_class [definition, in mathcomp.boot.monoid]
UMagma.Exports.monoid_UMagma__to__eqtype_Equality [definition, in mathcomp.boot.monoid]
UMagma.Exports.monoid_UMagma_class__to__eqtype_Equality_class [definition, in mathcomp.boot.monoid]
UMagma.Exports.monoid_UMagma__to__monoid_BaseUMagma [definition, in mathcomp.boot.monoid]
UMagma.Exports.monoid_UMagma_class__to__monoid_BaseUMagma_class [definition, in mathcomp.boot.monoid]
UMagma.Exports.monoid_UMagma__to__monoid_Magma [definition, in mathcomp.boot.monoid]
UMagma.Exports.monoid_UMagma_class__to__monoid_Magma_class [definition, in mathcomp.boot.monoid]
UMagma.monoid_BaseUMagma_isUMagma_mixin [projection, in mathcomp.boot.monoid]
UMagma.monoid_hasMul_mixin [projection, in mathcomp.boot.monoid]
UMagma.monoid_hasOne_mixin [projection, in mathcomp.boot.monoid]
UMagma.pack_ [definition, in mathcomp.boot.monoid]
UMagma.phant_on_ [definition, in mathcomp.boot.monoid]
UMagma.phant_clone [definition, in mathcomp.boot.monoid]
UMagma.sort [projection, in mathcomp.boot.monoid]
UMagma.type [record, in mathcomp.boot.monoid]
unbump [definition, in mathcomp.boot.fintype]
unbumpDl [lemma, in mathcomp.boot.fintype]
unbumpK [lemma, in mathcomp.boot.fintype]
unbumpKcond [lemma, in mathcomp.boot.fintype]
unbumpS [lemma, in mathcomp.boot.fintype]
undup [definition, in mathcomp.boot.seq]
undup_flatten_nseq [lemma, in mathcomp.boot.seq]
undup_map_inj [lemma, in mathcomp.boot.seq]
undup_subseq [lemma, in mathcomp.boot.seq]
undup_rcons [lemma, in mathcomp.boot.seq]
undup_cat [lemma, in mathcomp.boot.seq]
undup_nil [lemma, in mathcomp.boot.seq]
undup_id [lemma, in mathcomp.boot.seq]
undup_uniq [lemma, in mathcomp.boot.seq]
undup_sorted [lemma, in mathcomp.boot.path]
undup_path [lemma, in mathcomp.boot.path]
undup_cycle_cons [lemma, in mathcomp.boot.fingraph]
Unify [projection, in mathcomp.algebra.interval_inference]
unify [record, in mathcomp.algebra.interval_inference]
Unify [constructor, in mathcomp.algebra.interval_inference]
unify [inductive, in mathcomp.algebra.interval_inference]
unify_itv [abbreviation, in mathcomp.algebra.interval_inference]
Unify' [projection, in mathcomp.algebra.interval_inference]
unify' [record, in mathcomp.algebra.interval_inference]
Unify' [constructor, in mathcomp.algebra.interval_inference]
unify' [inductive, in mathcomp.algebra.interval_inference]
unify'P [instance, in mathcomp.algebra.interval_inference]
uniq [definition, in mathcomp.boot.seq]
UniqCycle [section, in mathcomp.boot.path]
UniqCycleRev [section, in mathcomp.boot.path]
UniqCycleRev.T [variable, in mathcomp.boot.path]
UniqCycle.e [variable, in mathcomp.boot.path]
UniqCycle.n0 [variable, in mathcomp.boot.path]
UniqCycle.p [variable, in mathcomp.boot.path]
UniqCycle.T [variable, in mathcomp.boot.path]
UniqCycle.Up [variable, in mathcomp.boot.path]
uniqP [lemma, in mathcomp.boot.seq]
uniqPn [lemma, in mathcomp.boot.seq]
UniqRotrCycle [section, in mathcomp.boot.path]
UniqRotrCycle.n0 [variable, in mathcomp.boot.path]
UniqRotrCycle.p [variable, in mathcomp.boot.path]
UniqRotrCycle.T [variable, in mathcomp.boot.path]
UniqRotrCycle.Up [variable, in mathcomp.boot.path]
uniq_sub_le_big_cond [lemma, in mathcomp.boot.bigop]
uniq_sub_le_big [lemma, in mathcomp.boot.bigop]
uniq_traject_porbit [lemma, in mathcomp.fingroup.perm]
uniq_pairwise [lemma, in mathcomp.boot.seq]
uniq_subseq_pivot [lemma, in mathcomp.boot.seq]
uniq_perm [lemma, in mathcomp.boot.seq]
uniq_min_size [lemma, in mathcomp.boot.seq]
uniq_size_uniq [lemma, in mathcomp.boot.seq]
uniq_leq_size [lemma, in mathcomp.boot.seq]
uniq_eqseq_pivotr [lemma, in mathcomp.boot.seq]
uniq_eqseq_pivotl [lemma, in mathcomp.boot.seq]
uniq_catCA [lemma, in mathcomp.boot.seq]
uniq_catC [lemma, in mathcomp.boot.seq]
uniq_normal_Hall [lemma, in mathcomp.solvable.pgroup]
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]
unitarymx [definition, in mathcomp.algebra.spectral]
unitarymx [section, in mathcomp.algebra.spectral]
unitarymxP [lemma, in mathcomp.algebra.spectral]
unitarymx_unit [lemma, in mathcomp.algebra.spectral]
unitarymx_keyed [definition, in mathcomp.algebra.spectral]
unitarymx_key [lemma, in mathcomp.algebra.spectral]
unitarymx.C [variable, in mathcomp.algebra.spectral]
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]
UnitRingQuotient [module, in mathcomp.algebra.ring_quotient]
UnitRingQuotientElpiOperations [module, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Algebra_AddMagma_isAddSemigroup_mixin [projection, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Algebra_BaseAddMagma_isAddMagma_mixin [projection, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Algebra_BaseAddUMagma_isAddUMagma_mixin [projection, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Algebra_BaseZmoduleNmodule_isZmodule_mixin [projection, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Algebra_hasAdd_mixin [projection, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Algebra_hasZero_mixin [projection, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Algebra_hasOpp_mixin [projection, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.axioms_ [record, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.choice_hasChoice_mixin [projection, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.class [projection, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.eqtype_hasDecEq_mixin [projection, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports [module, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports.join_ring_quotient_UnitRingQuotient_between_ring_quotient_NzRingQuotient_and_GRing_UnitRing [definition, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports.join_ring_quotient_UnitRingQuotient_between_GRing_UnitRing_and_ring_quotient_ZmodQuotient [definition, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports.join_ring_quotient_UnitRingQuotient_between_generic_quotient_EqQuotient_and_GRing_UnitRing [definition, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports.join_ring_quotient_UnitRingQuotient_between_generic_quotient_Quotient_and_GRing_UnitRing [definition, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports.ring_quotient_UnitRingQuotient__to__ring_quotient_NzRingQuotient [definition, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports.ring_quotient_UnitRingQuotient_class__to__ring_quotient_NzRingQuotient_class [definition, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports.ring_quotient_UnitRingQuotient__to__GRing_UnitRing [definition, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports.ring_quotient_UnitRingQuotient_class__to__GRing_UnitRing_class [definition, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports.ring_quotient_UnitRingQuotient__to__GRing_NzRing [definition, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports.ring_quotient_UnitRingQuotient_class__to__GRing_NzRing_class [definition, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports.ring_quotient_UnitRingQuotient__to__GRing_NzSemiRing [definition, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports.ring_quotient_UnitRingQuotient_class__to__GRing_NzSemiRing_class [definition, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports.ring_quotient_UnitRingQuotient__to__GRing_PzRing [definition, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports.ring_quotient_UnitRingQuotient_class__to__GRing_PzRing_class [definition, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports.ring_quotient_UnitRingQuotient__to__GRing_PzSemiRing [definition, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports.ring_quotient_UnitRingQuotient_class__to__GRing_PzSemiRing_class [definition, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports.ring_quotient_UnitRingQuotient__to__ring_quotient_ZmodQuotient [definition, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports.ring_quotient_UnitRingQuotient_class__to__ring_quotient_ZmodQuotient_class [definition, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports.ring_quotient_UnitRingQuotient__to__Algebra_Zmodule [definition, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports.ring_quotient_UnitRingQuotient_class__to__Algebra_Zmodule_class [definition, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports.ring_quotient_UnitRingQuotient__to__Algebra_Nmodule [definition, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports.ring_quotient_UnitRingQuotient_class__to__Algebra_Nmodule_class [definition, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports.ring_quotient_UnitRingQuotient__to__Algebra_AddSemigroup [definition, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports.ring_quotient_UnitRingQuotient_class__to__Algebra_AddSemigroup_class [definition, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports.ring_quotient_UnitRingQuotient__to__Algebra_AddUMagma [definition, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports.ring_quotient_UnitRingQuotient_class__to__Algebra_AddUMagma_class [definition, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports.ring_quotient_UnitRingQuotient__to__Algebra_AddMagma [definition, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports.ring_quotient_UnitRingQuotient_class__to__Algebra_AddMagma_class [definition, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports.ring_quotient_UnitRingQuotient__to__Algebra_ChoiceBaseAddUMagma [definition, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports.ring_quotient_UnitRingQuotient_class__to__Algebra_ChoiceBaseAddUMagma_class [definition, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports.ring_quotient_UnitRingQuotient__to__Algebra_ChoiceBaseAddMagma [definition, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports.ring_quotient_UnitRingQuotient_class__to__Algebra_ChoiceBaseAddMagma_class [definition, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports.ring_quotient_UnitRingQuotient__to__choice_Choice [definition, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports.ring_quotient_UnitRingQuotient_class__to__choice_Choice_class [definition, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports.ring_quotient_UnitRingQuotient__to__generic_quotient_EqQuotient [definition, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports.ring_quotient_UnitRingQuotient_class__to__generic_quotient_EqQuotient_class [definition, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports.ring_quotient_UnitRingQuotient__to__eqtype_Equality [definition, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports.ring_quotient_UnitRingQuotient_class__to__eqtype_Equality_class [definition, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports.ring_quotient_UnitRingQuotient__to__Algebra_BaseZmodule [definition, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports.ring_quotient_UnitRingQuotient_class__to__Algebra_BaseZmodule_class [definition, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports.ring_quotient_UnitRingQuotient__to__Algebra_BaseAddUMagma [definition, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports.ring_quotient_UnitRingQuotient_class__to__Algebra_BaseAddUMagma_class [definition, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports.ring_quotient_UnitRingQuotient__to__Algebra_BaseAddMagma [definition, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports.ring_quotient_UnitRingQuotient_class__to__Algebra_BaseAddMagma_class [definition, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports.ring_quotient_UnitRingQuotient__to__generic_quotient_Quotient [definition, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports.ring_quotient_UnitRingQuotient_class__to__generic_quotient_Quotient_class [definition, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.generic_quotient_isEqQuotient_mixin [projection, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.generic_quotient_isQuotient_mixin [projection, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.GRing_NzRing_hasMulInverse_mixin [projection, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.GRing_PzSemiRing_isNonZero_mixin [projection, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.GRing_Nmodule_isPzSemiRing_mixin [projection, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.pack_ [definition, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.phant_on_ [definition, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.phant_clone [definition, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.ring_quotient_isUnitRingQuotient_mixin [projection, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.ring_quotient_isNzRingQuotient_mixin [projection, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.ring_quotient_isZmodQuotient_mixin [projection, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.sort [projection, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.type [record, 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_group [definition, in mathcomp.algebra.zmodp]
units_Zp [definition, in mathcomp.algebra.zmodp]
units_Zp_cyclic [lemma, in mathcomp.solvable.cyclic]
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_Zp_expg [lemma, in mathcomp.algebra.zmodp]
unit_Zp_mulgC [lemma, in mathcomp.algebra.zmodp]
unit_enumP [lemma, in mathcomp.boot.fintype]
unit_eqP [lemma, in mathcomp.boot.eqtype]
unlift [definition, in mathcomp.boot.fintype]
UnliftNone [constructor, in mathcomp.boot.fintype]
unliftP [lemma, in mathcomp.boot.fintype]
UnliftSome [constructor, in mathcomp.boot.fintype]
unlift_some [lemma, in mathcomp.boot.fintype]
unlift_none [lemma, in mathcomp.boot.fintype]
unlift_spec [inductive, in mathcomp.boot.fintype]
unlift_subproof [lemma, in mathcomp.boot.fintype]
unlockable_enum_rank_in [definition, in mathcomp.boot.fintype]
Unnamed_thm [definition, in mathcomp.algebra.interval_inference]
Unnamed_thm [definition, in mathcomp.algebra.interval_inference]
Unnamed_thm [definition, in mathcomp.algebra.interval_inference]
Unnamed_thm [definition, in mathcomp.algebra.interval_inference]
unpickle [definition, in mathcomp.boot.choice]
unpickle_tagged [definition, in mathcomp.boot.choice]
unpickle_seq [definition, in mathcomp.boot.choice]
unset1 [definition, in mathcomp.boot.finset]
unset1 [section, in mathcomp.boot.finset]
unset1K [lemma, in mathcomp.boot.finset]
unset1N1 [lemma, in mathcomp.boot.finset]
unset1.I [variable, in mathcomp.boot.finset]
unset10 [lemma, in mathcomp.boot.finset]
unsplit [definition, in mathcomp.boot.fintype]
unsplitK [lemma, in mathcomp.boot.fintype]
untag [definition, in mathcomp.boot.eqtype]
untagE [lemma, in mathcomp.boot.eqtype]
untag_cst [lemma, in mathcomp.boot.eqtype]
untag_dflt [lemma, in mathcomp.boot.eqtype]
untag_with_bij [lemma, in mathcomp.boot.eqtype]
untag_withK [lemma, in mathcomp.boot.eqtype]
untag_with [definition, in mathcomp.boot.eqtype]
unzip1 [definition, in mathcomp.boot.seq]
unzip1_map_nth_zip [lemma, in mathcomp.boot.seq]
unzip1_zip [lemma, in mathcomp.boot.seq]
unzip2 [definition, in mathcomp.boot.seq]
unzip2_map_nth_zip [lemma, in mathcomp.boot.seq]
unzip2_zip [lemma, in mathcomp.boot.seq]
uphalf [definition, in mathcomp.boot.ssrnat]
uphalfE [lemma, in mathcomp.boot.ssrnat]
uphalfK [lemma, in mathcomp.boot.ssrnat]
uphalf_gt0 [lemma, in mathcomp.boot.ssrnat]
uphalf_leq [lemma, in mathcomp.boot.ssrnat]
uphalf_half [lemma, in mathcomp.boot.ssrnat]
uphalf_double [lemma, in mathcomp.boot.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_group [definition, in mathcomp.solvable.nilpotent]
upper_central_at [definition, in mathcomp.solvable.nilpotent]
up_log_trunc_log [lemma, in mathcomp.boot.prime]
up_log2S [lemma, in mathcomp.boot.prime]
up_log2_double [lemma, in mathcomp.boot.prime]
up_logMp [lemma, in mathcomp.boot.prime]
up_expnK [lemma, in mathcomp.boot.prime]
up_lognn [lemma, in mathcomp.boot.prime]
up_log_eq [lemma, in mathcomp.boot.prime]
up_log_min [lemma, in mathcomp.boot.prime]
up_log_gtn [lemma, in mathcomp.boot.prime]
up_logP [lemma, in mathcomp.boot.prime]
up_log_bounds [lemma, in mathcomp.boot.prime]
up_log_gt0 [lemma, in mathcomp.boot.prime]
up_log_eq0 [lemma, in mathcomp.boot.prime]
up_log1 [lemma, in mathcomp.boot.prime]
up_log0 [lemma, in mathcomp.boot.prime]
up_log [definition, in mathcomp.boot.prime]
ursubmx [definition, in mathcomp.algebra.matrix]
ursubmxEsub [lemma, in mathcomp.algebra.matrix]
ursubmx_trig [lemma, in mathcomp.algebra.matrix]
UseFinTuple [section, in mathcomp.boot.tuple]
UseFinTuple.ImageTuple [section, in mathcomp.boot.tuple]
UseFinTuple.ImageTuple.A [variable, in mathcomp.boot.tuple]
UseFinTuple.ImageTuple.f [variable, in mathcomp.boot.tuple]
UseFinTuple.ImageTuple.T' [variable, in mathcomp.boot.tuple]
UseFinTuple.MkTuple [section, in mathcomp.boot.tuple]
UseFinTuple.MkTuple.f [variable, in mathcomp.boot.tuple]
UseFinTuple.MkTuple.T' [variable, in mathcomp.boot.tuple]
UseFinTuple.n [variable, in mathcomp.boot.tuple]
UseFinTuple.T [variable, in mathcomp.boot.tuple]
usubmx [definition, in mathcomp.algebra.matrix]
usubmxEsub [lemma, 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 | (72861 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 | (2184 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 | (2366 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 | (9859 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 | (106 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 | (15730 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 | (72 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 | (239 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 | (139 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 | (3716 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 | (2702 entries) |
| Instance 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 | (3 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 | (1171 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 | (33700 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 | (874 entries) |