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 | (69505 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 | (1943 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 | (39748 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 | (379 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 | (3958 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 | (13542 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 | (480 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 | (45 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 | (452 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 | (1344 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 | (1014 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 | (6127 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 | (248 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 _ } (ring_scope) [in mathcomp.algebra.ssralg]

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

[ algType _ of _ for _ ] (form_scope) [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]

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

_ *^ _ _ (linear_ring_scope) [in mathcomp.algebra.ssralg]

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

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

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

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

{ linear _ } (ring_scope) [in mathcomp.algebra.ssralg]

{ linear _ | _ } (ring_scope) [in mathcomp.algebra.ssralg]

*:%R [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 _ } (ring_scope) [in mathcomp.algebra.ssralg]

{ lrmorphism _ | _ } (ring_scope) [in mathcomp.algebra.ssralg]

_ ^f [in mathcomp.algebra.ssralg]

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

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

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

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

{ rmorphism _ } (ring_scope) [in mathcomp.algebra.ssralg]

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

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

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

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

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

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

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

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

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

_ \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]

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

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

_ *: _ (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]

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]

_ - _ (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]

-%R (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]

*%R [in mathcomp.algebra.ssralg]

*:%R [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 | (69505 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 | (1943 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 | (39748 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 | (379 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 | (3958 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 | (13542 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 | (480 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 | (45 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 | (452 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 | (1344 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 | (1014 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 | (6127 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 | (248 entries) |