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 (14626 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 (165 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 (112 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 (7292 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 (761 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 (250 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 (390 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 (84 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 (3144 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 (126 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 (28 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 (2221 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 (53 entries)

D

d [abbreviation, in mxpoly]
DecField [module, in finalg]
DecidableField [module, in ssralg]
DecideRed [section, in mxrepresentation]
DecideRed.Definitions [section, in mxrepresentation]
DecideRed.Definitions.F [variable, in mxrepresentation]
DecideRed.Definitions.G [variable, in mxrepresentation]
DecideRed.Definitions.gT [variable, in mxrepresentation]
DecideRed.Definitions.n [variable, in mxrepresentation]
DecideRed.Definitions.rG [variable, in mxrepresentation]
DecideRed.F [variable, in mxrepresentation]
DecideRed.G [variable, in mxrepresentation]
DecideRed.gT [variable, in mxrepresentation]
DecideRed.n [variable, in mxrepresentation]
DecideRed.rG [variable, in mxrepresentation]
decP [definition, in ssrbool]
decPcases [lemma, in ssrbool]
DecSocleType [lemma, in mxrepresentation]
dec_mxsimple_exists [lemma, in mxrepresentation]
dec_mx_reducible_semisimple [lemma, in mxrepresentation]
Def [section, in finfun]
Def [section, in tuple]
defG [definition, in abelian]
Definitions [section, in frobenius]
Definitions.FrobeniusAction [section, in frobenius]
Definitions.FrobeniusAction.G [variable, in frobenius]
Definitions.FrobeniusAction.H [variable, in frobenius]
Definitions.FrobeniusAction.S [variable, in frobenius]
Definitions.FrobeniusAction.sT [variable, in frobenius]
Definitions.FrobeniusAction.to [variable, in frobenius]
Definitions.gT [variable, in frobenius]
defQ [definition, in extremal]
Defs [section, in gproduct]
Defs [section, in maximal]
Defs [section, in center]
Defs.gT [variable, in maximal]
Defs.gT [variable, in center]
Defs.gT [variable, in gproduct]
defU [definition, in mxrepresentation]
def_p [definition, in extremal]
def_q [definition, in extremal]
def_r [definition, in extremal]
def_q [definition, in extremal]
def_pnElem [lemma, in abelian]
def_n [definition, in extremal]
Def.aT [variable, in finfun]
Def.n [variable, in tuple]
Def.rT [variable, in finfun]
Def.T [variable, in tuple]
def2 [definition, in extremal]
def2qr [definition, in extremal]
degree_mxminpoly_map [lemma, in mxpoly]
degree_irr1 [lemma, in mxrepresentation]
degree_mxminpoly [definition, in mxpoly]
degree_mxminpoly_proof [lemma, in mxpoly]
delta_mx [definition, in matrix]
delta_mx_rshift [lemma, in matrix]
delta_mx_ushift [lemma, in matrix]
delta_mx_dshift [lemma, in matrix]
delta_mx_lshift [lemma, in matrix]
dependentReturnType [definition, in ssreflect]
dergS [lemma, in commutator]
dergSn [lemma, in commutator]
derg0 [lemma, in commutator]
derg1 [lemma, in commutator]
derG1P [lemma, in commutator]
deriv [definition, in poly]
Deriv [section, in poly]
derivC [lemma, in poly]
DerivC [section, in poly]
derivCE [definition, in poly]
DerivC.R [variable, in poly]
derivD [lemma, in poly]
derivE [definition, in poly]
DerivedBasics [section, in commutator]
DerivedBasics.gT [variable, in commutator]
derivedP [lemma, in nilpotent]
derived_at_rec [definition, in commutator]
derived_at_group [definition, in commutator]
derived_at [definition, in commutator]
derivM [lemma, in poly]
derivMn [lemma, in poly]
derivMNn [lemma, in poly]
derivN [lemma, in poly]
derivn [definition, in poly]
derivnC [lemma, in poly]
derivnD [lemma, in poly]
derivnMn [lemma, in poly]
derivnMNn [lemma, in poly]
derivnN [lemma, in poly]
derivnS [lemma, in poly]
derivnXn [lemma, in poly]
derivnZ [lemma, in poly]
derivn_linear [definition, in poly]
derivn_map [lemma, in poly]
derivn_amulX [lemma, in poly]
derivn_poly0 [lemma, in poly]
derivn_linear_proof [lemma, in poly]
derivn0 [lemma, in poly]
derivn1 [lemma, in poly]
derivPn [lemma, in poly]
derivSn [lemma, in poly]
derivX [lemma, in poly]
derivXn [lemma, in poly]
derivZ [lemma, in poly]
deriv_linear [definition, in poly]
deriv_linear_proof [lemma, in poly]
deriv_amulX [lemma, in poly]
deriv_poly_comp [lemma, in poly]
deriv_map [lemma, in poly]
Deriv.R [variable, in poly]
deriv0 [lemma, in poly]
derJ [lemma, in commutator]
der_sub [lemma, in commutator]
der_subS [lemma, in commutator]
der_norm [lemma, in commutator]
der_normalS [lemma, in commutator]
der_abelian [lemma, in commutator]
der_normal [lemma, in commutator]
der_mgFun [definition, in commutator]
der_gFun [definition, in commutator]
der_igFun [definition, in commutator]
der_group_set [lemma, in commutator]
der_cprod [lemma, in nilpotent]
der_cont [lemma, in commutator]
der_char [lemma, in commutator]
der1_stab_Ohm1_SCN_series [lemma, in maximal]
der1_min [lemma, in commutator]
der1_joing_cycles [lemma, in commutator]
der1_subG [lemma, in fingroup]
der1_sub_rker [lemma, in mxrepresentation]
determinant [definition, in matrix]
determinant_multilinear [lemma, in matrix]
determinant_alternate [lemma, in matrix]
detM [lemma, in matrix]
detV [lemma, in matrix]
det_mulmx [lemma, in matrix]
det_inv [lemma, in matrix]
det_scalar1 [lemma, in matrix]
det_perm [lemma, in matrix]
det_map_mx [lemma, in matrix]
det_scalemx [lemma, in matrix]
det_diag [lemma, in matrix]
det_tr [lemma, in matrix]
det_ublock [lemma, in matrix]
det_scalar [lemma, in matrix]
det_lblock [lemma, in matrix]
det0 [lemma, in matrix]
det0P [lemma, in mxalgebra]
det1 [lemma, in matrix]
dfs [definition, in fingraph]
dfsP [lemma, in fingraph]
DfsPath [constructor, in fingraph]
dfs_path [inductive, in fingraph]
DgH [definition, in gproduct]
DgK [definition, in gproduct]
diagA [definition, in mxpoly]
diag_mx_comm [lemma, in matrix]
diag_mx_sum_delta [lemma, in matrix]
diag_const_mx [lemma, in matrix]
diag_mx [definition, in matrix]
diag_mx_is_linear [lemma, in matrix]
diag_mxC [lemma, in matrix]
diag_mx_linear [definition, in matrix]
diag_mx_additive [definition, in matrix]
diffmx [definition, in mxalgebra]
diffmxE [lemma, in mxalgebra]
diffmxSl [lemma, in mxalgebra]
diffmx_def [definition, in mxalgebra]
diffmx_key [lemma, in mxalgebra]
diffv [definition, in vector]
diffvSl [lemma, in vector]
diff_roots [definition, in poly]
Dihedral [constructor, in extremal]
dihedral_classP [lemma, in extremal]
dihedral_gtype [definition, in extremal]
dihedral2_structure [lemma, in extremal]
dimv [definition, in vector]
dimvf [lemma, in vector]
dimvS [lemma, in vector]
dimv_leqif_eq [lemma, in vector]
dimv_disjoint_sum [lemma, in vector]
dimv_compl [lemma, in vector]
dimv_sum_leqif [lemma, in vector]
dimv_cap_compl [lemma, in vector]
dimv_leqif_sup [lemma, in vector]
dimv_sum_cap [lemma, in vector]
dimv_eq0 [lemma, in vector]
dimv_leq_sum [lemma, in vector]
dimv_sumw_leqif [lemma, in vector]
dimv0 [lemma, in vector]
dim_injv [lemma, in vector]
dim_span [lemma, in vector]
dim_abelemE [lemma, in mxabelem]
dinjectiveb [definition, in fintype]
dinjectiveP [lemma, in fintype]
dinjectivePn [lemma, in fintype]
directv [abbreviation, in vector]
directv [abbreviation, in vector]
directvE [lemma, in vector]
directvEgeq [lemma, in vector]
directvP [lemma, in vector]
directv_sumP [lemma, in vector]
directv_sumE [lemma, in vector]
directv_sum_recP [definition, in vector]
directv_sum_unique [lemma, in vector]
directv_addP [lemma, in vector]
directv_def [definition, in vector]
directv_trivial [lemma, in vector]
directv_addE [lemma, in vector]
directv_add_unique [lemma, in vector]
direct_product [definition, in gproduct]
DirprodIsom [section, in gproduct]
DirprodIsom.gT [variable, in gproduct]
disjoint [definition, in fintype]
disjoints_subset [lemma, in finset]
disjointU [lemma, in fintype]
disjointU1 [lemma, in fintype]
disjoint_has [lemma, in fintype]
disjoint_subset [lemma, in fintype]
disjoint_cat [lemma, in fintype]
disjoint_setI0 [lemma, in finset]
disjoint_cons [lemma, in fintype]
disjoint_trans [lemma, in fintype]
disjoint_sym [lemma, in fintype]
disjoint0 [lemma, in fintype]
disjoint1 [lemma, in fintype]
distn [definition, in ssrnat]
DistnArg [constructor, in ssrnat]
distnC [lemma, in ssrnat]
distnEl [lemma, in ssrnat]
distnEr [lemma, in ssrnat]
distnn [lemma, in ssrnat]
distnS [lemma, in ssrnat]
distn_add2l [lemma, in ssrnat]
distn_eq1 [lemma, in ssrnat]
distn_arg [inductive, in ssrnat]
distn_add2r [lemma, in ssrnat]
distn_eq0 [lemma, in ssrnat]
distn0 [lemma, in ssrnat]
Distributivity [section, in bigop]
Distributivity.one [variable, in bigop]
Distributivity.plus [variable, in bigop]
Distributivity.R [variable, in bigop]
Distributivity.times [variable, in bigop]
Distributivity.zero [variable, in bigop]
distSn [lemma, in ssrnat]
dist0n [lemma, in ssrnat]
div [library]
divCp_spec [lemma, in poly]
divgI [lemma, in fingroup]
divgr [definition, in gproduct]
divgrMid [lemma, in gproduct]
divgrMl [lemma, in gproduct]
divgr_id [lemma, in gproduct]
divgr_eq [lemma, in gproduct]
divgS [lemma, in fingroup]
divg_normal [lemma, in quotient]
divg_index [lemma, in fingroup]
divisorn [lemma, in prime]
divisors [definition, in prime]
divisors_uniq [lemma, in prime]
divisors_correct [lemma, in prime]
divisor1 [lemma, in prime]
divn [definition, in div]
divnAC [lemma, in div]
divnK [lemma, in div]
divnn [lemma, in div]
divn_divr [lemma, in div]
divn_pmul2r [lemma, in div]
divn_divl [lemma, in div]
divn_addl_mul [lemma, in div]
divn_mulCA [lemma, in div]
divn_gt0 [lemma, in div]
divn_pmul2l [lemma, in div]
divn_mulA [lemma, in div]
divn_small [lemma, in div]
divn_eq [lemma, in div]
divn_addl [lemma, in div]
divn_mulAC [lemma, in div]
divn_addr [lemma, in div]
divn0 [lemma, in div]
divn1 [lemma, in div]
divn2 [lemma, in div]
divp [definition, in poly]
divp_mon_spec [lemma, in poly]
divp_mon_eq [lemma, in poly]
divp_spec [lemma, in poly]
divp_mull [lemma, in poly]
divp_size [lemma, in poly]
divp1 [lemma, in poly]
div_ring_mul_group_cyclic [lemma, in cyclic]
div0n [lemma, in div]
div0p [lemma, in poly]
dlsubmx [definition, in matrix]
DnQ_P [lemma, in extraspecial]
DnQ_pgroup [lemma, in extraspecial]
DnQ_extraspecial [lemma, in extraspecial]
dom [definition, in morphism]
dom [abbreviation, in action]
domG [definition, in automorphism]
domG [definition, in automorphism]
domP [lemma, in morphism]
dom_hom_mx_module [lemma, in mxrepresentation]
dom_qactJ [lemma, in action]
dom_hom_invmx [lemma, in mxrepresentation]
dom_hom_mx [definition, in mxrepresentation]
dom_ker [lemma, in morphism]
double [definition, in ssrnat]
doubleE [lemma, in ssrnat]
doubleK [lemma, in ssrnat]
doubleS [lemma, in ssrnat]
double_mulr [lemma, in ssrnat]
double_gt0 [lemma, in ssrnat]
double_inj [definition, in ssrnat]
double_add [lemma, in ssrnat]
double_rec [definition, in ssrnat]
double_mull [lemma, in ssrnat]
double_sub [lemma, in ssrnat]
double_eq0 [lemma, in ssrnat]
double0 [lemma, in ssrnat]
dp [definition, in mxpoly]
dpair [definition, in perm]
dprod [abbreviation, in gproduct]
dprod [abbreviation, in gproduct]
dprodA [lemma, in gproduct]
dprodC [lemma, in gproduct]
dprodE [lemma, in gproduct]
dprodEcprod [lemma, in gproduct]
dprodEsdprod [lemma, in gproduct]
dprodEY [lemma, in gproduct]
dprodg1 [lemma, in gproduct]
dprodm [definition, in gproduct]
dprodmE [lemma, in gproduct]
dprodmEl [lemma, in gproduct]
dprodmEr [lemma, in gproduct]
dprodm_morphism [definition, in gproduct]
dprodm_eqf [lemma, in gproduct]
dprodm_cprod [lemma, in gproduct]
dprodP [lemma, in gproduct]
dprodYP [lemma, in gproduct]
dprod_abelaw [definition, in gproduct]
dprod_law [definition, in gproduct]
dprod_exponent [lemma, in abelian]
dprod_modl [lemma, in gproduct]
dprod_card [lemma, in gproduct]
dprod_modr [lemma, in gproduct]
dprod_abelem [lemma, in abelian]
dprod_normal2 [lemma, in gproduct]
dprod_nil [lemma, in nilpotent]
dprod1g [lemma, in gproduct]
dq [definition, in mxpoly]
drop [definition, in seq]
drop_cat [lemma, in seq]
drop_size_cat [lemma, in seq]
drop_nth [lemma, in seq]
drop_size [lemma, in seq]
drop_cons [lemma, in seq]
drop_tuple [definition, in tuple]
drop_tupleP [lemma, in tuple]
drop_rcons [lemma, in seq]
drop_behead [lemma, in seq]
drop_oversize [lemma, in seq]
drop0 [lemma, in seq]
drop1 [lemma, in seq]
drsubmx [definition, in matrix]
dsubmx [definition, in matrix]
dsubmx_linear [definition, in matrix]
dsubmx_additive [definition, in matrix]
dtuple_on_subset [lemma, in primitive_action]
dtuple_on_add [lemma, in primitive_action]
dtuple_on [definition, in primitive_action]
dtuple_onP [lemma, in primitive_action]
dtuple_on_add_D1 [lemma, in primitive_action]
dvdMpP [lemma, in poly]
dvdn [definition, in div]
dvdnn [lemma, in div]
dvdnP [lemma, in div]
dvdn_lcml [lemma, in div]
dvdn_mulr [lemma, in div]
dvdn_gcd [lemma, in div]
dvdn_odd [lemma, in div]
dvdn_addr [lemma, in div]
dvdn_biglcmP [lemma, in bigop]
dvdn_pmul2r [lemma, in div]
dvdn_add_eq [lemma, in div]
dvdn_indexg [lemma, in fingroup]
dvdn_addl [lemma, in div]
dvdn_biggcdP [lemma, in bigop]
dvdn_leq_log [lemma, in prime]
dvdn_gcdl [lemma, in div]
dvdn_lcm_idl [lemma, in div]
dvdn_gcd_idr [lemma, in div]
dvdn_sum [lemma, in prime]
dvdn_cardMg [lemma, in fingroup]
dvdn_exp2r [lemma, in div]
dvdn_eq [lemma, in div]
dvdn_prime2 [lemma, in prime]
dvdn_exp2l [lemma, in div]
dvdn_lcm_idr [lemma, in div]
dvdn_morphim [lemma, in quotient]
dvdn_orbit [lemma, in action]
dvdn_Pexp2l [lemma, in div]
dvdn_gcd_idl [lemma, in div]
dvdn_lcmr [lemma, in div]
dvdn_gt0 [lemma, in div]
dvdn_mull [lemma, in div]
dvdn_sub [lemma, in div]
dvdn_exponent [lemma, in abelian]
dvdn_leq [lemma, in div]
dvdn_gcdr [lemma, in div]
dvdn_exp [lemma, in div]
dvdn_subr [lemma, in div]
dvdn_quotient [lemma, in quotient]
dvdn_pfactor [lemma, in prime]
dvdn_pmul2l [lemma, in div]
dvdn_mul [lemma, in div]
dvdn_part [lemma, in prime]
dvdn_prime_cyclic [lemma, in cyclic]
dvdn_lcm [lemma, in div]
dvdn_partP [lemma, in prime]
dvdn_pexp2r [lemma, in div]
dvdn_divisors [lemma, in prime]
dvdn_trans [lemma, in div]
dvdn_add [lemma, in div]
dvdn_subl [lemma, in div]
dvdn0 [lemma, in div]
dvdn1 [lemma, in div]
dvdn2 [lemma, in div]
dvdp [definition, in poly]
dvdpp [lemma, in poly]
dvdpP [lemma, in poly]
dvdpPc [lemma, in poly]
dvdp_add_eq [lemma, in poly]
dvdp_gcd [lemma, in poly]
dvdp_addl [lemma, in poly]
dvdp_sub [lemma, in poly]
dvdp_gcd2 [lemma, in poly]
dvdp_mulr [lemma, in poly]
dvdp_mod [lemma, in poly]
dvdp_mul [lemma, in poly]
dvdp_addr [lemma, in poly]
dvdp_gcdl [lemma, in poly]
dvdp_mull [lemma, in poly]
dvdp_map [lemma, in poly]
dvdp_subr [lemma, in poly]
dvdp_subl [lemma, in poly]
dvdp_gcdr [lemma, in poly]
dvdp_add [lemma, in poly]
dvdp_trans [lemma, in poly]
dvdp0 [lemma, in poly]
dvd0n [lemma, in div]
dvd1n [lemma, in div]
dvd1p [lemma, in poly]



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 (14626 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 (165 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 (112 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 (7292 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 (761 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 (250 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 (390 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 (84 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 (3144 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 (126 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 (28 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 (2221 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 (53 entries)