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 | _ | (6599 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 | _ | (86 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 | _ | (57 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 | _ | (3455 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 | _ | (290 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 | _ | (147 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 | _ | (148 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 | _ | (53 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 | _ | (1466 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 | _ | (28 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 | _ | (53 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 | _ | (788 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 | _ | (28 entries) |

## C (definition)

cancel [in ssrfun]CanChoiceMixin [in choice]

CanCountMixin [in choice]

CanEqMixin [in eqtype]

CanFinMixin [in fintype]

CardDef.card [in fintype]

CardDef.cardEdef [in fintype]

card_unlock [in fintype]

cast_ord [in fintype]

cat [in seq]

catrev [in seq]

cat_monoid [in bigops]

cat_tuple [in tuple]

centralised [in groups]

centraliser [in groups]

centraliser_group [in groups]

centralises [in groups]

characteristic [in automorphism]

char_poly [in charpoly]

chinese [in div]

Choice.CanMixin2 [in choice]

Choice.class [in choice]

Choice.correct [in choice]

Choice.eqType [in choice]

Choice.extensional [in choice]

Choice.ext0 [in choice]

Choice.natMixin [in choice]

Choice.pack [in choice]

Choice.PcanMixin [in choice]

Choice.pcan_xchoose [in choice]

Choice.repack [in choice]

Choice.unpack [in choice]

Choice.xfun [in choice]

choose [in choice]

class [in groups]

classes [in groups]

class_support [in groups]

closed [in connect]

closure [in connect]

CodeSeq.Nat.code [in choice]

CodeSeq.Nat.decode [in choice]

CodeSeq.Nat.decode_rec [in choice]

CodeSeq.Seq2.code [in choice]

CodeSeq.Seq2.decode [in choice]

CodeSeq.Seq2.pad [in choice]

CodeSeq.Seq2.padding [in choice]

CodeSeq.Seq2.strip [in choice]

codom [in fintype]

cofactor [in matrix]

commg [in groups]

commg_set [in groups]

commutative [in ssrfun]

commutator [in groups]

commutator_group [in groups]

commute [in groups]

comp [in ssrfun]

comparable [in eqtype]

comparableClass [in eqtype]

compareb [in eqtype]

comp_morphism [in morphisms]

com_coef [in poly]

com_poly [in poly]

congr1 [in ssrfun]

congr2 [in ssrfun]

conjg [in groups]

conjgm [in automorphism]

conjgm_morphism [in automorphism]

conjG_group [in groups]

conjugate [in groups]

conjugates [in groups]

conj_aut [in automorphism]

conj_aut_morphism [in automorphism]

connect [in connect]

connect_sym [in connect]

constant [in seq]

cons_pfactor [in prime]

cons_tuple [in tuple]

coprime [in div]

cormen_lup [in matrix]

coset [in normal]

coset_baseGroupType [in normal]

coset_choiceMixin [in normal]

coset_choiceType [in normal]

coset_countMixin [in normal]

coset_countType [in normal]

coset_eqMixin [in normal]

coset_eqType [in normal]

coset_finMixin [in normal]

coset_finType [in normal]

coset_groupType [in normal]

coset_inv [in normal]

coset_morphism [in normal]

coset_mul [in normal]

coset_of_groupMixin [in normal]

coset_one [in normal]

coset_range [in normal]

coset_subCountType [in normal]

coset_subFinType [in normal]

coset_subType [in normal]

count [in seq]

Countable.ChoiceMixin [in choice]

Countable.choiceType [in choice]

Countable.class [in choice]

Countable.EqMixin [in choice]

Countable.eqType [in choice]

Countable.pack [in choice]

Countable.pickle_seq [in choice]

Countable.repack [in choice]

Countable.unpack [in choice]

Countable.unpickle_seq [in choice]

cover [in finset]

cover_at [in finset]

cswap [in matrix]

cycle [in groups]

cycle [in paths]

cyclem [in cyclic]

cyclem_morphism [in cyclic]

cycle_group [in groups]

cyclic [in cyclic]

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 | _ | (6599 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 | _ | (86 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 | _ | (57 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 | _ | (3455 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 | _ | (290 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 | _ | (147 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 | _ | (148 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 | _ | (53 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 | _ | (1466 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 | _ | (28 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 | _ | (53 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 | _ | (788 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 | _ | (28 entries) |