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) |

## F (notation)

{ aspace _ } (type_scope) [in mathcomp.field.falgebra]'Z ( _ ) (vspace_scope) [in mathcomp.field.falgebra]

'C ( _ ) (vspace_scope) [in mathcomp.field.falgebra]

'C [ _ ] (vspace_scope) [in mathcomp.field.falgebra]

_ ^+ _ (vspace_scope) [in mathcomp.field.falgebra]

_ * _ (vspace_scope) [in mathcomp.field.falgebra]

[ FalgType _ of _ for _ ] (form_scope) [in mathcomp.field.falgebra]

[ FalgType _ of _ ] (form_scope) [in mathcomp.field.falgebra]

_ ^u [in mathcomp.character.classfun]

[ fieldExtType _ of _ for _ ] (form_scope) [in mathcomp.field.fieldext]

[ fieldExtType _ of _ ] (form_scope) [in mathcomp.field.fieldext]

{ subfield _ } (type_scope) [in mathcomp.field.fieldext]

_ *F: _ [in mathcomp.field.fieldext]

'Cl (action_scope) [in mathcomp.character.mxrepresentation]

'e_ _ (group_ring_scope) [in mathcomp.character.mxrepresentation]

'R_ _ (group_ring_scope) [in mathcomp.character.mxrepresentation]

'n_ _ (group_ring_scope) [in mathcomp.character.mxrepresentation]

1 (irrType_scope) [in mathcomp.character.mxrepresentation]

[ 1 _ ] (irrType_scope) [in mathcomp.character.mxrepresentation]

_ %| _ [in mathcomp.field.finfield]

_ ^%:A (ring_scope) [in mathcomp.field.finfield]

'Zm (action_scope) [in mathcomp.character.mxabelem]

[ finGroupType of _ ] (form_scope) [in mathcomp.fingroup.fingroup]

[ baseFinGroupType of _ ] (form_scope) [in mathcomp.fingroup.fingroup]

_ ^-1 [in mathcomp.fingroup.fingroup]

_ * _ [in mathcomp.fingroup.fingroup]

1 [in mathcomp.fingroup.fingroup]

'M (action_scope) [in mathcomp.solvable.finmodule]

'M (groupAction_scope) [in mathcomp.solvable.finmodule]

_ ^@ _ (ring_scope) [in mathcomp.solvable.finmodule]

'M (action_scope) [in mathcomp.solvable.finmodule]

'M (groupAction_scope) [in mathcomp.solvable.finmodule]

_ ^@ _ (ring_scope) [in mathcomp.solvable.finmodule]

, exists _ : _ in _ _ (bool_scope) [in mathcomp.ssreflect.fintype]

, exists _ in _ _ (bool_scope) [in mathcomp.ssreflect.fintype]

[ exists _ : _ in _ _ ] (bool_scope) [in mathcomp.ssreflect.fintype]

[ exists _ in _ _ ] (bool_scope) [in mathcomp.ssreflect.fintype]

[ exists ( _ : _ | _ ) _ ] (bool_scope) [in mathcomp.ssreflect.fintype]

[ exists ( _ | _ ) _ ] (bool_scope) [in mathcomp.ssreflect.fintype]

[ exists _ : _ _ ] (bool_scope) [in mathcomp.ssreflect.fintype]

[ exists _ _ ] (bool_scope) [in mathcomp.ssreflect.fintype]

, forall _ : _ in _ _ (bool_scope) [in mathcomp.ssreflect.fintype]

, forall _ in _ _ (bool_scope) [in mathcomp.ssreflect.fintype]

[ forall _ : _ in _ _ ] (bool_scope) [in mathcomp.ssreflect.fintype]

[ forall _ in _ _ ] (bool_scope) [in mathcomp.ssreflect.fintype]

[ forall ( _ : _ | _ ) _ ] (bool_scope) [in mathcomp.ssreflect.fintype]

[ forall ( _ | _ ) _ ] (bool_scope) [in mathcomp.ssreflect.fintype]

[ forall _ : _ _ ] (bool_scope) [in mathcomp.ssreflect.fintype]

[ forall _ _ ] (bool_scope) [in mathcomp.ssreflect.fintype]

, exists ( _ : _ | _ ) _ (fin_quant_scope) [in mathcomp.ssreflect.fintype]

, exists ( _ | _ ) _ (fin_quant_scope) [in mathcomp.ssreflect.fintype]

, exists _ : _ _ (fin_quant_scope) [in mathcomp.ssreflect.fintype]

, exists _ _ (fin_quant_scope) [in mathcomp.ssreflect.fintype]

, forall ( _ : _ | _ ) _ (fin_quant_scope) [in mathcomp.ssreflect.fintype]

, forall ( _ | _ ) _ (fin_quant_scope) [in mathcomp.ssreflect.fintype]

, forall _ : _ _ (fin_quant_scope) [in mathcomp.ssreflect.fintype]

, forall _ _ (fin_quant_scope) [in mathcomp.ssreflect.fintype]

, _ (fin_quant_scope) [in mathcomp.ssreflect.fintype]

_ ^~ [in mathcomp.ssreflect.fintype]

_ ^* [in mathcomp.ssreflect.fintype]

[ _ : _ | _ ] [in mathcomp.ssreflect.fintype]

[ _ | _ ] [in mathcomp.ssreflect.fintype]

[ finType of _ ] (form_scope) [in mathcomp.ssreflect.fintype]

[ finType of _ for _ ] (form_scope) [in mathcomp.ssreflect.fintype]

[ finAlgType _ of _ ] (form_scope) [in mathcomp.algebra.finalg]

[ finComRingType of _ ] (form_scope) [in mathcomp.algebra.finalg]

[ finComUnitRingType of _ ] (form_scope) [in mathcomp.algebra.finalg]

[ finFieldType of _ ] (form_scope) [in mathcomp.algebra.finalg]

[ finIdomainType of _ ] (form_scope) [in mathcomp.algebra.finalg]

[ finLalgType _ of _ ] (form_scope) [in mathcomp.algebra.finalg]

[ finLmodType _ of _ ] (form_scope) [in mathcomp.algebra.finalg]

[ finRingType of _ ] (form_scope) [in mathcomp.algebra.finalg]

[ finUnitAlgType _ of _ ] (form_scope) [in mathcomp.algebra.finalg]

[ finUnitRingType of _ ] (form_scope) [in mathcomp.algebra.finalg]

[ finGroupType of _ for +%R ] (form_scope) [in mathcomp.algebra.finalg]

[ baseFinGroupType of _ for +%R ] (form_scope) [in mathcomp.algebra.finalg]

[ finZmodType of _ ] (form_scope) [in mathcomp.algebra.finalg]

{ ratio _ } [in mathcomp.algebra.fraction]

_ %:F [in mathcomp.algebra.fraction]

_ %:F [in mathcomp.algebra.fraction]

{ fraction _ } [in mathcomp.algebra.fraction]

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) |