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

decP [in ssrbool]
defG [in abelian]
defQ [in extremal]
defU [in mxrepresentation]
def_p [in extremal]
def_q [in extremal]
def_r [in extremal]
def_q [in extremal]
def_n [in extremal]
def2 [in extremal]
def2qr [in extremal]
degree_mxminpoly [in mxpoly]
delta_mx [in matrix]
dependentReturnType [in ssreflect]
deriv [in poly]
derivCE [in poly]
derivE [in poly]
derived_at_rec [in commutator]
derived_at_group [in commutator]
derived_at [in commutator]
derivn [in poly]
derivn_linear [in poly]
deriv_linear [in poly]
der_mgFun [in commutator]
der_gFun [in commutator]
der_igFun [in commutator]
determinant [in matrix]
dfs [in fingraph]
DgH [in gproduct]
DgK [in gproduct]
diagA [in mxpoly]
diag_mx [in matrix]
diag_mx_linear [in matrix]
diag_mx_additive [in matrix]
diffmx [in mxalgebra]
diffmx_def [in mxalgebra]
diffv [in vector]
diff_roots [in poly]
dihedral_gtype [in extremal]
dimv [in vector]
dinjectiveb [in fintype]
directv_sum_recP [in vector]
directv_def [in vector]
direct_product [in gproduct]
disjoint [in fintype]
distn [in ssrnat]
divgr [in gproduct]
divisors [in prime]
divn [in div]
divp [in poly]
dlsubmx [in matrix]
dom [in morphism]
domG [in automorphism]
domG [in automorphism]
dom_hom_mx [in mxrepresentation]
double [in ssrnat]
double_inj [in ssrnat]
double_rec [in ssrnat]
dp [in mxpoly]
dpair [in perm]
dprodm [in gproduct]
dprodm_morphism [in gproduct]
dprod_abelaw [in gproduct]
dprod_law [in gproduct]
dq [in mxpoly]
drop [in seq]
drop_tuple [in tuple]
drsubmx [in matrix]
dsubmx [in matrix]
dsubmx_linear [in matrix]
dsubmx_additive [in matrix]
dtuple_on [in primitive_action]
dvdn [in div]
dvdp [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)