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 | (14626 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 | (165 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 | (112 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 | (7292 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 | (761 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 | (250 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 | (390 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 | (84 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 | (3144 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 | (126 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 | (28 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 | (2221 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 | (53 entries) |

## F (abbreviation)

f [in gproduct]f [in automorphism]

fA [in morphism]

fcard [in fingraph]

fclosed [in fingraph]

fclosure [in fingraph]

fconnect [in fingraph]

fcycle [in path]

fE [in automorphism]

ff [in morphism]

ffT [in finfun]

fGisom [in action]

fH [in quotient]

fHisom [in action]

fH_G [in quotient]

finfun [in finfun]

finfun_def [in finfun]

FinGroup.class [in fingroup]

FinGroup.Exports.baseFinGroupType [in fingroup]

FinGroup.Exports.BaseFinGroupType [in fingroup]

FinGroup.Exports.FinGroupType [in fingroup]

FinGroup.Exports.finGroupType [in fingroup]

FinGroup.rT [in fingroup]

FinGroup.T [in fingroup]

FiniteModule.fmodA [in finmodule]

FiniteModule.valA [in finmodule]

Finite.enum [in fintype]

Finite.Exports.FinMixin [in fintype]

Finite.Exports.FinType [in fintype]

Finite.Exports.finType [in fintype]

Finite.Exports.UniqFinMixin [in fintype]

FinRing.Algebra.Exports.finAlgType [in finalg]

FinRing.base_group [in finalg]

FinRing.ComRing.Exports.finComRingType [in finalg]

FinRing.ComUnitRing.Exports.finComUnitRingType [in finalg]

FinRing.do_pack [in finalg]

FinRing.Field.Exports.finFieldType [in finalg]

FinRing.fin_ [in finalg]

FinRing.fin_group [in finalg]

FinRing.IntegralDomain.Exports.finIdomainType [in finalg]

FinRing.Lalgebra.Exports.finLalgType [in finalg]

FinRing.Lmodule.Exports.finLmodType [in finalg]

FinRing.mixin_of [in finalg]

FinRing.Ring.Exports.finRingType [in finalg]

FinRing.UnitAlgebra.Exports.finUnitAlgType [in finalg]

FinRing.UnitRing.Exports.finUnitRingType [in finalg]

FinRing.uT [in finalg]

FinRing.Zmodule.Exports.finZmodType [in finalg]

finset [in finset]

finset_def [in finset]

fmod [in finmodule]

fMT [in morphism]

fp [in mxpoly]

fp [in mxpoly]

fp [in mxpoly]

fpath [in path]

Frobenius_aut [in ssralg]

froot [in fingraph]

froots [in fingraph]

fsH [in gproduct]

fsK [in gproduct]

fT [in finfun]

fT [in finfun]

fT [in finfun]

fun_of_fin_def [in finfun]

fun_of_perm [in perm]

fun_of_fin [in finfun]

fun_of_perm_def [in perm]

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 | (14626 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 | (165 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 | (112 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 | (7292 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 | (761 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 | (250 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 | (390 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 | (84 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 | (3144 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 | (126 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 | (28 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 | (2221 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 | (53 entries) |