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

## R

rcons [definition, in seq]rcons_cat [lemma, in seq]

rcons_cons [lemma, in seq]

rcons_uniq [lemma, in seq]

rcoset [definition, in groups]

rcosetE [lemma, in groups]

rcosetK [lemma, in groups]

rcosetKV [lemma, in groups]

rcosetM [lemma, in groups]

rcosetP [lemma, in groups]

RcosetReprSpec [constructor, in groups]

rcosets [definition, in groups]

rcosetsP [lemma, in groups]

rcoset1 [lemma, in groups]

rcoset_id [lemma, in groups]

rcoset_inj [lemma, in groups]

rcoset_kercosetP [lemma, in normal]

rcoset_kerP [lemma, in morphisms]

rcoset_mul [lemma, in groups]

rcoset_refl [lemma, in groups]

rcoset_repr [lemma, in groups]

rcoset_repr_spec [inductive, in groups]

rcoset_sym [lemma, in groups]

rcoset_trans [lemma, in groups]

rcoset_transl [lemma, in groups]

rcoset_transr [lemma, in groups]

rcutmx [definition, in matrix]

reducebig [definition, in bigops]

ReduceBig [module, in bigops]

ReduceBigSig [module, in bigops]

ReduceBigSig.bigop [axiom, in bigops]

ReduceBigSig.bigopE [axiom, in bigops]

ReduceBig.bigop [definition, in bigops]

ReduceBig.bigopE [lemma, in bigops]

reduce_big_unlock [definition, in bigops]

reflect [inductive, in ssrbool]

Reflect [section, in ssrbool]

ReflectConnectives [section, in ssrbool]

ReflectConnectives.b1 [variable, in ssrbool]

ReflectConnectives.b2 [variable, in ssrbool]

ReflectConnectives.b3 [variable, in ssrbool]

ReflectConnectives.b4 [variable, in ssrbool]

ReflectConnectives.b5 [variable, in ssrbool]

ReflectCore [section, in ssrbool]

ReflectCore.b [variable, in ssrbool]

ReflectCore.c [variable, in ssrbool]

ReflectCore.Hb [variable, in ssrbool]

ReflectCore.P [variable, in ssrbool]

ReflectCore.Q [variable, in ssrbool]

ReflectF [constructor, in ssrbool]

ReflectNegCore [section, in ssrbool]

ReflectNegCore.b [variable, in ssrbool]

ReflectNegCore.c [variable, in ssrbool]

ReflectNegCore.Hb [variable, in ssrbool]

ReflectNegCore.P [variable, in ssrbool]

ReflectNegCore.Q [variable, in ssrbool]

ReflectProp [section, in morphisms]

ReflectProp.aT [variable, in morphisms]

ReflectProp.Defs [section, in morphisms]

ReflectProp.Defs.A [variable, in morphisms]

ReflectProp.Defs.B [variable, in morphisms]

ReflectProp.Defs.MorphicProps [section, in morphisms]

ReflectProp.Defs.MorphicProps.f [variable, in morphisms]

ReflectProp.f [variable, in morphisms]

ReflectProp.G [variable, in morphisms]

ReflectProp.Main [section, in morphisms]

ReflectProp.Main.G [variable, in morphisms]

ReflectProp.Main.H [variable, in morphisms]

ReflectProp.rT [variable, in morphisms]

ReflectT [constructor, in ssrbool]

Reflect.b [variable, in ssrbool]

Reflect.b' [variable, in ssrbool]

Reflect.c [variable, in ssrbool]

Reflect.P [variable, in ssrbool]

Reflect.Pb [variable, in ssrbool]

Reflect.Pb' [variable, in ssrbool]

Reflect.Q [variable, in ssrbool]

reflexive [definition, in ssrbool]

reindex [lemma, in bigops]

reindex_onto [lemma, in bigops]

rel [definition, in ssrbool]

RelAdjunction [section, in connect]

RelAdjunction [constructor, in connect]

RelAdjunction.a [variable, in connect]

RelAdjunction.e [variable, in connect]

RelAdjunction.e' [variable, in connect]

RelAdjunction.h [variable, in connect]

RelAdjunction.Ha [variable, in connect]

RelAdjunction.He [variable, in connect]

RelAdjunction.He' [variable, in connect]

RelAdjunction.T [variable, in connect]

RelAdjunction.T' [variable, in connect]

RelationProperties [section, in ssrbool]

RelationProperties.R [variable, in ssrbool]

RelationProperties.T [variable, in ssrbool]

relU [definition, in ssrbool]

relU_sym [lemma, in connect]

rel_adjunction [record, in connect]

rel_base [definition, in paths]

rel_functor [projection, in connect]

rel_of_simpl_rel [definition, in ssrbool]

rel_unit [projection, in connect]

repack_group [definition, in groups]

repack_morphism [definition, in morphisms]

repack_pos_nat [definition, in ssrnat]

repack_pred [definition, in ssrbool]

repack_sub [definition, in eqtype]

repr [definition, in groups]

repr_class [lemma, in groups]

repr_coset1 [lemma, in normal]

repr_coset_norm [lemma, in normal]

repr_group [lemma, in groups]

repr_rcosetP [lemma, in groups]

repr_set0 [lemma, in groups]

repr_set1 [lemma, in groups]

reshape [definition, in seq]

reshapeKl [lemma, in seq]

reshapeKr [lemma, in seq]

RestrictedMorphism [section, in morphisms]

RestrictedMorphism.A [variable, in morphisms]

RestrictedMorphism.aT [variable, in morphisms]

RestrictedMorphism.B [variable, in morphisms]

RestrictedMorphism.Props [section, in morphisms]

RestrictedMorphism.Props.f [variable, in morphisms]

RestrictedMorphism.Props.sAB [variable, in morphisms]

RestrictedMorphism.rT [variable, in morphisms]

restrm [definition, in morphisms]

restrmP [lemma, in morphisms]

restrm_morphism [definition, in morphisms]

returnType [definition, in ssreflect]

rev [definition, in seq]

Rev [section, in seq]

revK [lemma, in seq]

RevRingType [abbreviation, in ssralg]

Rev.T [variable, in seq]

rev_cat [lemma, in seq]

rev_cons [lemma, in seq]

rev_rcons [lemma, in seq]

rev_rot [lemma, in seq]

rev_rotr [lemma, in seq]

rev_tuple [definition, in tuple]

rev_tupleP [lemma, in tuple]

rev_uniq [lemma, in seq]

rhs [definition, in finset]

right_arc [lemma, in paths]

right_commutative [definition, in ssrfun]

right_distributive [definition, in ssrfun]

right_id [definition, in ssrfun]

right_inverse [definition, in ssrfun]

right_transitive [definition, in ssrbool]

right_zero [definition, in ssrfun]

Ring [module, in ssralg]

RingMixin [abbreviation, in ssralg]

ringType [abbreviation, in ssralg]

RingType [abbreviation, in ssralg]

root [definition, in connect]

rootP [lemma, in connect]

roots [definition, in poly]

roots [definition, in connect]

roots_root [lemma, in connect]

root_connect [lemma, in connect]

root_factor_theorem [lemma, in poly]

root_root [lemma, in connect]

rot [definition, in seq]

RotCompLemmas [section, in seq]

RotCompLemmas.T [variable, in seq]

rotK [lemma, in seq]

rotr [definition, in seq]

rotrK [lemma, in seq]

RotrLemmas [section, in seq]

RotrLemmas.n0 [variable, in seq]

RotrLemmas.T [variable, in seq]

RotrLemmas.T' [variable, in seq]

rotr1_rcons [lemma, in seq]

rotr_inj [lemma, in seq]

rotr_rotr [lemma, in seq]

rotr_size_cat [lemma, in seq]

rotr_tuple [definition, in tuple]

rotr_tupleP [lemma, in tuple]

rotr_uniq [lemma, in seq]

rotS [lemma, in seq]

RotToArcSpec [constructor, in paths]

RotToSpec [constructor, in seq]

rot0 [lemma, in seq]

rot1_cons [lemma, in seq]

rot_addn [lemma, in seq]

rot_add_mod [lemma, in seq]

rot_inj [lemma, in seq]

rot_oversize [lemma, in seq]

rot_rot [lemma, in seq]

rot_rotr [lemma, in seq]

rot_size [lemma, in seq]

rot_size_cat [lemma, in seq]

rot_to [lemma, in seq]

rot_to_arc [lemma, in paths]

rot_to_arc_spec [inductive, in paths]

rot_to_spec [inductive, in seq]

rot_tuple [definition, in tuple]

rot_tupleP [lemma, in tuple]

rot_uniq [lemma, in seq]

rrefl [lemma, in ssrfun]

rshift [definition, in fintype]

rshift1 [lemma, in matrix]

rshift_subproof [lemma, in fintype]

rswap [definition, in matrix]

rT [abbreviation, in groups]

rT [abbreviation, in groups]

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