mathcomp.ssreflect.tuple

Global Index

Y

_

(24263 entries)

Notation Index

H

J

O

T

W

X

Y

_

(1399 entries)

Module Index

H

J

K

L

O

T

W

X

Y

Z

_

other

(226 entries)

Variable Index

J

W

X

Y

_

other

(3670 entries)

Library Index

K

L

O

U

W

X

Y

_

other

(89 entries)

Lemma Index

Y

_

other

(12297 entries)

Constructor Index

J

K

W

Y

_

other

(383 entries)

Axiom Index

D

G

H

J

K

L

M

N

O

Q

T

U

V

W

X

Y

Z

_

other

(45 entries)

Inductive Index

J

K

Q

W

Y

Z

_

other

(114 entries)

Projection Index

H

J

K

L

O

W

X

Y

_

other

(279 entries)

Section Index

J

W

X

Y

_

other

(1169 entries)

Abbreviation Index

Y

_

other

(742 entries)

Definition Index

Y

_

other

(3657 entries)

Record Index

B

H

J

K

L

O

W

X

Y

_

other

(193 entries)

D

d [abbreviation, in mathcomp.algebra.mxpoly]
daddv_pi_add [lemma, in mathcomp.algebra.vector]
daddv_pi_proj [lemma, in mathcomp.algebra.vector]
daddv_pi_id [lemma, in mathcomp.algebra.vector]
daddv_pi [definition, in mathcomp.algebra.vector]
dadd_grepr [definition, in mathcomp.character.character]
dc [abbreviation, in mathcomp.ssreflect.choice]
dchi [definition, in mathcomp.character.vcharacter]
dchi_vchar [lemma, in mathcomp.character.vcharacter]
dchi_ndirrE [lemma, in mathcomp.character.vcharacter]
dchi1 [lemma, in mathcomp.character.vcharacter]
DecField [section, in mathcomp.algebra.poly]
DecField.F [variable, in mathcomp.algebra.poly]
decidable_embedding [definition, in mathcomp.field.algebraics_fundamentals]
DecideRed [section, in mathcomp.character.mxrepresentation]
DecideRed.Definitions [section, in mathcomp.character.mxrepresentation]
DecideRed.Definitions.F [variable, in mathcomp.character.mxrepresentation]
DecideRed.Definitions.G [variable, in mathcomp.character.mxrepresentation]
DecideRed.Definitions.gT [variable, in mathcomp.character.mxrepresentation]
DecideRed.Definitions.n [variable, in mathcomp.character.mxrepresentation]
DecideRed.Definitions.rG [variable, in mathcomp.character.mxrepresentation]
DecideRed.F [variable, in mathcomp.character.mxrepresentation]
DecideRed.G [variable, in mathcomp.character.mxrepresentation]
DecideRed.gT [variable, in mathcomp.character.mxrepresentation]
DecideRed.n [variable, in mathcomp.character.mxrepresentation]
DecideRed.rG [variable, in mathcomp.character.mxrepresentation]
decrn_inj_in [lemma, in mathcomp.ssreflect.ssrnat]
decrn_inj [lemma, in mathcomp.ssreflect.ssrnat]
DecSocleType [lemma, in mathcomp.character.mxrepresentation]
dec_mx_reducible_semisimple [lemma, in mathcomp.character.mxrepresentation]
dec_mxsimple_exists [lemma, in mathcomp.character.mxrepresentation]
dec_Qint_span [lemma, in mathcomp.algebra.intdiv]
dec_Cint_span [lemma, in mathcomp.field.algnum]
dec_factor_theorem [lemma, in mathcomp.algebra.poly]
Def [section, in mathcomp.ssreflect.tuple]
Def [section, in mathcomp.ssreflect.finfun]
defaultEncModRelClass [definition, in mathcomp.ssreflect.generic_quotient]
DefaultEncodingModuloRel [section, in mathcomp.ssreflect.generic_quotient]
DefaultEncodingModuloRel.D [variable, in mathcomp.ssreflect.generic_quotient]
DefaultEncodingModuloRel.r [variable, in mathcomp.ssreflect.generic_quotient]
defHgX [abbreviation, in mathcomp.solvable.finmodule]
Definitions [section, in mathcomp.solvable.frobenius]
Definitions.FrobeniusAction [section, in mathcomp.solvable.frobenius]
Definitions.FrobeniusAction.G [variable, in mathcomp.solvable.frobenius]
Definitions.FrobeniusAction.H [variable, in mathcomp.solvable.frobenius]
Definitions.FrobeniusAction.S [variable, in mathcomp.solvable.frobenius]
Definitions.FrobeniusAction.sT [variable, in mathcomp.solvable.frobenius]
Definitions.FrobeniusAction.to [variable, in mathcomp.solvable.frobenius]
Definitions.gT [variable, in mathcomp.solvable.frobenius]
Defs [section, in mathcomp.fingroup.gproduct]
Defs [section, in mathcomp.solvable.maximal]
Defs [section, in mathcomp.character.classfun]
Defs [section, in mathcomp.solvable.center]
Defs.Automorphism [section, in mathcomp.character.classfun]
Defs.Automorphism.u [variable, in mathcomp.character.classfun]
Defs.B [variable, in mathcomp.character.classfun]
Defs.gT [variable, in mathcomp.fingroup.gproduct]
Defs.gT [variable, in mathcomp.solvable.maximal]
Defs.gT [variable, in mathcomp.character.classfun]
Defs.gT [variable, in mathcomp.solvable.center]
'1_ _ (ring_scope) [notation, in mathcomp.character.classfun]
def_pnElem [lemma, in mathcomp.solvable.abelian]
def_pblock [lemma, in mathcomp.ssreflect.finset]
Def.aT [variable, in mathcomp.ssreflect.finfun]
Def.n [variable, in mathcomp.ssreflect.tuple]
Def.rT [variable, in mathcomp.ssreflect.finfun]
Def.T [variable, in mathcomp.ssreflect.tuple]
degree_irr1 [lemma, in mathcomp.character.mxrepresentation]
degree_mxminpoly_map [lemma, in mathcomp.algebra.mxpoly]
degree_mxminpoly [definition, in mathcomp.algebra.mxpoly]
degree_mxminpoly_proof [lemma, in mathcomp.algebra.mxpoly]
delta_mx_dshift [lemma, in mathcomp.algebra.matrix]
delta_mx_ushift [lemma, in mathcomp.algebra.matrix]
delta_mx_rshift [lemma, in mathcomp.algebra.matrix]
delta_mx_lshift [lemma, in mathcomp.algebra.matrix]
delta_mx [definition, in mathcomp.algebra.matrix]
delta_mx_key [lemma, in mathcomp.algebra.matrix]
denom_Ratio [lemma, in mathcomp.algebra.fraction]
denom_ratioP [lemma, in mathcomp.algebra.fraction]
denq [definition, in mathcomp.algebra.rat]
denqN [lemma, in mathcomp.algebra.rat]
denqP [lemma, in mathcomp.algebra.rat]
denqVz [lemma, in mathcomp.algebra.rat]
denq_norm [lemma, in mathcomp.algebra.rat]
denq_mulr_sign [lemma, in mathcomp.algebra.rat]
denq_int [lemma, in mathcomp.algebra.rat]
denq_eq0 [lemma, in mathcomp.algebra.rat]
denq_neq0 [lemma, in mathcomp.algebra.rat]
denq_lt0 [lemma, in mathcomp.algebra.rat]
denq_ge0 [definition, in mathcomp.algebra.rat]
denq_gt0 [lemma, in mathcomp.algebra.rat]
DepPlainTheory [section, in mathcomp.ssreflect.finfun]
DepPlainTheory.aT [variable, in mathcomp.ssreflect.finfun]
DepPlainTheory.F [variable, in mathcomp.ssreflect.finfun]
DepPlainTheory.pT [variable, in mathcomp.ssreflect.finfun]
DepPlainTheory.rT [variable, in mathcomp.ssreflect.finfun]
deprecated_filter_index_enum [lemma, in mathcomp.ssreflect.bigop]
Deprecation [module, in mathcomp.ssreflect.ssreflect]
Deprecation.Exports [module, in mathcomp.ssreflect.ssreflect]
Deprecation.Exports.deprecate [abbreviation, in mathcomp.ssreflect.ssreflect]
Deprecation.exposed [definition, in mathcomp.ssreflect.ssreflect]
Deprecation.hidden [definition, in mathcomp.ssreflect.ssreflect]
Deprecation.hide [definition, in mathcomp.ssreflect.ssreflect]
Deprecation.hint [projection, in mathcomp.ssreflect.ssreflect]
Deprecation.Hint [constructor, in mathcomp.ssreflect.ssreflect]
Deprecation.hinted [record, in mathcomp.ssreflect.ssreflect]
Deprecation.Reject [module, in mathcomp.ssreflect.ssreflect]
Deprecation.Reject [constructor, in mathcomp.ssreflect.ssreflect]
Deprecation.reject [inductive, in mathcomp.ssreflect.ssreflect]
Deprecation.reject_hint [definition, in mathcomp.ssreflect.ssreflect]
Deprecation.Silent [module, in mathcomp.ssreflect.ssreflect]
Deprecation.Silent [constructor, in mathcomp.ssreflect.ssreflect]
Deprecation.silent [inductive, in mathcomp.ssreflect.ssreflect]
Deprecation.silent_hint [definition, in mathcomp.ssreflect.ssreflect]
Deprecation.statement [projection, in mathcomp.ssreflect.ssreflect]
dergS [lemma, in mathcomp.solvable.commutator]
dergSn [lemma, in mathcomp.solvable.commutator]
derg0 [lemma, in mathcomp.solvable.commutator]
derg1 [lemma, in mathcomp.solvable.commutator]
derG1P [lemma, in mathcomp.solvable.commutator]
deriv [definition, in mathcomp.algebra.poly]
Derivation [definition, in mathcomp.field.separable]
DerivationS [lemma, in mathcomp.field.separable]
Derivation_separableP [lemma, in mathcomp.field.separable]
Derivation_separable [lemma, in mathcomp.field.separable]
Derivation_horner [lemma, in mathcomp.field.separable]
Derivation_exp [lemma, in mathcomp.field.separable]
Derivation_scalar [lemma, in mathcomp.field.separable]
Derivation_mul_poly [lemma, in mathcomp.field.separable]
Derivation_mul [lemma, in mathcomp.field.separable]
Derivation1 [lemma, in mathcomp.field.separable]
derivB [lemma, in mathcomp.algebra.poly]
derivC [lemma, in mathcomp.algebra.poly]
derivCE [definition, in mathcomp.algebra.poly]
derivD [lemma, in mathcomp.algebra.poly]
derivE [definition, in mathcomp.algebra.poly]
DerivedBasics [section, in mathcomp.solvable.commutator]
DerivedBasics.gT [variable, in mathcomp.solvable.commutator]
DerivedGroup [section, in mathcomp.character.character]
DerivedGroup.gT [variable, in mathcomp.character.character]
derivedP [lemma, in mathcomp.solvable.nilpotent]
derived_at [definition, in mathcomp.solvable.commutator]
derived_at_rec [definition, in mathcomp.solvable.commutator]
derivM [lemma, in mathcomp.algebra.poly]
derivMn [lemma, in mathcomp.algebra.poly]
derivMNn [lemma, in mathcomp.algebra.poly]
derivMXaddC [lemma, in mathcomp.algebra.poly]
derivMz [lemma, in mathcomp.algebra.ssrint]
derivn [definition, in mathcomp.algebra.poly]
derivN [lemma, in mathcomp.algebra.poly]
derivnC [lemma, in mathcomp.algebra.poly]
derivnD [lemma, in mathcomp.algebra.poly]
derivnMn [lemma, in mathcomp.algebra.poly]
derivnMNn [lemma, in mathcomp.algebra.poly]
derivnMXaddC [lemma, in mathcomp.algebra.poly]
derivnN [lemma, in mathcomp.algebra.poly]
derivnS [lemma, in mathcomp.algebra.poly]
derivnXn [lemma, in mathcomp.algebra.poly]
derivnZ [lemma, in mathcomp.algebra.poly]
derivn_map [lemma, in mathcomp.algebra.poly]
derivn_poly0 [lemma, in mathcomp.algebra.poly]
derivn_sub [lemma, in mathcomp.algebra.poly]
derivn_is_linear [lemma, in mathcomp.algebra.poly]
derivn0 [lemma, in mathcomp.algebra.poly]
derivn1 [lemma, in mathcomp.algebra.poly]
derivSn [lemma, in mathcomp.algebra.poly]
derivX [lemma, in mathcomp.algebra.poly]
derivXn [lemma, in mathcomp.algebra.poly]
derivXsubC [lemma, in mathcomp.algebra.poly]
derivZ [lemma, in mathcomp.algebra.poly]
deriv_exp [lemma, in mathcomp.algebra.poly]
deriv_comp [lemma, in mathcomp.algebra.poly]
deriv_map [lemma, in mathcomp.algebra.poly]
deriv_mulC [lemma, in mathcomp.algebra.poly]
deriv_is_linear [lemma, in mathcomp.algebra.poly]
deriv0 [lemma, in mathcomp.algebra.poly]
derJ [lemma, in mathcomp.solvable.commutator]
der_bigdprod [lemma, in mathcomp.solvable.nilpotent]
der_bigcprod [lemma, in mathcomp.solvable.nilpotent]
der_dprod [lemma, in mathcomp.solvable.nilpotent]
der_cprod [lemma, in mathcomp.solvable.nilpotent]
der_cont [lemma, in mathcomp.solvable.commutator]
der_normalS [lemma, in mathcomp.solvable.commutator]
der_subS [lemma, in mathcomp.solvable.commutator]
der_normal [lemma, in mathcomp.solvable.commutator]
der_norm [lemma, in mathcomp.solvable.commutator]
der_sub [lemma, in mathcomp.solvable.commutator]
der_char [lemma, in mathcomp.solvable.commutator]
der_abelian [lemma, in mathcomp.solvable.commutator]
der_group_set [lemma, in mathcomp.solvable.commutator]
der1_sub_rker [lemma, in mathcomp.character.mxrepresentation]
der1_stab_Ohm1_SCN_series [lemma, in mathcomp.solvable.maximal]
der1_joing_cycles [lemma, in mathcomp.solvable.commutator]
der1_min [lemma, in mathcomp.solvable.commutator]
der1_subG [lemma, in mathcomp.fingroup.fingroup]
determinant [definition, in mathcomp.algebra.matrix]
determinant_alternate [lemma, in mathcomp.algebra.matrix]
determinant_multilinear [lemma, in mathcomp.algebra.matrix]
detM [lemma, in mathcomp.algebra.matrix]
DetOrder [section, in mathcomp.character.character]
DetOrder.DetRepr [section, in mathcomp.character.character]
DetOrder.DetRepr.n [variable, in mathcomp.character.character]
DetOrder.DetRepr.rG [variable, in mathcomp.character.character]
DetOrder.G [variable, in mathcomp.character.character]
DetOrder.gT [variable, in mathcomp.character.character]
detRepr [definition, in mathcomp.character.character]
detRepr_lin_char [lemma, in mathcomp.character.character]
detV [lemma, in mathcomp.algebra.matrix]
detZ [lemma, in mathcomp.algebra.matrix]
det_inv [lemma, in mathcomp.algebra.matrix]
det_lblock [lemma, in mathcomp.algebra.matrix]
det_ublock [lemma, in mathcomp.algebra.matrix]
det_diag [lemma, in mathcomp.algebra.matrix]
det_mulmx [lemma, in mathcomp.algebra.matrix]
det_scalar1 [lemma, in mathcomp.algebra.matrix]
det_scalar [lemma, in mathcomp.algebra.matrix]
det_mx00 [lemma, in mathcomp.algebra.matrix]
det_perm [lemma, in mathcomp.algebra.matrix]
det_tr [lemma, in mathcomp.algebra.matrix]
det_map_mx [lemma, in mathcomp.algebra.matrix]
det_is_repr [lemma, in mathcomp.character.character]
det_repr_mx [definition, in mathcomp.character.character]
det0 [lemma, in mathcomp.algebra.matrix]
det0P [lemma, in mathcomp.algebra.matrix]
det1 [lemma, in mathcomp.algebra.matrix]
dffun_aT [abbreviation, in mathcomp.ssreflect.finfun]
dfinfun_of [definition, in mathcomp.ssreflect.finfun]
dfs [definition, in mathcomp.ssreflect.fingraph]
dfsP [lemma, in mathcomp.ssreflect.fingraph]
DfsPath [constructor, in mathcomp.ssreflect.fingraph]
dfs_pathP [lemma, in mathcomp.ssreflect.fingraph]
dfs_path [inductive, in mathcomp.ssreflect.fingraph]
diag_mx_comm [lemma, in mathcomp.algebra.matrix]
diag_mxC [lemma, in mathcomp.algebra.matrix]
diag_const_mx [lemma, in mathcomp.algebra.matrix]
diag_mx_sum_delta [lemma, in mathcomp.algebra.matrix]
diag_mx_is_linear [lemma, in mathcomp.algebra.matrix]
diag_mx [definition, in mathcomp.algebra.matrix]
diag_mx_key [lemma, in mathcomp.algebra.matrix]
diffmx [definition, in mathcomp.algebra.mxalgebra]
diffmxE [lemma, in mathcomp.algebra.mxalgebra]
diffmxSl [lemma, in mathcomp.algebra.mxalgebra]
diffmx_key [lemma, in mathcomp.algebra.mxalgebra]
diffmx_def [definition, in mathcomp.algebra.mxalgebra]
diffv [definition, in mathcomp.algebra.vector]
diffvSl [lemma, in mathcomp.algebra.vector]
diffv_eq0 [lemma, in mathcomp.algebra.vector]
diff_roots [definition, in mathcomp.algebra.poly]
diff_id_sh [lemma, in mathcomp.solvable.burnside_app]
Dihedral [constructor, in mathcomp.solvable.extremal]
dihedral_classP [lemma, in mathcomp.solvable.extremal]
dihedral_gtype [definition, in mathcomp.solvable.extremal]
dihedral2_structure [lemma, in mathcomp.solvable.extremal]
dIirr [definition, in mathcomp.character.vcharacter]
dimv [definition, in mathcomp.algebra.vector]
dimvf [lemma, in mathcomp.algebra.vector]
dimvS [lemma, in mathcomp.algebra.vector]
dimv_sum_leqif [lemma, in mathcomp.algebra.vector]
dimv_leq_sum [lemma, in mathcomp.algebra.vector]
dimv_add_leqif [lemma, in mathcomp.algebra.vector]
dimv_disjoint_sum [lemma, in mathcomp.algebra.vector]
dimv_sum_cap [lemma, in mathcomp.algebra.vector]
dimv_cap_compl [lemma, in mathcomp.algebra.vector]
dimv_compl [lemma, in mathcomp.algebra.vector]
dimv_leqif_eq [lemma, in mathcomp.algebra.vector]
dimv_leqif_sup [lemma, in mathcomp.algebra.vector]
dimv_eq0 [lemma, in mathcomp.algebra.vector]
dimv0 [lemma, in mathcomp.algebra.vector]
dimv1 [lemma, in mathcomp.field.falgebra]
dim_fixed_galois [lemma, in mathcomp.field.galois]
dim_fixedField [lemma, in mathcomp.field.galois]
dim_refBaseField [lemma, in mathcomp.field.fieldext]
dim_baseVspace [lemma, in mathcomp.field.fieldext]
dim_aspaceOver [lemma, in mathcomp.field.fieldext]
dim_vspaceOver [lemma, in mathcomp.field.fieldext]
dim_Fadjoin [lemma, in mathcomp.field.fieldext]
dim_sup_field [lemma, in mathcomp.field.fieldext]
dim_field_module [lemma, in mathcomp.field.fieldext]
dim_cosetv [lemma, in mathcomp.field.fieldext]
dim_span [lemma, in mathcomp.algebra.vector]
dim_vline [lemma, in mathcomp.algebra.vector]
dim_cfun_on_abelian [lemma, in mathcomp.character.classfun]
dim_cfun_on [lemma, in mathcomp.character.classfun]
dim_cfun [lemma, in mathcomp.character.classfun]
dim_abelemE [lemma, in mathcomp.character.mxabelem]
dim_cosetv_unit [lemma, in mathcomp.field.falgebra]
dim_algid [lemma, in mathcomp.field.falgebra]
dim_prodv [lemma, in mathcomp.field.falgebra]
dinjectiveb [definition, in mathcomp.ssreflect.fintype]
dinjectiveP [lemma, in mathcomp.ssreflect.fintype]
dinjectivePn [lemma, in mathcomp.ssreflect.fintype]
DirectSums [section, in mathcomp.algebra.mxalgebra]
DirectSums.F [variable, in mathcomp.algebra.mxalgebra]
DirectSums.I [variable, in mathcomp.algebra.mxalgebra]
DirectSums.P [variable, in mathcomp.algebra.mxalgebra]
directv [abbreviation, in mathcomp.algebra.vector]
directv [abbreviation, in mathcomp.algebra.vector]
directvE [lemma, in mathcomp.algebra.vector]
directvEgeq [lemma, in mathcomp.algebra.vector]
directvP [lemma, in mathcomp.algebra.vector]
directv_sum_unique [lemma, in mathcomp.algebra.vector]
directv_sum_independent [lemma, in mathcomp.algebra.vector]
directv_sumE [lemma, in mathcomp.algebra.vector]
directv_sumP [lemma, in mathcomp.algebra.vector]
directv_add_unique [lemma, in mathcomp.algebra.vector]
directv_addP [lemma, in mathcomp.algebra.vector]
directv_addE [lemma, in mathcomp.algebra.vector]
directv_trivial [lemma, in mathcomp.algebra.vector]
directv_def [definition, in mathcomp.algebra.vector]
direct_product [definition, in mathcomp.fingroup.gproduct]
DirprodIsom [section, in mathcomp.fingroup.gproduct]
DirprodIsom.gT [variable, in mathcomp.fingroup.gproduct]
dirr [definition, in mathcomp.character.vcharacter]
dirrE [lemma, in mathcomp.character.vcharacter]
dIrrP [lemma, in mathcomp.character.vcharacter]
dirrP [lemma, in mathcomp.character.vcharacter]
dirr_small_norm [lemma, in mathcomp.character.vcharacter]
dirr_constt_oppl [lemma, in mathcomp.character.vcharacter]
dirr_constt_oppI [lemma, in mathcomp.character.vcharacter]
dirr_constt_oppr [lemma, in mathcomp.character.vcharacter]
dirr_consttE [lemma, in mathcomp.character.vcharacter]
dirr_constt [definition, in mathcomp.character.vcharacter]
dirr_dIirrE [lemma, in mathcomp.character.vcharacter]
dirr_dIirrPE [lemma, in mathcomp.character.vcharacter]
dirr_dIirr [definition, in mathcomp.character.vcharacter]
dirr_inj [lemma, in mathcomp.character.vcharacter]
dirr_dchi [lemma, in mathcomp.character.vcharacter]
dirr_aut [lemma, in mathcomp.character.vcharacter]
dirr_norm1 [lemma, in mathcomp.character.vcharacter]
dirr_sign [lemma, in mathcomp.character.vcharacter]
dirr_opp [lemma, in mathcomp.character.vcharacter]
dirr_oppr_closed [lemma, in mathcomp.character.vcharacter]
dirr_key [lemma, in mathcomp.character.vcharacter]
dirr1 [definition, in mathcomp.character.vcharacter]
dir_s0p [lemma, in mathcomp.solvable.burnside_app]
dir_iso_iso3 [lemma, in mathcomp.solvable.burnside_app]
dir_iso3l [definition, in mathcomp.solvable.burnside_app]
dir_iso3 [definition, in mathcomp.solvable.burnside_app]
disjoint [definition, in mathcomp.ssreflect.fintype]
disjoints_subset [lemma, in mathcomp.ssreflect.finset]
disjointU [lemma, in mathcomp.ssreflect.fintype]
disjointU1 [lemma, in mathcomp.ssreflect.fintype]
disjoint_cat [lemma, in mathcomp.ssreflect.fintype]
disjoint_has [lemma, in mathcomp.ssreflect.fintype]
disjoint_cons [lemma, in mathcomp.ssreflect.fintype]
disjoint_trans [lemma, in mathcomp.ssreflect.fintype]
disjoint_subset [lemma, in mathcomp.ssreflect.fintype]
disjoint_sym [lemma, in mathcomp.ssreflect.fintype]
disjoint_setI0 [lemma, in mathcomp.ssreflect.finset]
disjoint0 [lemma, in mathcomp.ssreflect.fintype]
disjoint1 [lemma, in mathcomp.ssreflect.fintype]
Distributivity [section, in mathcomp.ssreflect.bigop]
Distributivity.one [variable, in mathcomp.ssreflect.bigop]
Distributivity.plus [variable, in mathcomp.ssreflect.bigop]
Distributivity.R [variable, in mathcomp.ssreflect.bigop]
Distributivity.times [variable, in mathcomp.ssreflect.bigop]
Distributivity.zero [variable, in mathcomp.ssreflect.bigop]
_ + _ [notation, in mathcomp.ssreflect.bigop]
_ * _ [notation, in mathcomp.ssreflect.bigop]
*%M [notation, in mathcomp.ssreflect.bigop]
+%M [notation, in mathcomp.ssreflect.bigop]
0 [notation, in mathcomp.ssreflect.bigop]
1 [notation, in mathcomp.ssreflect.bigop]
div [library]
divgI [lemma, in mathcomp.fingroup.fingroup]
divgr [definition, in mathcomp.fingroup.gproduct]
divgrM [lemma, in mathcomp.fingroup.gproduct]
divgrMid [lemma, in mathcomp.fingroup.gproduct]
divgrMl [lemma, in mathcomp.fingroup.gproduct]
divgr_id [lemma, in mathcomp.fingroup.gproduct]
divgr_eq [lemma, in mathcomp.fingroup.gproduct]
divgS [lemma, in mathcomp.fingroup.fingroup]
divg_normal [lemma, in mathcomp.fingroup.quotient]
divg_indexS [lemma, in mathcomp.fingroup.fingroup]
divg_index [lemma, in mathcomp.fingroup.fingroup]
divisors [definition, in mathcomp.ssreflect.prime]
divisors_id [lemma, in mathcomp.ssreflect.prime]
divisors_uniq [lemma, in mathcomp.ssreflect.prime]
divisors_correct [lemma, in mathcomp.ssreflect.prime]
divisor1 [lemma, in mathcomp.ssreflect.prime]
divn [definition, in mathcomp.ssreflect.div]
divnA [lemma, in mathcomp.ssreflect.div]
divnAC [lemma, in mathcomp.ssreflect.div]
divnB [lemma, in mathcomp.ssreflect.div]
divnBl [lemma, in mathcomp.ssreflect.div]
divnBMl [lemma, in mathcomp.ssreflect.div]
divnBr [lemma, in mathcomp.ssreflect.div]
divnD [lemma, in mathcomp.ssreflect.div]
divnDl [lemma, in mathcomp.ssreflect.div]
divnDMl [lemma, in mathcomp.ssreflect.div]
divnDr [lemma, in mathcomp.ssreflect.div]
divnK [lemma, in mathcomp.ssreflect.div]
divnMA [lemma, in mathcomp.ssreflect.div]
divnMBl [lemma, in mathcomp.ssreflect.div]
divnMDl [lemma, in mathcomp.ssreflect.div]
divnMl [lemma, in mathcomp.ssreflect.div]
divnMr [lemma, in mathcomp.ssreflect.div]
divnn [lemma, in mathcomp.ssreflect.div]
divnS [lemma, in mathcomp.ssreflect.div]
divNz_nat [lemma, in mathcomp.algebra.intdiv]
divn_count_dvd [lemma, in mathcomp.ssreflect.prime]
divn_pred [lemma, in mathcomp.ssreflect.div]
divn_modl [lemma, in mathcomp.ssreflect.div]
divn_mulAC [lemma, in mathcomp.ssreflect.div]
divn_gt0 [lemma, in mathcomp.ssreflect.div]
divn_small [lemma, in mathcomp.ssreflect.div]
divn_eq [lemma, in mathcomp.ssreflect.div]
divn0 [lemma, in mathcomp.ssreflect.div]
divn1 [lemma, in mathcomp.ssreflect.div]
divn2 [lemma, in mathcomp.ssreflect.div]
divp_polyOver [lemma, in mathcomp.field.fieldext]
divq [definition, in mathcomp.algebra.rat]
divqP [lemma, in mathcomp.algebra.rat]
DivqSpecN [constructor, in mathcomp.algebra.rat]
DivqSpecP [constructor, in mathcomp.algebra.rat]
divq_eq [lemma, in mathcomp.algebra.rat]
divq_spec [inductive, in mathcomp.algebra.rat]
divq_num_den [lemma, in mathcomp.algebra.rat]
divz [definition, in mathcomp.algebra.intdiv]
divzA [lemma, in mathcomp.algebra.intdiv]
divzAC [lemma, in mathcomp.algebra.intdiv]
divzDl [lemma, in mathcomp.algebra.intdiv]
divzDr [lemma, in mathcomp.algebra.intdiv]
divzK [lemma, in mathcomp.algebra.intdiv]
divzMA [lemma, in mathcomp.algebra.intdiv]
divzMA_ge0 [lemma, in mathcomp.algebra.intdiv]
divzMDl [lemma, in mathcomp.algebra.intdiv]
divzMl [lemma, in mathcomp.algebra.intdiv]
divzMpl [lemma, in mathcomp.algebra.intdiv]
divzMpr [lemma, in mathcomp.algebra.intdiv]
divzMr [lemma, in mathcomp.algebra.intdiv]
divzN [lemma, in mathcomp.algebra.intdiv]
divzz [lemma, in mathcomp.algebra.intdiv]
divz_mulAC [lemma, in mathcomp.algebra.intdiv]
divz_ge0 [lemma, in mathcomp.algebra.intdiv]
divz_small [lemma, in mathcomp.algebra.intdiv]
divz_eq [lemma, in mathcomp.algebra.intdiv]
divz_abs [lemma, in mathcomp.algebra.intdiv]
divz_nat [lemma, in mathcomp.algebra.intdiv]
divz0 [lemma, in mathcomp.algebra.intdiv]
divz1 [lemma, in mathcomp.algebra.intdiv]
div_annihilantP [lemma, in mathcomp.algebra.polyXY]
div_annihilant_neq0 [lemma, in mathcomp.algebra.polyXY]
div_annihilant_in_ideal [lemma, in mathcomp.algebra.polyXY]
div_annihilant [definition, in mathcomp.algebra.polyXY]
div_ring_mul_group_cyclic [lemma, in mathcomp.solvable.cyclic]
div0n [lemma, in mathcomp.ssreflect.div]
div0z [lemma, in mathcomp.algebra.intdiv]
dlsubmx [definition, in mathcomp.algebra.matrix]
DnQ_extraspecial [lemma, in mathcomp.solvable.extraspecial]
DnQ_pgroup [lemma, in mathcomp.solvable.extraspecial]
DnQ_P [lemma, in mathcomp.solvable.extraspecial]
dom [abbreviation, in mathcomp.fingroup.action]
dom [definition, in mathcomp.fingroup.morphism]
domP [lemma, in mathcomp.fingroup.morphism]
dom_hom_mx_module [lemma, in mathcomp.character.mxrepresentation]
dom_hom_invmx [lemma, in mathcomp.character.mxrepresentation]
dom_hom_mx [definition, in mathcomp.character.mxrepresentation]
dom_qactJ [lemma, in mathcomp.fingroup.action]
dom_ker [lemma, in mathcomp.fingroup.morphism]
DotProduct [section, in mathcomp.character.classfun]
DotProduct.G [variable, in mathcomp.character.classfun]
DotProduct.gT [variable, in mathcomp.character.classfun]
double [definition, in mathcomp.ssreflect.ssrnat]
doubleB [lemma, in mathcomp.ssreflect.ssrnat]
doubleD [lemma, in mathcomp.ssreflect.ssrnat]
doubleE [lemma, in mathcomp.ssreflect.ssrnat]
doubleK [lemma, in mathcomp.ssreflect.ssrnat]
doubleMl [lemma, in mathcomp.ssreflect.ssrnat]
doubleMr [lemma, in mathcomp.ssreflect.ssrnat]
doubleS [lemma, in mathcomp.ssreflect.ssrnat]
double_inj [definition, in mathcomp.ssreflect.ssrnat]
double_eq0 [lemma, in mathcomp.ssreflect.ssrnat]
double_gt0 [lemma, in mathcomp.ssreflect.ssrnat]
double_rec [definition, in mathcomp.ssreflect.ssrnat]
double0 [lemma, in mathcomp.ssreflect.ssrnat]
dpair [definition, in mathcomp.fingroup.perm]
dprod [abbreviation, in mathcomp.fingroup.gproduct]
dprod [abbreviation, in mathcomp.fingroup.gproduct]
DProd [section, in mathcomp.character.character]
dprodA [lemma, in mathcomp.fingroup.gproduct]
dprodC [lemma, in mathcomp.fingroup.gproduct]
dprodE [lemma, in mathcomp.fingroup.gproduct]
dprodEcp [lemma, in mathcomp.fingroup.gproduct]
dprodEsd [lemma, in mathcomp.fingroup.gproduct]
dprodEY [lemma, in mathcomp.fingroup.gproduct]
dprodg1 [lemma, in mathcomp.fingroup.gproduct]
dprodJ [lemma, in mathcomp.fingroup.gproduct]
dprodl_Iirr0 [lemma, in mathcomp.character.character]
dprodl_Iirr_eq0 [lemma, in mathcomp.character.character]
dprodl_IirrK [lemma, in mathcomp.character.character]
dprodl_IirrE [lemma, in mathcomp.character.character]
dprodl_Iirr [definition, in mathcomp.character.character]
dprodm [definition, in mathcomp.fingroup.gproduct]
dprodmE [lemma, in mathcomp.fingroup.gproduct]
dprodmEl [lemma, in mathcomp.fingroup.gproduct]
dprodmEr [lemma, in mathcomp.fingroup.gproduct]
dprodm_eqf [lemma, in mathcomp.fingroup.gproduct]
dprodm_cprod [lemma, in mathcomp.fingroup.gproduct]
dprodP [lemma, in mathcomp.fingroup.gproduct]
dprodr_Iirr0 [lemma, in mathcomp.character.character]
dprodr_Iirr_eq0 [lemma, in mathcomp.character.character]
dprodr_IirrK [lemma, in mathcomp.character.character]
dprodr_IirrE [lemma, in mathcomp.character.character]
dprodr_Iirr [definition, in mathcomp.character.character]
DProduct [section, in mathcomp.character.classfun]
DProduct.cKH [variable, in mathcomp.character.classfun]
DProduct.G [variable, in mathcomp.character.classfun]
DProduct.gT [variable, in mathcomp.character.classfun]
DProduct.H [variable, in mathcomp.character.classfun]
DProduct.K [variable, in mathcomp.character.classfun]
DProduct.KxH [variable, in mathcomp.character.classfun]
DProduct.nsHG [variable, in mathcomp.character.classfun]
DProduct.nsKG [variable, in mathcomp.character.classfun]
DProduct.sHG [variable, in mathcomp.character.classfun]
DProduct.sKG [variable, in mathcomp.character.classfun]
dprodW [lemma, in mathcomp.fingroup.gproduct]
dprodWC [lemma, in mathcomp.fingroup.gproduct]
dprodWcp [lemma, in mathcomp.fingroup.gproduct]
dprodWsd [lemma, in mathcomp.fingroup.gproduct]
dprodWsdC [lemma, in mathcomp.fingroup.gproduct]
dprodWY [lemma, in mathcomp.fingroup.gproduct]
dprodYP [lemma, in mathcomp.fingroup.gproduct]
dprod_card [lemma, in mathcomp.fingroup.gproduct]
dprod_modr [lemma, in mathcomp.fingroup.gproduct]
dprod_modl [lemma, in mathcomp.fingroup.gproduct]
dprod_normal2 [lemma, in mathcomp.fingroup.gproduct]
dprod_IirrC [lemma, in mathcomp.character.character]
dprod_IirrK [lemma, in mathcomp.character.character]
dprod_Iirr_onto [lemma, in mathcomp.character.character]
dprod_Iirr_eq0 [lemma, in mathcomp.character.character]
dprod_Iirr0r [lemma, in mathcomp.character.character]
dprod_Iirr0l [lemma, in mathcomp.character.character]
dprod_Iirr0 [lemma, in mathcomp.character.character]
dprod_Iirr_inj [lemma, in mathcomp.character.character]
dprod_IirrEr [lemma, in mathcomp.character.character]
dprod_IirrEl [lemma, in mathcomp.character.character]
dprod_IirrE [lemma, in mathcomp.character.character]
dprod_Iirr [definition, in mathcomp.character.character]
dprod_homocyclic [lemma, in mathcomp.solvable.abelian]
dprod_abelem [lemma, in mathcomp.solvable.abelian]
dprod_exponent [lemma, in mathcomp.solvable.abelian]
dprod_rowg [lemma, in mathcomp.character.mxabelem]
dprod_nil [lemma, in mathcomp.solvable.nilpotent]
DProd.G [variable, in mathcomp.character.character]
DProd.gT [variable, in mathcomp.character.character]
DProd.H [variable, in mathcomp.character.character]
DProd.K [variable, in mathcomp.character.character]
DProd.KxH [variable, in mathcomp.character.character]
dprod1g [lemma, in mathcomp.fingroup.gproduct]
drop [definition, in mathcomp.ssreflect.seq]
drop_tupleP [lemma, in mathcomp.ssreflect.tuple]
drop_iota [lemma, in mathcomp.ssreflect.seq]
drop_subseq [lemma, in mathcomp.ssreflect.seq]
drop_rev [lemma, in mathcomp.ssreflect.seq]
drop_nth [lemma, in mathcomp.ssreflect.seq]
drop_nseq [lemma, in mathcomp.ssreflect.seq]
drop_rcons [lemma, in mathcomp.ssreflect.seq]
drop_drop [lemma, in mathcomp.ssreflect.seq]
drop_size_cat [lemma, in mathcomp.ssreflect.seq]
drop_cat [lemma, in mathcomp.ssreflect.seq]
drop_cons [lemma, in mathcomp.ssreflect.seq]
drop_size [lemma, in mathcomp.ssreflect.seq]
drop_oversize [lemma, in mathcomp.ssreflect.seq]
drop_behead [lemma, in mathcomp.ssreflect.seq]
drop0 [lemma, in mathcomp.ssreflect.seq]
drop1 [lemma, in mathcomp.ssreflect.seq]
drsubmx [definition, in mathcomp.algebra.matrix]
dsubmx [definition, in mathcomp.algebra.matrix]
dsubmx_key [lemma, in mathcomp.algebra.matrix]
dsumx_mul [lemma, in mathcomp.character.character]
dtuple_on_subset [lemma, in mathcomp.solvable.primitive_action]
dtuple_on_add_D1 [lemma, in mathcomp.solvable.primitive_action]
dtuple_on_add [lemma, in mathcomp.solvable.primitive_action]
dtuple_onP [lemma, in mathcomp.solvable.primitive_action]
dtuple_on [definition, in mathcomp.solvable.primitive_action]
dvdA [definition, in mathcomp.field.algnum]
dvdA_zmod_closed [lemma, in mathcomp.field.algnum]
dvdA_key [lemma, in mathcomp.field.algnum]
dvdCP [lemma, in mathcomp.field.algC]
dvdCP_nat [lemma, in mathcomp.field.algC]
dvdC_int [lemma, in mathcomp.field.algC]
dvdC_nat [lemma, in mathcomp.field.algC]
dvdC_zmod [lemma, in mathcomp.field.algC]
dvdC_key [lemma, in mathcomp.field.algC]
dvdC_refl [lemma, in mathcomp.field.algC]
dvdC_trans [lemma, in mathcomp.field.algC]
dvdC_mul2l [lemma, in mathcomp.field.algC]
dvdC_mul2r [lemma, in mathcomp.field.algC]
dvdC_mulr [lemma, in mathcomp.field.algC]
dvdC_mull [lemma, in mathcomp.field.algC]
dvdC0 [lemma, in mathcomp.field.algC]
dvdn [definition, in mathcomp.ssreflect.div]
dvdnn [lemma, in mathcomp.ssreflect.div]
dvdnP [lemma, in mathcomp.ssreflect.div]
dvdn_quotient [lemma, in mathcomp.fingroup.quotient]
dvdn_morphim [lemma, in mathcomp.fingroup.quotient]
dvdn_pred_predX [lemma, in mathcomp.ssreflect.binomial]
dvdn_partP [lemma, in mathcomp.ssreflect.prime]
dvdn_sum [lemma, in mathcomp.ssreflect.prime]
dvdn_divisors [lemma, in mathcomp.ssreflect.prime]
dvdn_part [lemma, in mathcomp.ssreflect.prime]
dvdn_pfactor [lemma, in mathcomp.ssreflect.prime]
dvdn_leq_log [lemma, in mathcomp.ssreflect.prime]
dvdn_prime2 [lemma, in mathcomp.ssreflect.prime]
dvdn_pexp2r [lemma, in mathcomp.ssreflect.div]
dvdn_double_ltn [lemma, in mathcomp.ssreflect.div]
dvdn_double_leq [lemma, in mathcomp.ssreflect.div]
dvdn_lcm [lemma, in mathcomp.ssreflect.div]
dvdn_lcmr [lemma, in mathcomp.ssreflect.div]
dvdn_lcml [lemma, in mathcomp.ssreflect.div]
dvdn_gcd [lemma, in mathcomp.ssreflect.div]
dvdn_gcdl [lemma, in mathcomp.ssreflect.div]
dvdn_gcdr [lemma, in mathcomp.ssreflect.div]
dvdn_fact [lemma, in mathcomp.ssreflect.div]
dvdn_exp [lemma, in mathcomp.ssreflect.div]
dvdn_sub [lemma, in mathcomp.ssreflect.div]
dvdn_subl [lemma, in mathcomp.ssreflect.div]
dvdn_subr [lemma, in mathcomp.ssreflect.div]
dvdn_add_eq [lemma, in mathcomp.ssreflect.div]
dvdn_add [lemma, in mathcomp.ssreflect.div]
dvdn_addl [lemma, in mathcomp.ssreflect.div]
dvdn_addr [lemma, in mathcomp.ssreflect.div]
dvdn_exp2r [lemma, in mathcomp.ssreflect.div]
dvdn_Pexp2l [lemma, in mathcomp.ssreflect.div]
dvdn_exp2l [lemma, in mathcomp.ssreflect.div]
dvdn_div [lemma, in mathcomp.ssreflect.div]
dvdn_divRL [lemma, in mathcomp.ssreflect.div]
dvdn_divLR [lemma, in mathcomp.ssreflect.div]
dvdn_pmul2r [lemma, in mathcomp.ssreflect.div]
dvdn_pmul2l [lemma, in mathcomp.ssreflect.div]
dvdn_leq [lemma, in mathcomp.ssreflect.div]
dvdn_odd [lemma, in mathcomp.ssreflect.div]
dvdn_eq [lemma, in mathcomp.ssreflect.div]
dvdn_trans [lemma, in mathcomp.ssreflect.div]
dvdn_mul [lemma, in mathcomp.ssreflect.div]
dvdn_mulr [lemma, in mathcomp.ssreflect.div]
dvdn_mull [lemma, in mathcomp.ssreflect.div]
dvdn_gt0 [lemma, in mathcomp.ssreflect.div]
dvdn_orderC [lemma, in mathcomp.field.algnum]
dvdn_constt_Res1_irr1 [lemma, in mathcomp.character.inertia]
dvdn_exponent [lemma, in mathcomp.solvable.abelian]
dvdn_orbit [lemma, in mathcomp.fingroup.action]
dvdn_cforder [lemma, in mathcomp.character.classfun]
dvdn_cforderP [lemma, in mathcomp.character.classfun]
dvdn_prim_root [lemma, in mathcomp.algebra.poly]
dvdn_biggcdP [lemma, in mathcomp.ssreflect.bigop]
dvdn_biglcmP [lemma, in mathcomp.ssreflect.bigop]
dvdn_cardMg [lemma, in mathcomp.fingroup.fingroup]
dvdn_indexg [lemma, in mathcomp.fingroup.fingroup]
dvdn_prime_cyclic [lemma, in mathcomp.solvable.cyclic]
dvdn0 [lemma, in mathcomp.ssreflect.div]
dvdn1 [lemma, in mathcomp.ssreflect.div]
dvdn2 [lemma, in mathcomp.ssreflect.div]
dvdpP_rat_int [lemma, in mathcomp.algebra.intdiv]
dvdpP_int [lemma, in mathcomp.algebra.intdiv]
dvdp_separable [lemma, in mathcomp.field.separable]
dvdp_rat_int [lemma, in mathcomp.algebra.intdiv]
dvdz [definition, in mathcomp.algebra.intdiv]
dvdzE [lemma, in mathcomp.algebra.intdiv]
dvdzP [lemma, in mathcomp.algebra.intdiv]
dvdzz [lemma, in mathcomp.algebra.intdiv]
dvdz_contents [lemma, in mathcomp.algebra.intdiv]
dvdz_pexp2r [lemma, in mathcomp.algebra.intdiv]
dvdz_gcd [lemma, in mathcomp.algebra.intdiv]
dvdz_gcdl [lemma, in mathcomp.algebra.intdiv]
dvdz_gcdr [lemma, in mathcomp.algebra.intdiv]
dvdz_exp [lemma, in mathcomp.algebra.intdiv]
dvdz_zmod_closed [lemma, in mathcomp.algebra.intdiv]
dvdz_exp2r [lemma, in mathcomp.algebra.intdiv]
dvdz_Pexp2l [lemma, in mathcomp.algebra.intdiv]
dvdz_exp2l [lemma, in mathcomp.algebra.intdiv]
dvdz_mul2r [lemma, in mathcomp.algebra.intdiv]
dvdz_mul2l [lemma, in mathcomp.algebra.intdiv]
dvdz_eq [lemma, in mathcomp.algebra.intdiv]
dvdz_mod0P [lemma, in mathcomp.algebra.intdiv]
dvdz_trans [lemma, in mathcomp.algebra.intdiv]
dvdz_mul [lemma, in mathcomp.algebra.intdiv]
dvdz_mulr [lemma, in mathcomp.algebra.intdiv]
dvdz_mull [lemma, in mathcomp.algebra.intdiv]
dvdz_key [lemma, in mathcomp.algebra.intdiv]
dvdz0 [lemma, in mathcomp.algebra.intdiv]
dvdz1 [lemma, in mathcomp.algebra.intdiv]
dvd_irr1_index_center [lemma, in mathcomp.character.integral_char]
dvd_irr1_cardG [lemma, in mathcomp.character.integral_char]
dvd0C [lemma, in mathcomp.field.algC]
dvd0n [lemma, in mathcomp.ssreflect.div]
dvd0z [lemma, in mathcomp.algebra.intdiv]
dvd1n [lemma, in mathcomp.ssreflect.div]
dvd1z [lemma, in mathcomp.algebra.intdiv]

Global Index

Y

_

(24263 entries)

Notation Index

H

J

O

T

W

X

Y

_

(1399 entries)

Module Index

H

J

K

L

O

T

W

X

Y

Z

_

other

(226 entries)

Variable Index

J

W

X

Y

_

other

(3670 entries)

Library Index

K

L

O

U

W

X

Y

_

other

(89 entries)

Lemma Index

Y

_

other

(12297 entries)

Constructor Index

J

K

W

Y

_

other

(383 entries)

Axiom Index

D

G

H

J

K

L

M

N

O

Q

T

U

V

W

X

Y

Z

_

other

(45 entries)

Inductive Index

J

K

Q

W

Y

Z

_

other

(114 entries)

Projection Index

H

J

K

L

O

W

X

Y

_

other

(279 entries)

Section Index

J

W

X

Y

_

other

(1169 entries)

Abbreviation Index

Y

_

other

(742 entries)

Definition Index

Y

_

other

(3657 entries)

Record Index

B

H

J

K

L

O

W

X

Y

_

other

(193 entries)