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 | (71649 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 | (1792 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 | (46193 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 | (266 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 | (3623 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 | (91 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 | (14204 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 | (259 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 | (8 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 | (134 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 | (44 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 | (1276 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 | (682 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 | (3041 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) |

## N (abbreviation)

n [in mathcomp.field.fieldext]n [in mathcomp.field.fieldext]

n [in mathcomp.algebra.matrix]

n [in mathcomp.algebra.matrix]

n [in mathcomp.algebra.matrix]

n [in mathcomp.algebra.mxpoly]

n [in mathcomp.algebra.mxpoly]

n [in mathcomp.character.mxabelem]

n [in mathcomp.character.mxabelem]

n [in mathcomp.character.mxrepresentation]

n [in mathcomp.character.mxrepresentation]

n [in mathcomp.ssreflect.fintype]

natTrecE [in mathcomp.ssreflect.ssrnat]

NatTrec.doublen [in mathcomp.ssreflect.ssrnat]

NatTrec.oddn [in mathcomp.ssreflect.ssrnat]

nG [in mathcomp.character.mxrepresentation]

nG [in mathcomp.character.mxrepresentation]

Nil [in mathcomp.ssreflect.seq]

Nirr [in mathcomp.character.character]

Notations.rT [in mathcomp.fingroup.fingroup]

nth [in mathcomp.ssreflect.seq]

Num.bound [in mathcomp.algebra.ssrnum]

Num.Builders_186.lt [in mathcomp.algebra.ssrnum]

Num.Builders_186.le [in mathcomp.algebra.ssrnum]

Num.Builders_176.lt [in mathcomp.algebra.ssrnum]

Num.Builders_176.le [in mathcomp.algebra.ssrnum]

Num.comparable [in mathcomp.algebra.ssrnum]

Num.Def.comparabler [in mathcomp.algebra.ssrnum]

Num.Def.ger [in mathcomp.algebra.ssrnum]

Num.Def.gtr [in mathcomp.algebra.ssrnum]

Num.Def.ler [in mathcomp.algebra.ssrnum]

Num.Def.lerif [in mathcomp.algebra.ssrnum]

Num.Def.lterif [in mathcomp.algebra.ssrnum]

Num.Def.ltr [in mathcomp.algebra.ssrnum]

Num.Def.maxr [in mathcomp.algebra.ssrnum]

Num.Def.minr [in mathcomp.algebra.ssrnum]

Num.Def.normr [in mathcomp.algebra.ssrnum]

Num.ge [in mathcomp.algebra.ssrnum]

Num.gt [in mathcomp.algebra.ssrnum]

Num.le [in mathcomp.algebra.ssrnum]

Num.leif [in mathcomp.algebra.ssrnum]

Num.lt [in mathcomp.algebra.ssrnum]

Num.lteif [in mathcomp.algebra.ssrnum]

Num.max [in mathcomp.algebra.ssrnum]

Num.min [in mathcomp.algebra.ssrnum]

Num.neg [in mathcomp.algebra.ssrnum]

Num.nneg [in mathcomp.algebra.ssrnum]

Num.NumFieldExports.numFieldType [in mathcomp.algebra.ssrnum]

Num.pos [in mathcomp.algebra.ssrnum]

Num.real [in mathcomp.algebra.ssrnum]

Num.sg [in mathcomp.algebra.ssrnum]

Num.sqrt [in mathcomp.algebra.ssrnum]

Num.Theory.mid [in mathcomp.algebra.ssrnum]

Num.Theory.sqrtC [in mathcomp.algebra.ssrnum]

Num.Theory.sqrtC [in mathcomp.algebra.ssrnum]

n_comp [in mathcomp.ssreflect.fingraph]

n' [in mathcomp.character.mxabelem]

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 | (71649 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 | (1792 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 | (46193 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 | (266 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 | (3623 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 | (91 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 | (14204 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 | (259 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 | (8 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 | (134 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 | (44 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 | (1276 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 | (682 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 | (3041 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) |