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 _ (6599 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 _ (86 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 _ (57 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 _ (3455 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 _ (290 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 _ (147 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 _ (148 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 _ (53 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 _ (1466 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 _ (28 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 _ (53 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 _ (788 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 _ (28 entries)

D (lemma)

decPcases [in ssrbool]
der1_subG [in groups]
determinant_multilinear [in matrix]
detM [in matrix]
det1 [in matrix]
det_invmx [in matrix]
det_lblock [in matrix]
det_mulmx [in matrix]
det_perm_mx [in matrix]
det_perm_mx_neq0 [in matrix]
det_scalar [in matrix]
det_scalar1 [in matrix]
det_scalemx [in matrix]
det_trmx [in matrix]
det_ublock [in matrix]
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]
divgI [in groups]
divgS [in groups]
divg_index [in groups]
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]
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]
div_ring_mul_group_cyclic [in cyclic]
dom_ker [in morphisms]
dotmx_paste [in matrix]
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_divisors [in prime]
dvdn_eq [in div]
dvdn_exp [in div]
dvdn_gcd [in div]
dvdn_gcdl [in div]
dvdn_gcdr [in div]
dvdn_gt0 [in div]
dvdn_indexg [in groups]
dvdn_lcm [in div]
dvdn_lcml [in div]
dvdn_lcmr [in div]
dvdn_leq [in div]
dvdn_leq_log [in prime]
dvdn_morphim [in normal]
dvdn_mul [in div]
dvdn_mull [in div]
dvdn_mulr [in div]
dvdn_part [in prime]
dvdn_partP [in prime]
dvdn_pdiv [in prime]
dvdn_pfactor [in prime]
dvdn_pmul2l [in div]
dvdn_pmul2r [in div]
dvdn_prime2 [in prime]
dvdn_quotient [in normal]
dvdn_sub [in div]
dvdn_subl [in div]
dvdn_subr [in div]
dvdn_sum [in prime]
dvdn_trans [in div]
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_gcd [in poly]
dvdp_gcdl [in poly]
dvdp_gcdr [in poly]
dvdp_gcd2 [in poly]
dvdp_mod [in poly]
dvdp_mon_mull [in poly]
dvdp_mul [in poly]
dvdp_mull [in poly]
dvdp_mulr [in poly]
dvdp_sub [in poly]
dvdp_subl [in poly]
dvdp_subr [in poly]
dvdp_trans [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 _ (6599 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 _ (86 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 _ (57 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 _ (3455 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 _ (290 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 _ (147 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 _ (148 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 _ (53 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 _ (1466 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 _ (28 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 _ (53 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 _ (788 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 _ (28 entries)