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 (lemma)

decPcases [in ssrbool]
DecSocleType [in mxrepresentation]
dec_mxsimple_exists [in mxrepresentation]
dec_mx_reducible_semisimple [in mxrepresentation]
def_pnElem [in abelian]
degree_mxminpoly_map [in mxpoly]
degree_irr1 [in mxrepresentation]
degree_mxminpoly_proof [in mxpoly]
delta_mx_rshift [in matrix]
delta_mx_ushift [in matrix]
delta_mx_dshift [in matrix]
delta_mx_lshift [in matrix]
dergS [in commutator]
dergSn [in commutator]
derg0 [in commutator]
derg1 [in commutator]
derG1P [in commutator]
derivC [in poly]
derivD [in poly]
derivedP [in nilpotent]
derivM [in poly]
derivMn [in poly]
derivMNn [in poly]
derivN [in poly]
derivnC [in poly]
derivnD [in poly]
derivnMn [in poly]
derivnMNn [in poly]
derivnN [in poly]
derivnS [in poly]
derivnXn [in poly]
derivnZ [in poly]
derivn_map [in poly]
derivn_amulX [in poly]
derivn_poly0 [in poly]
derivn_linear_proof [in poly]
derivn0 [in poly]
derivn1 [in poly]
derivPn [in poly]
derivSn [in poly]
derivX [in poly]
derivXn [in poly]
derivZ [in poly]
deriv_linear_proof [in poly]
deriv_amulX [in poly]
deriv_poly_comp [in poly]
deriv_map [in poly]
deriv0 [in poly]
derJ [in commutator]
der_sub [in commutator]
der_subS [in commutator]
der_norm [in commutator]
der_normalS [in commutator]
der_abelian [in commutator]
der_normal [in commutator]
der_group_set [in commutator]
der_cprod [in nilpotent]
der_cont [in commutator]
der_char [in commutator]
der1_stab_Ohm1_SCN_series [in maximal]
der1_min [in commutator]
der1_joing_cycles [in commutator]
der1_subG [in fingroup]
der1_sub_rker [in mxrepresentation]
determinant_multilinear [in matrix]
determinant_alternate [in matrix]
detM [in matrix]
detV [in matrix]
det_mulmx [in matrix]
det_inv [in matrix]
det_scalar1 [in matrix]
det_perm [in matrix]
det_map_mx [in matrix]
det_scalemx [in matrix]
det_diag [in matrix]
det_tr [in matrix]
det_ublock [in matrix]
det_scalar [in matrix]
det_lblock [in matrix]
det0 [in matrix]
det0P [in mxalgebra]
det1 [in matrix]
dfsP [in fingraph]
diag_mx_comm [in matrix]
diag_mx_sum_delta [in matrix]
diag_const_mx [in matrix]
diag_mx_is_linear [in matrix]
diag_mxC [in matrix]
diffmxE [in mxalgebra]
diffmxSl [in mxalgebra]
diffmx_key [in mxalgebra]
diffvSl [in vector]
dihedral_classP [in extremal]
dihedral2_structure [in extremal]
dimvf [in vector]
dimvS [in vector]
dimv_leqif_eq [in vector]
dimv_disjoint_sum [in vector]
dimv_compl [in vector]
dimv_sum_leqif [in vector]
dimv_cap_compl [in vector]
dimv_leqif_sup [in vector]
dimv_sum_cap [in vector]
dimv_eq0 [in vector]
dimv_leq_sum [in vector]
dimv_sumw_leqif [in vector]
dimv0 [in vector]
dim_injv [in vector]
dim_span [in vector]
dim_abelemE [in mxabelem]
dinjectiveP [in fintype]
dinjectivePn [in fintype]
directvE [in vector]
directvEgeq [in vector]
directvP [in vector]
directv_sumP [in vector]
directv_sumE [in vector]
directv_sum_unique [in vector]
directv_addP [in vector]
directv_trivial [in vector]
directv_addE [in vector]
directv_add_unique [in vector]
disjoints_subset [in finset]
disjointU [in fintype]
disjointU1 [in fintype]
disjoint_has [in fintype]
disjoint_subset [in fintype]
disjoint_cat [in fintype]
disjoint_setI0 [in finset]
disjoint_cons [in fintype]
disjoint_trans [in fintype]
disjoint_sym [in fintype]
disjoint0 [in fintype]
disjoint1 [in fintype]
distnC [in ssrnat]
distnEl [in ssrnat]
distnEr [in ssrnat]
distnn [in ssrnat]
distnS [in ssrnat]
distn_add2l [in ssrnat]
distn_eq1 [in ssrnat]
distn_add2r [in ssrnat]
distn_eq0 [in ssrnat]
distn0 [in ssrnat]
distSn [in ssrnat]
dist0n [in ssrnat]
divCp_spec [in poly]
divgI [in fingroup]
divgrMid [in gproduct]
divgrMl [in gproduct]
divgr_id [in gproduct]
divgr_eq [in gproduct]
divgS [in fingroup]
divg_normal [in quotient]
divg_index [in fingroup]
divisorn [in prime]
divisors_uniq [in prime]
divisors_correct [in prime]
divisor1 [in prime]
divnAC [in div]
divnK [in div]
divnn [in div]
divn_divr [in div]
divn_pmul2r [in div]
divn_divl [in div]
divn_addl_mul [in div]
divn_mulCA [in div]
divn_gt0 [in div]
divn_pmul2l [in div]
divn_mulA [in div]
divn_small [in div]
divn_eq [in div]
divn_addl [in div]
divn_mulAC [in div]
divn_addr [in div]
divn0 [in div]
divn1 [in div]
divn2 [in div]
divp_mon_spec [in poly]
divp_mon_eq [in poly]
divp_spec [in poly]
divp_mull [in poly]
divp_size [in poly]
divp1 [in poly]
div_ring_mul_group_cyclic [in cyclic]
div0n [in div]
div0p [in poly]
DnQ_P [in extraspecial]
DnQ_pgroup [in extraspecial]
DnQ_extraspecial [in extraspecial]
domP [in morphism]
dom_hom_mx_module [in mxrepresentation]
dom_qactJ [in action]
dom_hom_invmx [in mxrepresentation]
dom_ker [in morphism]
doubleE [in ssrnat]
doubleK [in ssrnat]
doubleS [in ssrnat]
double_mulr [in ssrnat]
double_gt0 [in ssrnat]
double_add [in ssrnat]
double_mull [in ssrnat]
double_sub [in ssrnat]
double_eq0 [in ssrnat]
double0 [in ssrnat]
dprodA [in gproduct]
dprodC [in gproduct]
dprodE [in gproduct]
dprodEcprod [in gproduct]
dprodEsdprod [in gproduct]
dprodEY [in gproduct]
dprodg1 [in gproduct]
dprodmE [in gproduct]
dprodmEl [in gproduct]
dprodmEr [in gproduct]
dprodm_eqf [in gproduct]
dprodm_cprod [in gproduct]
dprodP [in gproduct]
dprodYP [in gproduct]
dprod_exponent [in abelian]
dprod_modl [in gproduct]
dprod_card [in gproduct]
dprod_modr [in gproduct]
dprod_abelem [in abelian]
dprod_normal2 [in gproduct]
dprod_nil [in nilpotent]
dprod1g [in gproduct]
drop_cat [in seq]
drop_size_cat [in seq]
drop_nth [in seq]
drop_size [in seq]
drop_cons [in seq]
drop_tupleP [in tuple]
drop_rcons [in seq]
drop_behead [in seq]
drop_oversize [in seq]
drop0 [in seq]
drop1 [in seq]
dtuple_on_subset [in primitive_action]
dtuple_on_add [in primitive_action]
dtuple_onP [in primitive_action]
dtuple_on_add_D1 [in primitive_action]
dvdMpP [in poly]
dvdnn [in div]
dvdnP [in div]
dvdn_lcml [in div]
dvdn_mulr [in div]
dvdn_gcd [in div]
dvdn_odd [in div]
dvdn_addr [in div]
dvdn_biglcmP [in bigop]
dvdn_pmul2r [in div]
dvdn_add_eq [in div]
dvdn_indexg [in fingroup]
dvdn_addl [in div]
dvdn_biggcdP [in bigop]
dvdn_leq_log [in prime]
dvdn_gcdl [in div]
dvdn_lcm_idl [in div]
dvdn_gcd_idr [in div]
dvdn_sum [in prime]
dvdn_cardMg [in fingroup]
dvdn_exp2r [in div]
dvdn_eq [in div]
dvdn_prime2 [in prime]
dvdn_exp2l [in div]
dvdn_lcm_idr [in div]
dvdn_morphim [in quotient]
dvdn_orbit [in action]
dvdn_Pexp2l [in div]
dvdn_gcd_idl [in div]
dvdn_lcmr [in div]
dvdn_gt0 [in div]
dvdn_mull [in div]
dvdn_sub [in div]
dvdn_exponent [in abelian]
dvdn_leq [in div]
dvdn_gcdr [in div]
dvdn_exp [in div]
dvdn_subr [in div]
dvdn_quotient [in quotient]
dvdn_pfactor [in prime]
dvdn_pmul2l [in div]
dvdn_mul [in div]
dvdn_part [in prime]
dvdn_prime_cyclic [in cyclic]
dvdn_lcm [in div]
dvdn_partP [in prime]
dvdn_pexp2r [in div]
dvdn_divisors [in prime]
dvdn_trans [in div]
dvdn_add [in div]
dvdn_subl [in div]
dvdn0 [in div]
dvdn1 [in div]
dvdn2 [in div]
dvdpp [in poly]
dvdpP [in poly]
dvdpPc [in poly]
dvdp_add_eq [in poly]
dvdp_gcd [in poly]
dvdp_addl [in poly]
dvdp_sub [in poly]
dvdp_gcd2 [in poly]
dvdp_mulr [in poly]
dvdp_mod [in poly]
dvdp_mul [in poly]
dvdp_addr [in poly]
dvdp_gcdl [in poly]
dvdp_mull [in poly]
dvdp_map [in poly]
dvdp_subr [in poly]
dvdp_subl [in poly]
dvdp_gcdr [in poly]
dvdp_add [in poly]
dvdp_trans [in poly]
dvdp0 [in poly]
dvd0n [in div]
dvd1n [in div]
dvd1p [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)