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

DecFieldMixin [abbreviation, in ssralg]
DecFieldType [abbreviation, in ssralg]
decFieldType [abbreviation, in ssralg]
DecidableField [module, 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]
delta_mx [definition, in matrix]
dependentReturnType [definition, in ssreflect]
der1_subG [lemma, in groups]
determinant [definition, in matrix]
Determinant [section, in matrix]
Determinant.R [variable, in matrix]
determinant_multilinear [lemma, in matrix]
detM [lemma, in matrix]
det1 [lemma, in matrix]
det_invmx [lemma, in matrix]
det_lblock [lemma, in matrix]
det_mulmx [lemma, in matrix]
det_perm_mx [lemma, in matrix]
det_perm_mx_neq0 [lemma, in matrix]
det_scalar [lemma, in matrix]
det_scalar1 [lemma, in matrix]
det_scalemx [lemma, in matrix]
det_trmx [lemma, in matrix]
det_ublock [lemma, in matrix]
dfs [definition, in connect]
dfsP [lemma, in connect]
DfsPath [constructor, in connect]
dfs_path [inductive, in connect]
diff_root [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]
divgI [lemma, in groups]
divgS [lemma, in groups]
divg_index [lemma, in groups]
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]
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]
div_ring_mul_group_cyclic [lemma, in cyclic]
dom [definition, in morphisms]
dom_ker [lemma, in morphisms]
dotmx_paste [lemma, in matrix]
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]
dpair [definition, in perm]
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_divisors [lemma, in prime]
dvdn_eq [lemma, in div]
dvdn_exp [lemma, in div]
dvdn_gcd [lemma, in div]
dvdn_gcdl [lemma, in div]
dvdn_gcdr [lemma, in div]
dvdn_gt0 [lemma, in div]
dvdn_indexg [lemma, in groups]
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_morphim [lemma, in normal]
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_pdiv [lemma, in prime]
dvdn_pfactor [lemma, in prime]
dvdn_pmul2l [lemma, in div]
dvdn_pmul2r [lemma, in div]
dvdn_prime2 [lemma, in prime]
dvdn_quotient [lemma, in normal]
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]
dvdpp [lemma, in poly]
dvdpPc [lemma, in poly]
dvdpPm [lemma, in poly]
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_gcd [lemma, in poly]
dvdp_gcdl [lemma, in poly]
dvdp_gcdr [lemma, in poly]
dvdp_gcd2 [lemma, in poly]
dvdp_mod [lemma, in poly]
dvdp_mon_mull [lemma, in poly]
dvdp_mul [lemma, in poly]
dvdp_mull [lemma, in poly]
dvdp_mulr [lemma, in poly]
dvdp_sub [lemma, in poly]
dvdp_subl [lemma, in poly]
dvdp_subr [lemma, in poly]
dvdp_trans [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 _ (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)