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 | (23233 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 | (1373 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 | (213 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 | (3475 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 | (89 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 | (11853 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 | (359 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 | (47 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 | (103 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 | (266 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 | (1118 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 | (691 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 | (3461 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 | (185 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]

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]

deriv [in mathcomp.algebra.poly]

Derivation [in mathcomp.field.separable]

derivCE [in mathcomp.algebra.poly]

derivE [in mathcomp.algebra.poly]

derived_at [in mathcomp.solvable.commutator]

derived_at_rec [in mathcomp.solvable.commutator]

derivn [in mathcomp.algebra.poly]

determinant [in mathcomp.algebra.matrix]

detRepr [in mathcomp.character.character]

det_repr_mx [in mathcomp.character.character]

dfs [in mathcomp.ssreflect.fingraph]

diag_mx [in mathcomp.algebra.matrix]

diffmx [in mathcomp.algebra.mxalgebra]

diffmx_def [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]

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]

dprodr_Iirr [in mathcomp.character.character]

dprod_Iirr [in mathcomp.character.character]

drop [in mathcomp.ssreflect.seq]

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 | (23233 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 | (1373 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 | (213 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 | (3475 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 | (89 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 | (11853 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 | (359 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 | (47 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 | (103 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 | (266 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 | (1118 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 | (691 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 | (3461 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 | (185 entries) |