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

## C (definition)

cAA [in maximal]cancel [in ssrfun]

CanChoiceMixin [in choice]

CanCountMixin [in choice]

CanEqMixin [in eqtype]

CanFinMixin [in fintype]

capmx [in mxalgebra]

capmx_witnessP [in mxalgebra]

capmx_nopP [in mxalgebra]

capmx_def [in mxalgebra]

capmx_nop [in mxalgebra]

capmx_normP [in mxalgebra]

capmx_norm_eq [in mxalgebra]

capmx_witness [in mxalgebra]

capmx_norm [in mxalgebra]

capmx_gen [in mxalgebra]

capmx_eq_norm [in mxalgebra]

capmx_nop_id [in mxalgebra]

capmx_comoid [in mxalgebra]

capmx_monoid [in mxalgebra]

capv [in vector]

capv_comoid [in vector]

capv_monoid [in vector]

CardDef.card [in fintype]

CardDef.cardEdef [in fintype]

cardG_gt0_reduced [in fingroup]

card_unlock [in fintype]

castmx [in matrix]

cast_ord [in fintype]

cat [in seq]

catrev [in seq]

cat_tuple [in tuple]

cat_monoid [in bigop]

Cayley_repr [in action]

center [in center]

center_mx [in mxalgebra]

center_pgFun [in center]

center_gFun [in center]

center_igFun [in center]

center_group [in center]

centgmx [in mxrepresentation]

centralised [in fingroup]

centraliser [in fingroup]

centraliser_group [in fingroup]

centralises [in fingroup]

central_product [in gproduct]

central_factor [in gseries]

cent_mx_fun [in mxalgebra]

cent_mx [in mxalgebra]

cent_mx_fun_linear [in mxalgebra]

cent_mx_fun_additive [in mxalgebra]

characteristic [in automorphism]

charsimple [in maximal]

char_poly [in mxpoly]

char_poly_mx [in mxpoly]

chief_factor [in gseries]

chinese [in div]

Choice.CanMixin2 [in choice]

Choice.class [in choice]

Choice.clone [in choice]

Choice.correct [in choice]

Choice.eqType [in choice]

Choice.extensional [in choice]

Choice.mixin0 [in choice]

Choice.natMixin [in choice]

Choice.pack [in choice]

Choice.PcanMixin [in choice]

Choice.pcan_xchoose [in choice]

Choice.xfun [in choice]

choose [in choice]

class [in fingroup]

classes [in fingroup]

classg_base [in mxrepresentation]

classically [in ssrbool]

class_support [in fingroup]

Clifford_action [in mxrepresentation]

Clifford_act [in mxrepresentation]

clone_pred [in ssrbool]

clone_subType [in eqtype]

clone_action [in action]

clone_morphism [in morphism]

clone_group [in fingroup]

clone_groupAction [in action]

closed [in fingraph]

closure [in fingraph]

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]

coGA' [in hall]

cokermx [in mxalgebra]

col [in matrix]

col_base [in mxalgebra]

col_ebase [in mxalgebra]

col_perm [in matrix]

col_mxAx [in matrix]

col_perm_linear [in matrix]

col_linear [in matrix]

col_perm_additive [in matrix]

col_additive [in matrix]

col_mx [in matrix]

col' [in matrix]

col'_linear [in matrix]

col'_additive [in matrix]

commg [in fingroup]

commg_set [in fingroup]

commr_rmorph [in poly]

commutative [in ssrfun]

commutator [in fingroup]

commutator_group [in fingroup]

commute [in fingroup]

comparable [in eqtype]

comparableClass [in eqtype]

compareb [in eqtype]

complements_to_in [in gproduct]

complmx [in mxalgebra]

complv [in vector]

component_mx [in mxrepresentation]

comps [in jordanholder]

comp_act [in action]

comp_morphism [in morphism]

comp_lapp [in vector]

comp_groupAction [in action]

comp_action [in action]

com_poly [in poly]

com_coef [in poly]

conform_mx [in matrix]

congr1 [in ssrfun]

congr2 [in ssrfun]

conjg [in fingroup]

conjgm [in automorphism]

conjgm_morphism [in automorphism]

conjG_group [in fingroup]

conjG_action [in action]

conjg_groupAction [in action]

conjg_action [in action]

conjsg_action [in action]

conjugate [in fingroup]

conjugates [in fingroup]

conj_aut_morphism [in automorphism]

conj_aut [in automorphism]

connect [in fingraph]

connect_sym [in fingraph]

constant [in seq]

constt [in pgroup]

const_mx [in matrix]

const_mx_additive [in matrix]

cons_tuple [in tuple]

cons_pfactor [in prime]

contraNN [in ssrbool]

contraNT [in ssrbool]

contraTN [in ssrbool]

contraTT [in ssrbool]

coord [in vector]

coord_linear [in vector]

copid_mx [in matrix]

coprime [in div]

cormen_lup [in matrix]

coset [in quotient]

coset_inv [in quotient]

coset_eqMixin [in quotient]

coset_one [in quotient]

coset_morphism [in quotient]

coset_groupType [in quotient]

coset_baseGroupType [in quotient]

coset_subFinType [in quotient]

coset_finType [in quotient]

coset_subCountType [in quotient]

coset_countType [in quotient]

coset_choiceType [in quotient]

coset_eqType [in quotient]

coset_subType [in quotient]

coset_countMixin [in quotient]

coset_mul [in quotient]

coset_transversal [in finmodule]

coset_of_groupMixin [in quotient]

coset_finMixin [in quotient]

coset_choiceMixin [in quotient]

coset_range [in quotient]

count [in seq]

Countable.ChoiceMixin [in choice]

Countable.choiceType [in choice]

Countable.class [in choice]

Countable.clone [in choice]

Countable.EqMixin [in choice]

Countable.eqType [in choice]

Countable.pack [in choice]

Countable.pickle_seq [in choice]

Countable.unpickle_seq [in choice]

cover [in finset]

cover_at [in finset]

cpairg1 [in center]

cpair1g [in center]

cprodm [in gproduct]

cprodm_morphism [in gproduct]

cprod_abelaw [in gproduct]

cprod_law [in gproduct]

cprod_by [in center]

critical [in maximal]

cycle [in path]

cycle [in fingroup]

cyclem [in cyclic]

cyclem_morphism [in cyclic]

cycle_group [in fingroup]

cyclic [in cyclic]

cyclic_mx [in mxrepresentation]

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