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

## R (definition)

r [in extremal]r [in extremal]

r [in extremal]

ract [in action]

raction [in action]

ract_groupAction [in action]

rank [in abelian]

rcent [in mxrepresentation]

rcent_group [in mxrepresentation]

rconj_repr [in mxrepresentation]

rconj_mx [in mxrepresentation]

rcons [in seq]

rcoset [in fingroup]

rcosets [in fingroup]

rcosets_pcycle_transversal [in finmodule]

rcoset_action [in action]

reducebig [in bigop]

reflexive [in ssrbool]

regular_mx [in mxrepresentation]

regular_repr [in mxrepresentation]

rel [in ssrbool]

relU [in ssrbool]

rel_base [in path]

rel_of_simpl_rel [in ssrbool]

remgr [in gproduct]

repr [in fingroup]

reprGLm [in mxabelem]

reprGL_morphism [in mxabelem]

reshape [in seq]

restrm [in morphism]

restrm_morphism [in morphism]

restr_perm [in action]

restr_perm_morphism [in action]

resultant [in mxpoly]

returnType [in ssreflect]

rev [in seq]

rev_tuple [in tuple]

rev_ord [in fintype]

rev_right_loop [in ssrfun]

rev_left_loop [in ssrfun]

rfd [in alt]

rfd_fun [in alt]

rfd_morphism [in alt]

rfix_mx [in mxrepresentation]

rG [in mxabelem]

rgd [in alt]

rgd_fun [in alt]

rH [in mxrepresentation]

rhs [in finset]

right_id [in ssrfun]

right_distributive [in ssrfun]

right_loop [in ssrfun]

right_inverse [in ssrfun]

right_zero [in ssrfun]

right_commutative [in ssrfun]

right_transitive [in ssrbool]

right_injective [in ssrfun]

right_mx_ideal [in mxalgebra]

rker [in mxrepresentation]

rker_group [in mxrepresentation]

root [in fingraph]

root [in poly]

roots [in fingraph]

root_of_unity [in poly]

rot [in seq]

rotr [in seq]

rotr_tuple [in tuple]

rot_tuple [in tuple]

row [in matrix]

rowg [in mxabelem]

rowg_group [in mxabelem]

rowg_mx [in mxabelem]

row_free [in mxalgebra]

row_mxAx [in matrix]

row_perm_linear [in matrix]

row_linear [in matrix]

row_perm_additive [in matrix]

row_additive [in matrix]

row_full [in mxalgebra]

row_perm [in matrix]

row_base [in mxalgebra]

row_hom_mx [in mxrepresentation]

row_ebase [in mxalgebra]

row_mx [in matrix]

row' [in matrix]

row'_linear [in matrix]

row'_additive [in matrix]

rreg [in poly]

rshift [in fintype]

rsim_last [in mxrepresentation]

rsim_rcons [in mxrepresentation]

rstab [in mxrepresentation]

rstabs [in mxrepresentation]

rstabs_group [in mxrepresentation]

rstab_group [in mxrepresentation]

rsubmx [in matrix]

rsubmx_linear [in matrix]

rsubmx_additive [in matrix]

rVabelem [in mxabelem]

rVabelemJmx [in mxabelem]

rVabelem_morphism [in mxabelem]

rVpoly [in mxpoly]

rVpoly_linear [in mxpoly]

rVpoly_additive [in mxpoly]

rv2v_isomorphism [in vector]

rv2v_linear [in vector]

rZ [in mxabelem]

r_gt0 [in extremal]

r_gt0 [in extremal]

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