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)