mathcomp.ssreflect.tuple

Global Index

Y

_

(54001 entries)

Notation Index

J

T

W

X

Y

_

(1931 entries)

Module Index

J

K

W

X

Y

_

other

(1658 entries)

Variable Index

J

W

X

Y

_

other

(7199 entries)

Library Index

K

L

U

W

X

Y

_

other

(97 entries)

Lemma Index

Y

_

other

(15214 entries)

Axiom Index

H

J

K

L

N

O

T

U

V

W

X

Y

Z

_

other

(75 entries)

Constructor Index

J

K

W

Y

_

other

(224 entries)

Inductive Index

J

K

Q

W

Y

Z

_

other

(132 entries)

Projection Index

J

K

W

X

Y

_

other

(2371 entries)

Section Index

J

W

X

Y

_

other

(2266 entries)

Abbreviation Index

Y

_

other

(732 entries)

Definition Index

Y

_

other

(21455 entries)

Record Index

J

K

W

X

Y

_

other

(647 entries)

U

UbnEq [constructor, in mathcomp.ssreflect.ssrnat]
UbnGeq [constructor, in mathcomp.ssreflect.ssrnat]
UbnLeq [constructor, in mathcomp.ssreflect.ssrnat]
ubnP [lemma, in mathcomp.ssreflect.ssrnat]
ubnPeq [lemma, in mathcomp.ssreflect.ssrnat]
ubnPgeq [lemma, in mathcomp.ssreflect.ssrnat]
ubnPleq [lemma, in mathcomp.ssreflect.ssrnat]
ubn_eq_spec [inductive, in mathcomp.ssreflect.ssrnat]
ubn_geq_spec [inductive, in mathcomp.ssreflect.ssrnat]
ubn_leq_spec [inductive, in mathcomp.ssreflect.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.ssreflect.path]
ucycleb [definition, in mathcomp.ssreflect.path]
ucycle_uniq [lemma, in mathcomp.ssreflect.path]
ucycle_cycle [lemma, in mathcomp.ssreflect.path]
ufcycle [abbreviation, in mathcomp.ssreflect.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]
unbump [definition, in mathcomp.ssreflect.fintype]
unbumpDl [lemma, in mathcomp.ssreflect.fintype]
unbumpK [lemma, in mathcomp.ssreflect.fintype]
unbumpKcond [lemma, in mathcomp.ssreflect.fintype]
unbumpS [lemma, in mathcomp.ssreflect.fintype]
undup [definition, in mathcomp.ssreflect.seq]
undup_flatten_nseq [lemma, in mathcomp.ssreflect.seq]
undup_map_inj [lemma, in mathcomp.ssreflect.seq]
undup_subseq [lemma, in mathcomp.ssreflect.seq]
undup_rcons [lemma, in mathcomp.ssreflect.seq]
undup_cat [lemma, in mathcomp.ssreflect.seq]
undup_nil [lemma, in mathcomp.ssreflect.seq]
undup_id [lemma, in mathcomp.ssreflect.seq]
undup_uniq [lemma, in mathcomp.ssreflect.seq]
undup_sorted [lemma, in mathcomp.ssreflect.path]
undup_path [lemma, in mathcomp.ssreflect.path]
undup_cycle_cons [lemma, in mathcomp.ssreflect.fingraph]
uniq [definition, in mathcomp.ssreflect.seq]
UniqCycle [section, in mathcomp.ssreflect.path]
UniqCycleRev [section, in mathcomp.ssreflect.path]
UniqCycleRev.T [variable, in mathcomp.ssreflect.path]
UniqCycle.e [variable, in mathcomp.ssreflect.path]
UniqCycle.n0 [variable, in mathcomp.ssreflect.path]
UniqCycle.p [variable, in mathcomp.ssreflect.path]
UniqCycle.T [variable, in mathcomp.ssreflect.path]
UniqCycle.Up [variable, in mathcomp.ssreflect.path]
uniqP [lemma, in mathcomp.ssreflect.seq]
uniqPn [lemma, in mathcomp.ssreflect.seq]
UniqRotrCycle [section, in mathcomp.ssreflect.path]
UniqRotrCycle.n0 [variable, in mathcomp.ssreflect.path]
UniqRotrCycle.p [variable, in mathcomp.ssreflect.path]
UniqRotrCycle.T [variable, in mathcomp.ssreflect.path]
UniqRotrCycle.Up [variable, in mathcomp.ssreflect.path]
uniq_traject_porbit [lemma, in mathcomp.fingroup.perm]
uniq_pairwise [lemma, in mathcomp.ssreflect.seq]
uniq_subseq_pivot [lemma, in mathcomp.ssreflect.seq]
uniq_perm [lemma, in mathcomp.ssreflect.seq]
uniq_min_size [lemma, in mathcomp.ssreflect.seq]
uniq_size_uniq [lemma, in mathcomp.ssreflect.seq]
uniq_leq_size [lemma, in mathcomp.ssreflect.seq]
uniq_eqseq_pivotr [lemma, in mathcomp.ssreflect.seq]
uniq_eqseq_pivotl [lemma, in mathcomp.ssreflect.seq]
uniq_catCA [lemma, in mathcomp.ssreflect.seq]
uniq_catC [lemma, in mathcomp.ssreflect.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]
uniq_sub_le_big_cond [lemma, in mathcomp.ssreflect.bigop]
uniq_sub_le_big [lemma, in mathcomp.ssreflect.bigop]
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]
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.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_GRing_UnitRing_and_ring_quotient_ZmodQuotient [definition, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports.join_ring_quotient_UnitRingQuotient_between_ring_quotient_RingQuotient_and_GRing_UnitRing [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__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__ring_quotient_RingQuotient [definition, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports.ring_quotient_UnitRingQuotient_class__to__ring_quotient_RingQuotient_class [definition, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports.ring_quotient_UnitRingQuotient__to__GRing_Ring [definition, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports.ring_quotient_UnitRingQuotient_class__to__GRing_Ring_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__GRing_Zmodule [definition, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports.ring_quotient_UnitRingQuotient_class__to__GRing_Zmodule_class [definition, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports.ring_quotient_UnitRingQuotient__to__GRing_SemiRing [definition, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports.ring_quotient_UnitRingQuotient_class__to__GRing_SemiRing_class [definition, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports.ring_quotient_UnitRingQuotient__to__GRing_Nmodule [definition, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.Exports.ring_quotient_UnitRingQuotient_class__to__GRing_Nmodule_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__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_Ring_hasMulInverse_mixin [projection, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.GRing_Nmodule_isZmodule_mixin [projection, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.GRing_Nmodule_isSemiRing_mixin [projection, in mathcomp.algebra.ring_quotient]
UnitRingQuotient.GRing_isNmodule_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_isRingQuotient_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.ssreflect.fintype]
unit_eqP [lemma, in mathcomp.ssreflect.eqtype]
unlift [definition, in mathcomp.ssreflect.fintype]
UnliftNone [constructor, in mathcomp.ssreflect.fintype]
unliftP [lemma, in mathcomp.ssreflect.fintype]
UnliftSome [constructor, in mathcomp.ssreflect.fintype]
unlift_some [lemma, in mathcomp.ssreflect.fintype]
unlift_none [lemma, in mathcomp.ssreflect.fintype]
unlift_spec [inductive, in mathcomp.ssreflect.fintype]
unlift_subproof [lemma, in mathcomp.ssreflect.fintype]
unlockable_enum_rank_in [definition, in mathcomp.ssreflect.fintype]
unpickle [definition, in mathcomp.ssreflect.choice]
unpickle_tagged [definition, in mathcomp.ssreflect.choice]
unpickle_seq [definition, in mathcomp.ssreflect.choice]
unsplit [definition, in mathcomp.ssreflect.fintype]
unsplitK [lemma, in mathcomp.ssreflect.fintype]
unzip1 [definition, in mathcomp.ssreflect.seq]
unzip1_map_nth_zip [lemma, in mathcomp.ssreflect.seq]
unzip1_zip [lemma, in mathcomp.ssreflect.seq]
unzip2 [definition, in mathcomp.ssreflect.seq]
unzip2_map_nth_zip [lemma, in mathcomp.ssreflect.seq]
unzip2_zip [lemma, in mathcomp.ssreflect.seq]
uphalf [definition, in mathcomp.ssreflect.ssrnat]
uphalfE [lemma, in mathcomp.ssreflect.ssrnat]
uphalfK [lemma, in mathcomp.ssreflect.ssrnat]
uphalf_gt0 [lemma, in mathcomp.ssreflect.ssrnat]
uphalf_leq [lemma, in mathcomp.ssreflect.ssrnat]
uphalf_half [lemma, in mathcomp.ssreflect.ssrnat]
uphalf_double [lemma, in mathcomp.ssreflect.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.ssreflect.prime]
up_log2S [lemma, in mathcomp.ssreflect.prime]
up_log2_double [lemma, in mathcomp.ssreflect.prime]
up_logMp [lemma, in mathcomp.ssreflect.prime]
up_expnK [lemma, in mathcomp.ssreflect.prime]
up_lognn [lemma, in mathcomp.ssreflect.prime]
up_log_eq [lemma, in mathcomp.ssreflect.prime]
up_log_min [lemma, in mathcomp.ssreflect.prime]
up_log_gtn [lemma, in mathcomp.ssreflect.prime]
up_logP [lemma, in mathcomp.ssreflect.prime]
up_log_bounds [lemma, in mathcomp.ssreflect.prime]
up_log_gt0 [lemma, in mathcomp.ssreflect.prime]
up_log_eq0 [lemma, in mathcomp.ssreflect.prime]
up_log1 [lemma, in mathcomp.ssreflect.prime]
up_log0 [lemma, in mathcomp.ssreflect.prime]
up_log [definition, in mathcomp.ssreflect.prime]
ursubmx [definition, in mathcomp.algebra.matrix]
ursubmxEsub [lemma, in mathcomp.algebra.matrix]
ursubmx_trig [lemma, in mathcomp.algebra.matrix]
UseFinTuple [section, in mathcomp.ssreflect.tuple]
UseFinTuple.ImageTuple [section, in mathcomp.ssreflect.tuple]
UseFinTuple.ImageTuple.A [variable, in mathcomp.ssreflect.tuple]
UseFinTuple.ImageTuple.f [variable, in mathcomp.ssreflect.tuple]
UseFinTuple.ImageTuple.T' [variable, in mathcomp.ssreflect.tuple]
UseFinTuple.MkTuple [section, in mathcomp.ssreflect.tuple]
UseFinTuple.MkTuple.f [variable, in mathcomp.ssreflect.tuple]
UseFinTuple.MkTuple.T' [variable, in mathcomp.ssreflect.tuple]
UseFinTuple.n [variable, in mathcomp.ssreflect.tuple]
UseFinTuple.T [variable, in mathcomp.ssreflect.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

Y

_

(54001 entries)

Notation Index

J

T

W

X

Y

_

(1931 entries)

Module Index

J

K

W

X

Y

_

other

(1658 entries)

Variable Index

J

W

X

Y

_

other

(7199 entries)

Library Index

K

L

U

W

X

Y

_

other

(97 entries)

Lemma Index

Y

_

other

(15214 entries)

Axiom Index

H

J

K

L

N

O

T

U

V

W

X

Y

Z

_

other

(75 entries)

Constructor Index

J

K

W

Y

_

other

(224 entries)

Inductive Index

J

K

Q

W

Y

Z

_

other

(132 entries)

Projection Index

J

K

W

X

Y

_

other

(2371 entries)

Section Index

J

W

X

Y

_

other

(2266 entries)

Abbreviation Index

Y

_

other

(732 entries)

Definition Index

Y

_

other

(21455 entries)

Record Index

J

K

W

X

Y

_

other

(647 entries)