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 _ (5434 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 _ (89 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 _ (58 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 _ (2752 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 _ (233 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 _ (145 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 _ (139 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 _ (50 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 _ (1267 entries)
Moduleid 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 _ (47 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 _ (24 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 _ (609 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 _ (21 entries)

R

rabstrX [lemma, in closedfields]
ramulXnT [lemma, in closedfields]
rcons [definition, in seq]
rcons_cat [lemma, in seq]
rcons_cons [lemma, in seq]
rcons_uniq [lemma, in seq]
ReduceBig [moduleid, in bigops]
reducebig [definition, in bigops]
ReduceBigSig [moduleid, 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]
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_inj [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]
reshape [definition, in seq]
reshapeKl [lemma, in seq]
reshapeKr [lemma, in seq]
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_left_loop [definition, in ssrfun]
rev_ord [definition, in fintype]
rev_ordK [lemma, in fintype]
rev_ord_inj [lemma, in fintype]
rev_ord_proof [lemma, in fintype]
rev_rcons [lemma, in seq]
rev_right_loop [definition, in ssrfun]
rev_rot [lemma, in seq]
rev_rotr [lemma, in seq]
rev_trans [lemma, in ssrbool]
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_injective [definition, in ssrfun]
right_inverse [definition, in ssrfun]
right_loop [definition, in ssrfun]
right_transitive [definition, in ssrbool]
right_zero [definition, in ssrfun]
Ring [moduleid, in ssralg]
RingMixin [abbreviation, in ssralg]
ringType [abbreviation, in ssralg]
RingType [abbreviation, in ssralg]
rmulpT [lemma, in closedfields]
root [definition, in connect]
root [definition, in poly]
rootP [lemma, in connect]
roots [definition, in connect]
roots_root [lemma, in connect]
root0 [lemma, in polydiv]
root1n [lemma, in polydiv]
root_biggcd [lemma, in polydiv]
root_bigmul [lemma, in polydiv]
root_connect [lemma, in connect]
root_factor_theorem [lemma, in poly]
root_field_map_poly [lemma, in poly]
root_gcd [lemma, in polydiv]
root_gdco [lemma, in polydiv]
root_map_poly [lemma, in poly]
root_mul [lemma, in polydiv]
root_root [lemma, in connect]
root_size_neq1 [lemma, in polydiv]
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]
rpoly [definition, in closedfields]
rpoly_map_mul [lemma, in closedfields]
rrefl [lemma, in ssrfun]
rseq_poly [definition, in closedfields]
rseq_poly_map [lemma, in closedfields]
rshift [definition, in fintype]
rshift_subproof [lemma, in fintype]
rsumpT [lemma, in closedfields]



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 _ (5434 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 _ (89 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 _ (58 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 _ (2752 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 _ (233 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 _ (145 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 _ (139 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 _ (50 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 _ (1267 entries)
Moduleid 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 _ (47 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 _ (24 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 _ (609 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 _ (21 entries)