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 | (76754 entries) |

Notation 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 | (1892 entries) |

Binder 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 | (49588 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 | (305 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 | (4034 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 | (94 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 | (14802 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 | (222 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 | (9 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 | (131 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 | (43 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 | (1392 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 | (1140 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 | (3066 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 | (36 entries) |

## D (definition)

daddv_pi [in mathcomp.algebra.vector]dadd_grepr [in mathcomp.character.character]

dchi [in mathcomp.character.vcharacter]

decidable_embedding [in mathcomp.field.algebraics_fundamentals]

defaultEncModRel [in mathcomp.ssreflect.generic_quotient]

defaultEncModRelClass [in mathcomp.ssreflect.generic_quotient]

degree_mxminpoly [in mathcomp.algebra.mxpoly]

delta_mx [in mathcomp.algebra.matrix]

denq [in mathcomp.algebra.rat]

denq_ge0 [in mathcomp.algebra.rat]

deprecated_CanEqMixin [in mathcomp.ssreflect.eqtype]

deprecated_PcanEqMixin [in mathcomp.ssreflect.eqtype]

deprecated_InjEqMixin [in mathcomp.ssreflect.eqtype]

deriv [in mathcomp.algebra.poly]

Derivation [in mathcomp.field.separable]

derivCE [in mathcomp.algebra.poly]

derivE [in mathcomp.algebra.poly]

derived_at_group [in mathcomp.solvable.commutator]

derived_at [in mathcomp.solvable.commutator]

derived_at_rec [in mathcomp.solvable.commutator]

derivn [in mathcomp.algebra.poly]

der_mgFun [in mathcomp.solvable.commutator]

der_gFun [in mathcomp.solvable.commutator]

der_igFun [in mathcomp.solvable.commutator]

determinant [in mathcomp.algebra.matrix]

detRepr [in mathcomp.character.character]

det_repr [in mathcomp.character.character]

det_repr_mx [in mathcomp.character.character]

dfinfun_of [in mathcomp.ssreflect.finfun]

dfs [in mathcomp.ssreflect.fingraph]

diag_mx [in mathcomp.algebra.matrix]

diffmx_unlockable [in mathcomp.algebra.mxalgebra]

diffv [in mathcomp.algebra.vector]

diff_roots [in mathcomp.algebra.poly]

dihedral_gtype [in mathcomp.solvable.extremal]

dIirr [in mathcomp.character.vcharacter]

dimv [in mathcomp.algebra.vector]

dinjectiveb [in mathcomp.ssreflect.fintype]

directv_def [in mathcomp.algebra.vector]

direct_product [in mathcomp.fingroup.gproduct]

dirr [in mathcomp.character.vcharacter]

dirr_constt [in mathcomp.character.vcharacter]

dirr_dIirr [in mathcomp.character.vcharacter]

dirr1 [in mathcomp.character.vcharacter]

dir_iso3l [in mathcomp.solvable.burnside_app]

dir_iso3 [in mathcomp.solvable.burnside_app]

disjoint [in mathcomp.ssreflect.fintype]

diso_group3 [in mathcomp.solvable.burnside_app]

divgr [in mathcomp.fingroup.gproduct]

divisors [in mathcomp.ssreflect.prime]

divn [in mathcomp.ssreflect.div]

divq [in mathcomp.algebra.rat]

divz [in mathcomp.algebra.intdiv]

div_annihilant [in mathcomp.algebra.polyXY]

dlsubmx [in mathcomp.algebra.matrix]

dom [in mathcomp.fingroup.morphism]

dom_hom_mx [in mathcomp.character.mxrepresentation]

double [in mathcomp.ssreflect.ssrnat]

double_inj [in mathcomp.ssreflect.ssrnat]

double_rec [in mathcomp.ssreflect.ssrnat]

dpair [in mathcomp.fingroup.perm]

dprodl_Iirr [in mathcomp.character.character]

dprodm [in mathcomp.fingroup.gproduct]

dprodm_morphism [in mathcomp.fingroup.gproduct]

dprodr_Iirr [in mathcomp.character.character]

dprod_Iirr [in mathcomp.character.character]

drop [in mathcomp.ssreflect.seq]

drop_bseq [in mathcomp.ssreflect.tuple]

drop_tuple [in mathcomp.ssreflect.tuple]

drop_poly [in mathcomp.algebra.poly]

drsubmx [in mathcomp.algebra.matrix]

dsubmx [in mathcomp.algebra.matrix]

dtuple_on [in mathcomp.solvable.primitive_action]

dvdA [in mathcomp.field.algnum]

dvdn [in mathcomp.ssreflect.div]

dvdz [in mathcomp.algebra.intdiv]

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 | (76754 entries) |

Notation 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 | (1892 entries) |

Binder 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 | (49588 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 | (305 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 | (4034 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 | (94 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 | (14802 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 | (222 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 | (9 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 | (131 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 | (43 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 | (1392 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 | (1140 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 | (3066 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 | (36 entries) |