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 _ (5434 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 _ (89 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 _ (58 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 _ (2752 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 _ (233 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 _ (145 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 _ (139 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 _ (50 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 _ (1267 entries)
Moduleid 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 _ (47 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 _ (24 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 _ (609 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 _ (21 entries)

D

DecFieldMixin [abbreviation, in ssralg]
DecFieldType [abbreviation, in ssralg]
decFieldType [abbreviation, in ssralg]
DecidableField [moduleid, in ssralg]
decP [definition, in ssrbool]
decPcases [lemma, in ssrbool]
Def [section, in finfun]
Def [section, in tuple]
Def.aT [variable, in finfun]
Def.n [variable, in tuple]
Def.rT [variable, in finfun]
Def.T [variable, in tuple]
dependentReturnType [definition, in ssreflect]
deriv [definition, in poly]
Deriv [section, in poly]
derivC [lemma, in poly]
derivn [definition, in poly]
derivnC [lemma, in poly]
derivnS [lemma, in poly]
derivnXn [lemma, in poly]
derivn0 [lemma, in poly]
derivn1 [lemma, in poly]
derivn_amulX [lemma, in poly]
derivn_mulr [lemma, in poly]
derivn_poly0 [lemma, in poly]
derivSn [lemma, in poly]
derivX [lemma, in poly]
derivXn [lemma, in poly]
Deriv.R [variable, in poly]
deriv_add [lemma, in poly]
deriv_amulX [lemma, in poly]
deriv_mul [lemma, in poly]
deriv_mulr [lemma, in poly]
dfs [definition, in connect]
dfsP [lemma, in connect]
DfsPath [constructor, in connect]
dfs_path [inductive, in connect]
diff_roots [definition, in poly]
dinjectiveb [definition, in fintype]
dinjectiveP [lemma, in fintype]
dinjectivePn [lemma, in fintype]
disjoint [definition, in fintype]
disjointEsetI [lemma, in finset]
disjoints_subset [lemma, in finset]
disjointU [lemma, in fintype]
disjointU1 [lemma, in fintype]
disjoint0 [lemma, in fintype]
disjoint1 [lemma, in fintype]
disjoint_cat [lemma, in fintype]
disjoint_cons [lemma, in fintype]
disjoint_has [lemma, in fintype]
disjoint_setI0 [lemma, in finset]
disjoint_subset [lemma, in fintype]
disjoint_sym [lemma, in fintype]
disjoint_trans [lemma, in fintype]
Distributivity [section, in bigops]
Distributivity.one [variable, in bigops]
Distributivity.plus [variable, in bigops]
Distributivity.R [variable, in bigops]
Distributivity.times [variable, in bigops]
Distributivity.zero [variable, in bigops]
div [library]
divisorn [lemma, in prime]
divisors [definition, in prime]
divisors_correct [lemma, in prime]
divisors_uniq [lemma, in prime]
divisor1 [lemma, in prime]
divn [definition, in div]
divnAC [lemma, in div]
divnK [lemma, in div]
divnn [lemma, in div]
divn0 [lemma, in div]
divn1 [lemma, in div]
divn2 [lemma, in div]
divn_addl [lemma, in div]
divn_addl_mul [lemma, in div]
divn_addr [lemma, in div]
divn_divl [lemma, in div]
divn_divr [lemma, in div]
divn_eq [lemma, in div]
divn_gt0 [lemma, in div]
divn_mulA [lemma, in div]
divn_mulAC [lemma, in div]
divn_mulCA [lemma, in div]
divn_pmul2l [lemma, in div]
divn_pmul2r [lemma, in div]
divn_small [lemma, in div]
divp [definition, in poly]
divpp [lemma, in polydiv]
divpT [definition, in closedfields]
divp1 [lemma, in poly]
divp_mon_mull [lemma, in poly]
divp_mon_spec [lemma, in poly]
divp_mull [lemma, in poly]
divp_size [lemma, in poly]
divp_spec [lemma, in poly]
div0n [lemma, in div]
div0p [lemma, in poly]
double [definition, in ssrnat]
doubleE [lemma, in ssrnat]
doubleK [lemma, in ssrnat]
doubleS [lemma, in ssrnat]
double0 [lemma, in ssrnat]
double_add [lemma, in ssrnat]
double_eq0 [lemma, in ssrnat]
double_gt0 [lemma, in ssrnat]
double_inj [definition, in ssrnat]
double_mull [lemma, in ssrnat]
double_mulr [lemma, in ssrnat]
double_rec [definition, in ssrnat]
double_sub [lemma, in ssrnat]
drop [definition, in seq]
drop0 [lemma, in seq]
drop1 [lemma, in seq]
drop_behead [lemma, in seq]
drop_cat [lemma, in seq]
drop_cons [lemma, in seq]
drop_nth [lemma, in seq]
drop_oversize [lemma, in seq]
drop_rcons [lemma, in seq]
drop_size [lemma, in seq]
drop_size_cat [lemma, in seq]
drop_tuple [definition, in tuple]
drop_tupleP [lemma, in tuple]
dvdn [definition, in div]
dvdnn [lemma, in div]
dvdnP [lemma, in div]
dvdn0 [lemma, in div]
dvdn1 [lemma, in div]
dvdn2 [lemma, in div]
dvdn_add [lemma, in div]
dvdn_addl [lemma, in div]
dvdn_addr [lemma, in div]
dvdn_add_eq [lemma, in div]
dvdn_biggcdP [lemma, in bigops]
dvdn_biglcmP [lemma, in bigops]
dvdn_divisors [lemma, in prime]
dvdn_eq [lemma, in div]
dvdn_exp [lemma, in div]
dvdn_exp2l [lemma, in div]
dvdn_exp2r [lemma, in div]
dvdn_gcd [lemma, in div]
dvdn_gcdl [lemma, in div]
dvdn_gcdr [lemma, in div]
dvdn_gt0 [lemma, in div]
dvdn_lcm [lemma, in div]
dvdn_lcml [lemma, in div]
dvdn_lcmr [lemma, in div]
dvdn_leq [lemma, in div]
dvdn_leq_log [lemma, in prime]
dvdn_mul [lemma, in div]
dvdn_mull [lemma, in div]
dvdn_mulr [lemma, in div]
dvdn_part [lemma, in prime]
dvdn_partP [lemma, in prime]
dvdn_Pexp2l [lemma, in div]
dvdn_pexp2r [lemma, in div]
dvdn_pfactor [lemma, in prime]
dvdn_pmul2l [lemma, in div]
dvdn_pmul2r [lemma, in div]
dvdn_prime2 [lemma, in prime]
dvdn_sub [lemma, in div]
dvdn_subl [lemma, in div]
dvdn_subr [lemma, in div]
dvdn_sum [lemma, in prime]
dvdn_trans [lemma, in div]
dvdp [definition, in poly]
dvdpn0 [lemma, in polydiv]
dvdpp [lemma, in poly]
dvdpPc [lemma, in poly]
dvdpPm [lemma, in poly]
dvdpT [definition, in closedfields]
dvdp0 [lemma, in poly]
dvdp_add [lemma, in poly]
dvdp_addl [lemma, in poly]
dvdp_addr [lemma, in poly]
dvdp_add_eq [lemma, in poly]
dvdp_eqp1 [lemma, in polydiv]
dvdp_gcd [lemma, in poly]
dvdp_gcdl [lemma, in poly]
dvdp_gcdr [lemma, in poly]
dvdp_gcd2 [lemma, in poly]
dvdp_gdco [lemma, in polydiv]
dvdp_map [lemma, in poly]
dvdp_mod [lemma, in poly]
dvdp_mon_mull [lemma, in poly]
dvdp_mul [lemma, in poly]
dvdp_mulIl [lemma, in polydiv]
dvdp_mulIr [lemma, in polydiv]
dvdp_mull [lemma, in poly]
dvdp_mulr [lemma, in poly]
dvdp_size_eqp [lemma, in polydiv]
dvdp_sub [lemma, in poly]
dvdp_subl [lemma, in poly]
dvdp_subr [lemma, in poly]
dvdp_trans [lemma, in poly]
dvd0n [lemma, in div]
dvd0p [lemma, in polydiv]
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 _ (5434 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 _ (89 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 _ (58 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 _ (2752 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 _ (233 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 _ (145 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 _ (139 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 _ (50 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 _ (1267 entries)
Moduleid 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 _ (47 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 _ (24 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 _ (609 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 _ (21 entries)