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 | (100113 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 | (1864 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 | (49278 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 | (1631 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 | (6978 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 | (14781 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 | (75 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) |

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 | (2030 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 | (2189 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 | (1149 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 | (19126 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 | (565 entries) |

## G (notation)

'Gal ( _ / _ ) (Group_scope) [in mathcomp.field.galois]'Gal ( _ / _ ) (group_scope) [in mathcomp.field.galois]

'K_ _ (ring_scope) [in mathcomp.character.integral_char]

[ mgFun of _ ] (form_scope) [in mathcomp.solvable.gfunctor]

[ mgFun by _ ] (form_scope) [in mathcomp.solvable.gfunctor]

[ pgFun of _ ] (form_scope) [in mathcomp.solvable.gfunctor]

[ pgFun by _ ] (form_scope) [in mathcomp.solvable.gfunctor]

[ gFun of _ ] (form_scope) [in mathcomp.solvable.gfunctor]

[ gFun by _ ] (form_scope) [in mathcomp.solvable.gfunctor]

[ igFun of _ ] (form_scope) [in mathcomp.solvable.gfunctor]

[ igFun by _ & ! _ ] (form_scope) [in mathcomp.solvable.gfunctor]

[ igFun by _ & _ ] (form_scope) [in mathcomp.solvable.gfunctor]

[ additive of _ ] (form_scope) [in mathcomp.algebra.ssralg]

[ additive of _ as _ ] (form_scope) [in mathcomp.algebra.ssralg]

{ additive _ -> _ } (type_scope) [in mathcomp.algebra.ssralg]

[ algType _ of _ ] (form_scope) [in mathcomp.algebra.ssralg]

[ algType _ of _ for _ ] (form_scope) [in mathcomp.algebra.ssralg]

_ * _ [in mathcomp.algebra.ssralg]

1 [in mathcomp.algebra.ssralg]

[ closedFieldType of _ ] (form_scope) [in mathcomp.algebra.ssralg]

[ closedFieldType of _ for _ ] (form_scope) [in mathcomp.algebra.ssralg]

[ comAlgType _ of _ ] (form_scope) [in mathcomp.algebra.ssralg]

[ comRingType of _ ] (form_scope) [in mathcomp.algebra.ssralg]

[ comRingType of _ for _ ] (form_scope) [in mathcomp.algebra.ssralg]

[ comSemiRingType of _ ] (form_scope) [in mathcomp.algebra.ssralg]

[ comSemiRingType of _ for _ ] (form_scope) [in mathcomp.algebra.ssralg]

[ comUnitAlgType _ of _ ] (form_scope) [in mathcomp.algebra.ssralg]

[ comUnitRingType of _ ] (form_scope) [in mathcomp.algebra.ssralg]

[ decFieldType of _ ] (form_scope) [in mathcomp.algebra.ssralg]

[ decFieldType of _ for _ ] (form_scope) [in mathcomp.algebra.ssralg]

[ rec _ , _ ] [in mathcomp.algebra.ssralg]

[ fieldType of _ ] (form_scope) [in mathcomp.algebra.ssralg]

[ fieldType of _ for _ ] (form_scope) [in mathcomp.algebra.ssralg]

[ idomainType of _ ] (form_scope) [in mathcomp.algebra.ssralg]

[ idomainType of _ for _ ] (form_scope) [in mathcomp.algebra.ssralg]

[ lalgType _ of _ ] (form_scope) [in mathcomp.algebra.ssralg]

[ lalgType _ of _ for _ ] (form_scope) [in mathcomp.algebra.ssralg]

[ linear of _ ] (form_scope) [in mathcomp.algebra.ssralg]

[ linear of _ as _ ] (form_scope) [in mathcomp.algebra.ssralg]

{ scalar _ } (type_scope) [in mathcomp.algebra.ssralg]

{ linear _ -> _ } (type_scope) [in mathcomp.algebra.ssralg]

{ linear _ -> _ | _ } (type_scope) [in mathcomp.algebra.ssralg]

[ lmodType _ of _ ] (form_scope) [in mathcomp.algebra.ssralg]

[ lmodType _ of _ for _ ] (form_scope) [in mathcomp.algebra.ssralg]

[ lrmorphism of _ ] (form_scope) [in mathcomp.algebra.ssralg]

{ lrmorphism _ -> _ } (type_scope) [in mathcomp.algebra.ssralg]

{ lrmorphism _ -> _ | _ } (type_scope) [in mathcomp.algebra.ssralg]

[ nmodType of _ ] (form_scope) [in mathcomp.algebra.ssralg]

[ nmodType of _ for _ ] (form_scope) [in mathcomp.algebra.ssralg]

[ ringType of _ ] (form_scope) [in mathcomp.algebra.ssralg]

[ ringType of _ for _ ] (form_scope) [in mathcomp.algebra.ssralg]

_ ^f [in mathcomp.algebra.ssralg]

[ rmorphism of _ ] (form_scope) [in mathcomp.algebra.ssralg]

[ rmorphism of _ as _ ] (form_scope) [in mathcomp.algebra.ssralg]

{ rmorphism _ -> _ } (type_scope) [in mathcomp.algebra.ssralg]

[ semiRingType of _ ] (form_scope) [in mathcomp.algebra.ssralg]

[ semiRingType of _ for _ ] (form_scope) [in mathcomp.algebra.ssralg]

_ ^f [in mathcomp.algebra.ssralg]

[ SubIntegralDomain_isSubField of _ by <: ] (form_scope) [in mathcomp.algebra.ssralg]

[ SubChoice_isSubIntegralDomain of _ by <: ] (form_scope) [in mathcomp.algebra.ssralg]

[ SubComUnitRing_isSubIntegralDomain of _ by <: ] (form_scope) [in mathcomp.algebra.ssralg]

[ SubChoice_isSubComUnitRing of _ by <: ] (form_scope) [in mathcomp.algebra.ssralg]

[ SubChoice_isSubUnitRing of _ by <: ] (form_scope) [in mathcomp.algebra.ssralg]

[ SubRing_isSubUnitRing of _ by <: ] (form_scope) [in mathcomp.algebra.ssralg]

[ SubChoice_isSubAlgebra of _ by <: ] (form_scope) [in mathcomp.algebra.ssralg]

[ SubLalgebra_isSubAlgebra of _ by <: ] (form_scope) [in mathcomp.algebra.ssralg]

[ SubChoice_isSubLalgebra of _ by <: ] (form_scope) [in mathcomp.algebra.ssralg]

[ SubRing_SubLmodule_isSubLalgebra of _ by <: ] (form_scope) [in mathcomp.algebra.ssralg]

[ SubChoice_isSubLmodule of _ by <: ] (form_scope) [in mathcomp.algebra.ssralg]

[ SubZmodule_isSubLmodule of _ by <: ] (form_scope) [in mathcomp.algebra.ssralg]

[ SubChoice_isSubComRing of _ by <: ] (form_scope) [in mathcomp.algebra.ssralg]

[ SubRing_isSubComRing of _ by <: ] (form_scope) [in mathcomp.algebra.ssralg]

[ SubChoice_isSubRing of _ by <: ] (form_scope) [in mathcomp.algebra.ssralg]

[ SubZmodule_isSubRing of _ by <: ] (form_scope) [in mathcomp.algebra.ssralg]

[ SubChoice_isSubComSemiRing of _ by <: ] (form_scope) [in mathcomp.algebra.ssralg]

[ SubSemiRing_isSubComSemiRing of _ by <: ] (form_scope) [in mathcomp.algebra.ssralg]

[ SubChoice_isSubSemiRing of _ by <: ] (form_scope) [in mathcomp.algebra.ssralg]

[ SubNmodule_isSubSemiRing of _ by <: ] (form_scope) [in mathcomp.algebra.ssralg]

[ SubChoice_isSubZmodule of _ by <: ] (form_scope) [in mathcomp.algebra.ssralg]

[ SubChoice_isSubNmodule of _ by <: ] (form_scope) [in mathcomp.algebra.ssralg]

[ unitAlgType _ of _ ] (form_scope) [in mathcomp.algebra.ssralg]

[ unitRingType of _ ] (form_scope) [in mathcomp.algebra.ssralg]

[ unitRingType of _ for _ ] (form_scope) [in mathcomp.algebra.ssralg]

[ zmodType of _ ] (form_scope) [in mathcomp.algebra.ssralg]

[ zmodType of _ for _ ] (form_scope) [in mathcomp.algebra.ssralg]

*:%R (fun_scope) [in mathcomp.algebra.ssralg]

*%R (fun_scope) [in mathcomp.algebra.ssralg]

+%R (fun_scope) [in mathcomp.algebra.ssralg]

_ \* _ (ring_scope) [in mathcomp.algebra.ssralg]

_ \o* _ (ring_scope) [in mathcomp.algebra.ssralg]

_ \*o _ (ring_scope) [in mathcomp.algebra.ssralg]

_ \*: _ (ring_scope) [in mathcomp.algebra.ssralg]

\- _ (ring_scope) [in mathcomp.algebra.ssralg]

_ \- _ (ring_scope) [in mathcomp.algebra.ssralg]

_ \+ _ (ring_scope) [in mathcomp.algebra.ssralg]

\0 (ring_scope) [in mathcomp.algebra.ssralg]

_ %:A (ring_scope) [in mathcomp.algebra.ssralg]

_ *: _ (ring_scope) [in mathcomp.algebra.ssralg]

- 1 (ring_scope) [in mathcomp.algebra.ssralg]

[ char _ ] (ring_scope) [in mathcomp.algebra.ssralg]

_ ^+ _ (ring_scope) [in mathcomp.algebra.ssralg]

_ * _ (ring_scope) [in mathcomp.algebra.ssralg]

_ %:R (ring_scope) [in mathcomp.algebra.ssralg]

1 (ring_scope) [in mathcomp.algebra.ssralg]

_ *- _ (ring_scope) [in mathcomp.algebra.ssralg]

_ - _ (ring_scope) [in mathcomp.algebra.ssralg]

- _ (ring_scope) [in mathcomp.algebra.ssralg]

-%R (ring_scope) [in mathcomp.algebra.ssralg]

_ `_ _ (ring_scope) [in mathcomp.algebra.ssralg]

_ *+ _ (ring_scope) [in mathcomp.algebra.ssralg]

_ + _ (ring_scope) [in mathcomp.algebra.ssralg]

0 (ring_scope) [in mathcomp.algebra.ssralg]

'forall 'X_ _ , _ (term_scope) [in mathcomp.algebra.ssralg]

'exists 'X_ _ , _ (term_scope) [in mathcomp.algebra.ssralg]

_ != _ (term_scope) [in mathcomp.algebra.ssralg]

~ _ (term_scope) [in mathcomp.algebra.ssralg]

_ ==> _ (term_scope) [in mathcomp.algebra.ssralg]

_ \/ _ (term_scope) [in mathcomp.algebra.ssralg]

_ /\ _ (term_scope) [in mathcomp.algebra.ssralg]

_ == _ (term_scope) [in mathcomp.algebra.ssralg]

_ ^+ _ (term_scope) [in mathcomp.algebra.ssralg]

_ / _ (term_scope) [in mathcomp.algebra.ssralg]

_ ^-1 (term_scope) [in mathcomp.algebra.ssralg]

_ *+ _ (term_scope) [in mathcomp.algebra.ssralg]

_ * _ (term_scope) [in mathcomp.algebra.ssralg]

_ - _ (term_scope) [in mathcomp.algebra.ssralg]

- _ (term_scope) [in mathcomp.algebra.ssralg]

_ + _ (term_scope) [in mathcomp.algebra.ssralg]

1 (term_scope) [in mathcomp.algebra.ssralg]

0 (term_scope) [in mathcomp.algebra.ssralg]

_ %:T (term_scope) [in mathcomp.algebra.ssralg]

_ %:R (term_scope) [in mathcomp.algebra.ssralg]

'X_ _ (term_scope) [in mathcomp.algebra.ssralg]

_ ^o (type_scope) [in mathcomp.algebra.ssralg]

_ ^c (type_scope) [in mathcomp.algebra.ssralg]

_ ^- _ [in mathcomp.algebra.ssralg]

_ / _ [in mathcomp.algebra.ssralg]

_ ^-1 [in mathcomp.algebra.ssralg]

\prod_ ( _ <= _ < _ ) _ [in mathcomp.algebra.ssralg]

\prod_ ( _ in _ ) _ [in mathcomp.algebra.ssralg]

\prod_ ( _ | _ ) _ [in mathcomp.algebra.ssralg]

\prod_ ( _ <- _ | _ ) _ [in mathcomp.algebra.ssralg]

\sum_ ( _ in _ ) _ [in mathcomp.algebra.ssralg]

\sum_ ( _ < _ ) _ [in mathcomp.algebra.ssralg]

\sum_ ( _ <= _ < _ ) _ [in mathcomp.algebra.ssralg]

\sum_ ( _ <- _ | _ ) _ [in mathcomp.algebra.ssralg]

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 | (100113 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 | (1864 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 | (49278 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 | (1631 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 | (6978 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 | (14781 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 | (75 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) |

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 | (2030 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 | (2189 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 | (1149 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 | (19126 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 | (565 entries) |