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

decPcases [in ssrbool]
derivC [in poly]
derivnC [in poly]
derivnS [in poly]
derivnXn [in poly]
derivn0 [in poly]
derivn1 [in poly]
derivn_amulX [in poly]
derivn_mulr [in poly]
derivn_poly0 [in poly]
derivSn [in poly]
derivX [in poly]
derivXn [in poly]
deriv_add [in poly]
deriv_amulX [in poly]
deriv_mul [in poly]
deriv_mulr [in poly]
dfsP [in connect]
dinjectiveP [in fintype]
dinjectivePn [in fintype]
disjointEsetI [in finset]
disjoints_subset [in finset]
disjointU [in fintype]
disjointU1 [in fintype]
disjoint0 [in fintype]
disjoint1 [in fintype]
disjoint_cat [in fintype]
disjoint_cons [in fintype]
disjoint_has [in fintype]
disjoint_setI0 [in finset]
disjoint_subset [in fintype]
disjoint_sym [in fintype]
disjoint_trans [in fintype]
divisorn [in prime]
divisors_correct [in prime]
divisors_uniq [in prime]
divisor1 [in prime]
divnAC [in div]
divnK [in div]
divnn [in div]
divn0 [in div]
divn1 [in div]
divn2 [in div]
divn_addl [in div]
divn_addl_mul [in div]
divn_addr [in div]
divn_divl [in div]
divn_divr [in div]
divn_eq [in div]
divn_gt0 [in div]
divn_mulA [in div]
divn_mulAC [in div]
divn_mulCA [in div]
divn_pmul2l [in div]
divn_pmul2r [in div]
divn_small [in div]
divpp [in polydiv]
divp1 [in poly]
divp_mon_mull [in poly]
divp_mon_spec [in poly]
divp_mull [in poly]
divp_size [in poly]
divp_spec [in poly]
div0n [in div]
div0p [in poly]
doubleE [in ssrnat]
doubleK [in ssrnat]
doubleS [in ssrnat]
double0 [in ssrnat]
double_add [in ssrnat]
double_eq0 [in ssrnat]
double_gt0 [in ssrnat]
double_mull [in ssrnat]
double_mulr [in ssrnat]
double_sub [in ssrnat]
drop0 [in seq]
drop1 [in seq]
drop_behead [in seq]
drop_cat [in seq]
drop_cons [in seq]
drop_nth [in seq]
drop_oversize [in seq]
drop_rcons [in seq]
drop_size [in seq]
drop_size_cat [in seq]
drop_tupleP [in tuple]
dvdnn [in div]
dvdnP [in div]
dvdn0 [in div]
dvdn1 [in div]
dvdn2 [in div]
dvdn_add [in div]
dvdn_addl [in div]
dvdn_addr [in div]
dvdn_add_eq [in div]
dvdn_biggcdP [in bigops]
dvdn_biglcmP [in bigops]
dvdn_divisors [in prime]
dvdn_eq [in div]
dvdn_exp [in div]
dvdn_exp2l [in div]
dvdn_exp2r [in div]
dvdn_gcd [in div]
dvdn_gcdl [in div]
dvdn_gcdr [in div]
dvdn_gt0 [in div]
dvdn_lcm [in div]
dvdn_lcml [in div]
dvdn_lcmr [in div]
dvdn_leq [in div]
dvdn_leq_log [in prime]
dvdn_mul [in div]
dvdn_mull [in div]
dvdn_mulr [in div]
dvdn_part [in prime]
dvdn_partP [in prime]
dvdn_Pexp2l [in div]
dvdn_pexp2r [in div]
dvdn_pfactor [in prime]
dvdn_pmul2l [in div]
dvdn_pmul2r [in div]
dvdn_prime2 [in prime]
dvdn_sub [in div]
dvdn_subl [in div]
dvdn_subr [in div]
dvdn_sum [in prime]
dvdn_trans [in div]
dvdpn0 [in polydiv]
dvdpp [in poly]
dvdpPc [in poly]
dvdpPm [in poly]
dvdp0 [in poly]
dvdp_add [in poly]
dvdp_addl [in poly]
dvdp_addr [in poly]
dvdp_add_eq [in poly]
dvdp_eqp1 [in polydiv]
dvdp_gcd [in poly]
dvdp_gcdl [in poly]
dvdp_gcdr [in poly]
dvdp_gcd2 [in poly]
dvdp_gdco [in polydiv]
dvdp_map [in poly]
dvdp_mod [in poly]
dvdp_mon_mull [in poly]
dvdp_mul [in poly]
dvdp_mulIl [in polydiv]
dvdp_mulIr [in polydiv]
dvdp_mull [in poly]
dvdp_mulr [in poly]
dvdp_size_eqp [in polydiv]
dvdp_sub [in poly]
dvdp_subl [in poly]
dvdp_subr [in poly]
dvdp_trans [in poly]
dvd0n [in div]
dvd0p [in polydiv]
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 _ (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)