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

r [definition, in extremal]
r [definition, in extremal]
r [definition, in extremal]
r [abbreviation, in mxabelem]
ract [definition, in action]
ractE [lemma, in action]
raction [definition, in action]
ractpermE [lemma, in action]
ract_is_groupAction [lemma, in action]
ract_groupAction [definition, in action]
ract_is_action [lemma, in action]
range [abbreviation, in action]
rank [definition, in abelian]
rankJ [lemma, in abelian]
rankS [lemma, in abelian]
rank_pid_mx [lemma, in mxalgebra]
rank_leq_row [lemma, in mxalgebra]
rank_irr_comp [lemma, in mxrepresentation]
rank_Dn [lemma, in extraspecial]
rank_DnQ [lemma, in extraspecial]
rank_Ohm1 [lemma, in abelian]
rank_Sylow [lemma, in abelian]
rank_pgroup [lemma, in abelian]
rank_gt0 [lemma, in abelian]
rank_copid_mx [lemma, in mxalgebra]
rank_leq_col [lemma, in mxalgebra]
rank_abelem [lemma, in abelian]
rank_witness [lemma, in abelian]
rank_irr1 [lemma, in mxrepresentation]
rank_cycle [lemma, in abelian]
rank_abelian_pgroup [lemma, in abelian]
rank_geP [lemma, in abelian]
rank_ltmx [lemma, in mxalgebra]
rank_Wedderburn_subring [lemma, in mxrepresentation]
rank_rV [lemma, in mxalgebra]
rank1 [lemma, in abelian]
RawAction [section, in action]
RawAction.ActsSetop [section, in action]
RawAction.ActsSetop.A [variable, in action]
RawAction.ActsSetop.AactS [variable, in action]
RawAction.ActsSetop.AactT [variable, in action]
RawAction.ActsSetop.S [variable, in action]
RawAction.ActsSetop.T [variable, in action]
RawAction.aT [variable, in action]
RawAction.D [variable, in action]
RawAction.Reindex [section, in action]
RawAction.Reindex.idx [variable, in action]
RawAction.Reindex.op [variable, in action]
RawAction.Reindex.S [variable, in action]
RawAction.Reindex.vT [variable, in action]
RawAction.rT [variable, in action]
RawAction.to [variable, in action]
RawGroupAction [section, in action]
RawGroupAction.a [variable, in action]
RawGroupAction.A [variable, in action]
RawGroupAction.aT [variable, in action]
RawGroupAction.B [variable, in action]
RawGroupAction.D [variable, in action]
RawGroupAction.Da [variable, in action]
RawGroupAction.R [variable, in action]
RawGroupAction.rT [variable, in action]
RawGroupAction.S [variable, in action]
RawGroupAction.sAD [variable, in action]
RawGroupAction.sSR [variable, in action]
RawGroupAction.to [variable, in action]
rcent [definition, in mxrepresentation]
rcent_group_set [lemma, in mxrepresentation]
rcent_quo [lemma, in mxrepresentation]
rcent_eqg [lemma, in mxrepresentation]
rcent_group [definition, in mxrepresentation]
rcent_subg [lemma, in mxrepresentation]
rcent_sub [lemma, in mxrepresentation]
rcent_map [lemma, in mxrepresentation]
rcent_conj [lemma, in mxrepresentation]
rconj_mxE [lemma, in mxrepresentation]
rconj_repr [definition, in mxrepresentation]
rconj_mxJ [lemma, in mxrepresentation]
rconj_mx [definition, in mxrepresentation]
rconj_mx_repr [lemma, in mxrepresentation]
rcons [definition, in seq]
rcons_uniq [lemma, in seq]
rcons_cat [lemma, in seq]
rcons_cons [lemma, in seq]
rcoset [definition, in fingroup]
rcosetE [lemma, in fingroup]
rcosetK [lemma, in fingroup]
rcosetKV [lemma, in fingroup]
rcosetM [lemma, in fingroup]
rcosetP [lemma, in fingroup]
RcosetPcycleTransversalWitness [constructor, in finmodule]
RcosetReprSpec [constructor, in fingroup]
rcosets [definition, in fingroup]
rcosetS [lemma, in fingroup]
rcosetsP [lemma, in fingroup]
rcosets_pcycle_transversal [definition, in finmodule]
rcosets_pcycle_transversal_witness [inductive, in finmodule]
rcosets_pcycle_transversal_exists [lemma, in finmodule]
rcoset_kercosetP [lemma, in quotient]
rcoset_repr [lemma, in fingroup]
rcoset_transl [lemma, in fingroup]
rcoset_sym [lemma, in fingroup]
rcoset_id [lemma, in fingroup]
rcoset_inj [lemma, in fingroup]
rcoset_repr_spec [inductive, in fingroup]
rcoset_is_action [lemma, in action]
rcoset_action [definition, in action]
rcoset_refl [lemma, in fingroup]
rcoset_mul [lemma, in fingroup]
rcoset_index2 [lemma, in fingroup]
rcoset_trans [lemma, in fingroup]
rcoset_kerP [lemma, in morphism]
rcoset_transr [lemma, in fingroup]
rcoset1 [lemma, in fingroup]
reducebig [definition, in bigop]
reducible_Socle [lemma, in mxrepresentation]
reducible_Socle1 [lemma, in mxrepresentation]
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 morphism]
ReflectProp.aT [variable, in morphism]
ReflectProp.Defs [section, in morphism]
ReflectProp.Defs.A [variable, in morphism]
ReflectProp.Defs.B [variable, in morphism]
ReflectProp.Defs.MorphicProps [section, in morphism]
ReflectProp.Defs.MorphicProps.f [variable, in morphism]
ReflectProp.f [variable, in morphism]
ReflectProp.G [variable, in morphism]
ReflectProp.Main [section, in morphism]
ReflectProp.Main.G [variable, in morphism]
ReflectProp.Main.H [variable, in morphism]
ReflectProp.rT [variable, in morphism]
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]
regular_mx [definition, in mxrepresentation]
regular_repr [definition, in mxrepresentation]
regular_op_inj [lemma, in mxrepresentation]
regular_norm_coprime [lemma, in frobenius]
regular_mx_repr [lemma, in mxrepresentation]
regular_module_ideal [lemma, in mxrepresentation]
regular_norm_dvd_pred [lemma, in frobenius]
regular_mx_faithful [lemma, in mxrepresentation]
reindex [lemma, in bigop]
reindex_inj [lemma, in bigop]
reindex_astabs [lemma, in action]
reindex_acts [lemma, in action]
reindex_onto [lemma, in bigop]
rel [definition, in ssrbool]
RelAdjunction [section, in fingraph]
RelAdjunction [constructor, in fingraph]
RelAdjunction.a [variable, in fingraph]
RelAdjunction.e [variable, in fingraph]
RelAdjunction.e' [variable, in fingraph]
RelAdjunction.h [variable, in fingraph]
RelAdjunction.Ha [variable, in fingraph]
RelAdjunction.He [variable, in fingraph]
RelAdjunction.He' [variable, in fingraph]
RelAdjunction.T [variable, in fingraph]
RelAdjunction.T' [variable, in fingraph]
RelationProperties [section, in ssrbool]
RelationProperties.R [variable, in ssrbool]
RelationProperties.T [variable, in ssrbool]
relU [definition, in ssrbool]
relU_sym [lemma, in fingraph]
rel_unit [projection, in fingraph]
rel_base [definition, in path]
rel_functor [projection, in fingraph]
rel_of_simpl_rel [definition, in ssrbool]
rel_adjunction [record, in fingraph]
remgr [definition, in gproduct]
remgrM [lemma, in gproduct]
remgrMid [lemma, in gproduct]
remgrMl [lemma, in gproduct]
remgrP [lemma, in gproduct]
remgr_id [lemma, in gproduct]
remgr1 [lemma, in gproduct]
repr [definition, in fingroup]
Repr [section, in fingroup]
reprG [abbreviation, in mxrepresentation]
reprGLm [definition, in mxabelem]
reprGLmM [lemma, in mxabelem]
reprGL_morphism [definition, in mxabelem]
repr_coset1 [lemma, in quotient]
repr_group [lemma, in fingroup]
repr_mxMr [lemma, in mxrepresentation]
repr_class [lemma, in fingroup]
repr_rcosetP [lemma, in fingroup]
repr_set0 [lemma, in fingroup]
repr_coset_norm [lemma, in quotient]
repr_mxV [lemma, in mxrepresentation]
repr_mx [projection, in mxrepresentation]
repr_mxVr [lemma, in mxrepresentation]
repr_set1 [lemma, in fingroup]
repr_mx_unit [lemma, in mxrepresentation]
repr_mxKV [lemma, in mxrepresentation]
repr_mxM [lemma, in mxrepresentation]
repr_mx1 [lemma, in mxrepresentation]
repr_mxK [lemma, in mxrepresentation]
repr_mxX [lemma, in mxrepresentation]
repr_mx_unitr [lemma, in mxrepresentation]
repr_mx_free [lemma, in mxrepresentation]
Repr.gT [variable, in fingroup]
reshape [definition, in seq]
reshapeKl [lemma, in seq]
reshapeKr [lemma, in seq]
Restrict [section, in alt]
Restrict [section, in action]
RestrictActionTheory [section, in action]
RestrictActionTheory.A [variable, in action]
RestrictActionTheory.aT [variable, in action]
RestrictActionTheory.D [variable, in action]
RestrictActionTheory.rT [variable, in action]
RestrictActionTheory.sAD [variable, in action]
RestrictActionTheory.to [variable, in action]
RestrictedMorphism [section, in morphism]
RestrictedMorphism.A [variable, in morphism]
RestrictedMorphism.aT [variable, in morphism]
RestrictedMorphism.D [variable, in morphism]
RestrictedMorphism.Props [section, in morphism]
RestrictedMorphism.Props.f [variable, in morphism]
RestrictedMorphism.Props.sAD [variable, in morphism]
RestrictedMorphism.rT [variable, in morphism]
RestrictPerm [section, in action]
RestrictPerm.S [variable, in action]
RestrictPerm.T [variable, in action]
Restrict.A [variable, in action]
Restrict.aT [variable, in action]
Restrict.card_T [variable, in alt]
Restrict.D [variable, in action]
Restrict.rT [variable, in action]
Restrict.sAD [variable, in action]
Restrict.T [variable, in alt]
Restrict.to [variable, in action]
Restrict.x [variable, in alt]
restrm [definition, in morphism]
restrmP [lemma, in morphism]
restrm_morphism [definition, in morphism]
restr_perm_on [lemma, in action]
restr_perm [definition, in action]
restr_perm_isom [lemma, in action]
restr_perm_morphism [definition, in action]
restr_perm_Aut [lemma, in action]
restr_permE [lemma, in action]
resultant [definition, in mxpoly]
Resultant [section, in mxpoly]
resultant_eq0 [lemma, in mxpoly]
Resultant.F [variable, in mxpoly]
Resultant.p [variable, in mxpoly]
Resultant.q [variable, in mxpoly]
returnType [definition, in ssreflect]
rev [definition, in seq]
Rev [section, in seq]
revK [lemma, in seq]
rev_cons [lemma, in seq]
rev_tuple [definition, in tuple]
rev_tupleP [lemma, in tuple]
rev_ord_inj [lemma, in fintype]
rev_rcons [lemma, in seq]
rev_ordK [lemma, in fintype]
rev_ord_proof [lemma, in fintype]
rev_ord [definition, in fintype]
rev_rotr [lemma, in seq]
rev_trans [lemma, in ssrbool]
rev_uniq [lemma, in seq]
rev_right_loop [definition, in ssrfun]
rev_left_loop [definition, in ssrfun]
rev_rot [lemma, in seq]
rev_cat [lemma, in seq]
Rev.T [variable, in seq]
rF [abbreviation, in mxrepresentation]
rfd [definition, in alt]
rfdP [lemma, in alt]
rfd_morph [lemma, in alt]
rfd_iso [lemma, in alt]
rfd_funP [lemma, in alt]
rfd_odd [lemma, in alt]
rfd_fun [definition, in alt]
rfd_morphism [definition, in alt]
rfix_conj [lemma, in mxrepresentation]
rfix_mx_id [lemma, in mxrepresentation]
rfix_subg [lemma, in mxrepresentation]
rfix_regular [lemma, in mxrepresentation]
rfix_mxS [lemma, in mxrepresentation]
rfix_mx_rstabC [lemma, in mxrepresentation]
rfix_mx_conjsg [lemma, in mxrepresentation]
rfix_submod [lemma, in mxrepresentation]
rfix_factmod [lemma, in mxrepresentation]
rfix_pgroup_char [lemma, in mxabelem]
rfix_mxP [lemma, in mxrepresentation]
rfix_abelem [lemma, in mxabelem]
rfix_morphpre [lemma, in mxrepresentation]
rfix_mx [definition, in mxrepresentation]
rfix_quo [lemma, in mxrepresentation]
rfix_morphim [lemma, in mxrepresentation]
rfix_eqg [lemma, in mxrepresentation]
rfix_mx_module [lemma, in mxrepresentation]
rG [definition, in mxabelem]
rG [abbreviation, in mxrepresentation]
rG [abbreviation, in mxrepresentation]
rGB [abbreviation, in mxrepresentation]
rGB [abbreviation, in mxrepresentation]
rgd [definition, in alt]
rgdP [lemma, in alt]
rgd_fun [definition, in alt]
rGf [abbreviation, in mxrepresentation]
rGf [abbreviation, in mxrepresentation]
rGf [abbreviation, in mxrepresentation]
rGf [abbreviation, in mxrepresentation]
rGH [abbreviation, in mxrepresentation]
rGH [abbreviation, in mxrepresentation]
rH [abbreviation, in mxrepresentation]
rH [abbreviation, in mxrepresentation]
rH [abbreviation, in mxrepresentation]
rH [abbreviation, in mxrepresentation]
rH [definition, in mxrepresentation]
rhs [definition, in finset]
right_arc [lemma, in path]
right_id [definition, in ssrfun]
right_distributive [definition, in ssrfun]
right_loop [definition, in ssrfun]
right_inverse [definition, in ssrfun]
right_zero [definition, in ssrfun]
right_commutative [definition, in ssrfun]
right_transitive [definition, in ssrbool]
right_injective [definition, in ssrfun]
right_mx_ideal [definition, in mxalgebra]
Ring [section, in poly]
Ring [module, in ssralg]
Ring [module, in finalg]
RingRepr [section, in mxrepresentation]
RingRepr.ChangeGroup [section, in mxrepresentation]
RingRepr.ChangeGroup.G [variable, in mxrepresentation]
RingRepr.ChangeGroup.gT [variable, in mxrepresentation]
RingRepr.ChangeGroup.H [variable, in mxrepresentation]
RingRepr.ChangeGroup.n [variable, in mxrepresentation]
RingRepr.ChangeGroup.rG [variable, in mxrepresentation]
RingRepr.ChangeGroup.SameGroup [section, in mxrepresentation]
RingRepr.ChangeGroup.SameGroup.eqGH [variable, in mxrepresentation]
RingRepr.ChangeGroup.SameGroup.Stabiliser [section, in mxrepresentation]
RingRepr.ChangeGroup.SameGroup.Stabiliser.m [variable, in mxrepresentation]
RingRepr.ChangeGroup.SameGroup.Stabiliser.U [variable, in mxrepresentation]
RingRepr.ChangeGroup.SubGroup [section, in mxrepresentation]
RingRepr.ChangeGroup.SubGroup.sHG [variable, in mxrepresentation]
RingRepr.ChangeGroup.SubGroup.Stabiliser [section, in mxrepresentation]
RingRepr.ChangeGroup.SubGroup.Stabiliser.m [variable, in mxrepresentation]
RingRepr.ChangeGroup.SubGroup.Stabiliser.U [variable, in mxrepresentation]
RingRepr.Conjugate [section, in mxrepresentation]
RingRepr.Conjugate.B [variable, in mxrepresentation]
RingRepr.Conjugate.G [variable, in mxrepresentation]
RingRepr.Conjugate.gT [variable, in mxrepresentation]
RingRepr.Conjugate.n [variable, in mxrepresentation]
RingRepr.Conjugate.rG [variable, in mxrepresentation]
RingRepr.Conjugate.uB [variable, in mxrepresentation]
RingRepr.Morphim [section, in mxrepresentation]
RingRepr.Morphim.aT [variable, in mxrepresentation]
RingRepr.Morphim.D [variable, in mxrepresentation]
RingRepr.Morphim.f [variable, in mxrepresentation]
RingRepr.Morphim.G [variable, in mxrepresentation]
RingRepr.Morphim.n [variable, in mxrepresentation]
RingRepr.Morphim.rGf [variable, in mxrepresentation]
RingRepr.Morphim.rT [variable, in mxrepresentation]
RingRepr.Morphim.sGD [variable, in mxrepresentation]
RingRepr.Morphim.Stabiliser [section, in mxrepresentation]
RingRepr.Morphim.Stabiliser.m [variable, in mxrepresentation]
RingRepr.Morphim.Stabiliser.U [variable, in mxrepresentation]
RingRepr.Morphpre [section, in mxrepresentation]
RingRepr.Morphpre.aT [variable, in mxrepresentation]
RingRepr.Morphpre.D [variable, in mxrepresentation]
RingRepr.Morphpre.f [variable, in mxrepresentation]
RingRepr.Morphpre.G [variable, in mxrepresentation]
RingRepr.Morphpre.n [variable, in mxrepresentation]
RingRepr.Morphpre.rG [variable, in mxrepresentation]
RingRepr.Morphpre.rT [variable, in mxrepresentation]
RingRepr.Morphpre.Stabiliser [section, in mxrepresentation]
RingRepr.Morphpre.Stabiliser.m [variable, in mxrepresentation]
RingRepr.Morphpre.Stabiliser.U [variable, in mxrepresentation]
RingRepr.OneRepresentation [section, in mxrepresentation]
RingRepr.OneRepresentation.CentHom [section, in mxrepresentation]
RingRepr.OneRepresentation.CentHom.f [variable, in mxrepresentation]
RingRepr.OneRepresentation.G [variable, in mxrepresentation]
RingRepr.OneRepresentation.gT [variable, in mxrepresentation]
RingRepr.OneRepresentation.n [variable, in mxrepresentation]
RingRepr.OneRepresentation.rG [variable, in mxrepresentation]
RingRepr.OneRepresentation.Stabiliser [section, in mxrepresentation]
RingRepr.OneRepresentation.Stabiliser.m [variable, in mxrepresentation]
RingRepr.OneRepresentation.Stabiliser.U [variable, in mxrepresentation]
RingRepr.Proper [section, in mxrepresentation]
RingRepr.Proper.G [variable, in mxrepresentation]
RingRepr.Proper.gT [variable, in mxrepresentation]
RingRepr.Proper.n' [variable, in mxrepresentation]
RingRepr.Proper.rG [variable, in mxrepresentation]
RingRepr.Quotient [section, in mxrepresentation]
RingRepr.Quotient.G [variable, in mxrepresentation]
RingRepr.Quotient.gT [variable, in mxrepresentation]
RingRepr.Quotient.n [variable, in mxrepresentation]
RingRepr.Quotient.rG [variable, in mxrepresentation]
RingRepr.Quotient.SubQuotient [section, in mxrepresentation]
RingRepr.Quotient.SubQuotient.H [variable, in mxrepresentation]
RingRepr.Quotient.SubQuotient.krH [variable, in mxrepresentation]
RingRepr.Quotient.SubQuotient.nHG [variable, in mxrepresentation]
RingRepr.R [variable, in mxrepresentation]
RingRepr.Regular [section, in mxrepresentation]
RingRepr.Regular.G [variable, in mxrepresentation]
RingRepr.Regular.GringMx [section, in mxrepresentation]
RingRepr.Regular.GringMx.n [variable, in mxrepresentation]
RingRepr.Regular.GringMx.rG [variable, in mxrepresentation]
RingRepr.Regular.GringOp [section, in mxrepresentation]
RingRepr.Regular.GringOp.n [variable, in mxrepresentation]
RingRepr.Regular.GringOp.rG [variable, in mxrepresentation]
RingRepr.Regular.gT [variable, in mxrepresentation]
Ring.R [variable, in poly]
rker [definition, in mxrepresentation]
rkerP [lemma, in mxrepresentation]
rker_quo [lemma, in mxrepresentation]
rker_subg [lemma, in mxrepresentation]
rker_morphim [lemma, in mxrepresentation]
rker_mx_rsim [lemma, in mxrepresentation]
rker_norm [lemma, in mxrepresentation]
rker_linear [lemma, in mxrepresentation]
rker_group [definition, in mxrepresentation]
rker_abelem [lemma, in mxabelem]
rker_factmod [lemma, in mxrepresentation]
rker_normal [lemma, in mxrepresentation]
rker_map [lemma, in mxrepresentation]
rker_eqg [lemma, in mxrepresentation]
rker_conj [lemma, in mxrepresentation]
rker_submod [lemma, in mxrepresentation]
rker_morphpre [lemma, in mxrepresentation]
RMorphism [module, in ssralg]
rmorph_unity_root [lemma, in poly]
root [definition, in fingraph]
root [definition, in poly]
rootP [lemma, in fingraph]
roots [definition, in fingraph]
roots_root [lemma, in fingraph]
root_root [lemma, in fingraph]
root_connect [lemma, in fingraph]
root_factor_theorem [lemma, in poly]
root_field_map_poly [lemma, in poly]
root_of_unity [definition, in poly]
root_map_poly [lemma, in poly]
root_prod_factors [lemma, in poly]
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]
rotr_tuple [definition, in tuple]
rotr_inj [lemma, in seq]
rotr_uniq [lemma, in seq]
rotr_size_cat [lemma, in seq]
rotr_rotr [lemma, in seq]
rotr_tupleP [lemma, in tuple]
rotr1_rcons [lemma, in seq]
rotS [lemma, in seq]
RotToArcSpec [constructor, in path]
RotToSpec [constructor, in seq]
rot_inj [lemma, in seq]
rot_tuple [definition, in tuple]
rot_size [lemma, in seq]
rot_to_spec [inductive, in seq]
rot_to [lemma, in seq]
rot_to_arc_spec [inductive, in path]
rot_size_cat [lemma, in seq]
rot_add_mod [lemma, in seq]
rot_rot [lemma, in seq]
rot_oversize [lemma, in seq]
rot_rotr [lemma, in seq]
rot_uniq [lemma, in seq]
rot_tupleP [lemma, in tuple]
rot_to_arc [lemma, in path]
rot_addn [lemma, in seq]
rot0 [lemma, in seq]
rot1_cons [lemma, in seq]
row [definition, in matrix]
rowE [lemma, in matrix]
rowg [definition, in mxabelem]
rowgD [lemma, in mxabelem]
rowgI [lemma, in mxabelem]
rowgK [lemma, in mxabelem]
rowgS [lemma, in mxabelem]
rowg_mx1 [lemma, in mxabelem]
rowg_mx_eq0 [lemma, in mxabelem]
rowg_mxS [lemma, in mxabelem]
rowg_stable [lemma, in mxabelem]
rowg_group [definition, in mxabelem]
rowg_mx [definition, in mxabelem]
rowg_mxK [lemma, in mxabelem]
rowg_group_set [lemma, in mxabelem]
rowg_mxSK [lemma, in mxabelem]
rowg0 [lemma, in mxabelem]
rowg1 [lemma, in mxabelem]
rowK [lemma, in matrix]
rowKd [lemma, in matrix]
rowKu [lemma, in matrix]
rowP [lemma, in matrix]
RowPoly [section, in mxpoly]
RowPoly.d [variable, in mxpoly]
RowPoly.R [variable, in mxpoly]
RowSpaceTheory [section, in mxalgebra]
RowSpaceTheory.AddsmxSub [section, in mxalgebra]
RowSpaceTheory.AddsmxSub.A [variable, in mxalgebra]
RowSpaceTheory.AddsmxSub.B [variable, in mxalgebra]
RowSpaceTheory.AddsmxSub.m1 [variable, in mxalgebra]
RowSpaceTheory.AddsmxSub.m2 [variable, in mxalgebra]
RowSpaceTheory.AddsmxSub.n [variable, in mxalgebra]
RowSpaceTheory.BinaryDirect [section, in mxalgebra]
RowSpaceTheory.BinaryDirect.m1 [variable, in mxalgebra]
RowSpaceTheory.BinaryDirect.m2 [variable, in mxalgebra]
RowSpaceTheory.BinaryDirect.n [variable, in mxalgebra]
RowSpaceTheory.Defs [section, in mxalgebra]
RowSpaceTheory.Defs.A [variable, in mxalgebra]
RowSpaceTheory.Defs.m [variable, in mxalgebra]
RowSpaceTheory.Defs.n [variable, in mxalgebra]
RowSpaceTheory.Eigenspace [section, in mxalgebra]
RowSpaceTheory.Eigenspace.g [variable, in mxalgebra]
RowSpaceTheory.Eigenspace.n [variable, in mxalgebra]
RowSpaceTheory.F [variable, in mxalgebra]
RowSpaceTheory.I [variable, in mxalgebra]
RowSpaceTheory.LtmxIdentities [section, in mxalgebra]
RowSpaceTheory.LtmxIdentities.A [variable, in mxalgebra]
RowSpaceTheory.LtmxIdentities.B [variable, in mxalgebra]
RowSpaceTheory.LtmxIdentities.m1 [variable, in mxalgebra]
RowSpaceTheory.LtmxIdentities.m2 [variable, in mxalgebra]
RowSpaceTheory.LtmxIdentities.n [variable, in mxalgebra]
RowSpaceTheory.NaryDirect [section, in mxalgebra]
RowSpaceTheory.NaryDirect.n [variable, in mxalgebra]
RowSpaceTheory.NaryDirect.P [variable, in mxalgebra]
RowSpaceTheory.SubDaddsmx [section, in mxalgebra]
RowSpaceTheory.SubDaddsmx.A [variable, in mxalgebra]
RowSpaceTheory.SubDaddsmx.B1 [variable, in mxalgebra]
RowSpaceTheory.SubDaddsmx.B2 [variable, in mxalgebra]
RowSpaceTheory.SubDaddsmx.m [variable, in mxalgebra]
RowSpaceTheory.SubDaddsmx.m1 [variable, in mxalgebra]
RowSpaceTheory.SubDaddsmx.m2 [variable, in mxalgebra]
RowSpaceTheory.SubDaddsmx.n [variable, in mxalgebra]
RowSpaceTheory.SubDsumsmx [section, in mxalgebra]
RowSpaceTheory.SubDsumsmx.A [variable, in mxalgebra]
RowSpaceTheory.SubDsumsmx.B [variable, in mxalgebra]
RowSpaceTheory.SubDsumsmx.m [variable, in mxalgebra]
RowSpaceTheory.SubDsumsmx.n [variable, in mxalgebra]
RowSpaceTheory.SubDsumsmx.P [variable, in mxalgebra]
RowSpaceTheory.SumExpr [section, in mxalgebra]
RowSpaceTheory.SumExpr.Binary [section, in mxalgebra]
RowSpaceTheory.SumExpr.Binary.m1 [variable, in mxalgebra]
RowSpaceTheory.SumExpr.Binary.m2 [variable, in mxalgebra]
RowSpaceTheory.SumExpr.Binary.n [variable, in mxalgebra]
RowSpaceTheory.SumExpr.Binary.S1 [variable, in mxalgebra]
RowSpaceTheory.SumExpr.Binary.S2 [variable, in mxalgebra]
RowSpaceTheory.SumExpr.Nary [section, in mxalgebra]
RowSpaceTheory.SumExpr.Nary.n [variable, in mxalgebra]
RowSpaceTheory.SumExpr.Nary.P [variable, in mxalgebra]
RowSpaceTheory.SumExpr.Nary.S_ [variable, in mxalgebra]
rowV0P [lemma, in mxalgebra]
rowV0Pn [lemma, in mxalgebra]
row_free_unit [lemma, in mxalgebra]
row_free_map [lemma, in mxalgebra]
row_freeP [lemma, in mxalgebra]
row_full_unit [lemma, in mxalgebra]
row_mx0 [lemma, in matrix]
row_perm_const [lemma, in matrix]
row_full_dom_hom [lemma, in mxrepresentation]
row_subPn [lemma, in mxalgebra]
row_permM [lemma, in matrix]
row_perm1 [lemma, in matrix]
row_full_inj [lemma, in mxalgebra]
row_eq [lemma, in matrix]
row_mxEr [lemma, in matrix]
row_sub [lemma, in mxalgebra]
row_mxEl [lemma, in matrix]
row_row_mx [lemma, in matrix]
row_id [lemma, in matrix]
row_mx_const [lemma, in matrix]
row_subP [lemma, in mxalgebra]
row_free [definition, in mxalgebra]
row_hom_mxP [lemma, in mxrepresentation]
row_permE [lemma, in matrix]
row_leq_rank [lemma, in mxalgebra]
row_mxAx [definition, in matrix]
row_ebase_unit [lemma, in mxalgebra]
row_full_map [lemma, in mxalgebra]
row_perm_linear [definition, in matrix]
row_linear [definition, in matrix]
row_perm_additive [definition, in matrix]
row_additive [definition, in matrix]
row_full [definition, in mxalgebra]
row_base_free [lemma, in mxalgebra]
row_perm [definition, in matrix]
row_base [definition, in mxalgebra]
row_hom_mx [definition, in mxrepresentation]
row_mxA [lemma, in matrix]
row_free_inj [lemma, in mxalgebra]
row_mxKr [lemma, in matrix]
row_mxKl [lemma, in matrix]
row_ebase [definition, in mxalgebra]
row_fullP [lemma, in mxalgebra]
row_mul [lemma, in matrix]
row_sum_delta [lemma, in matrix]
row_const [lemma, in matrix]
row_matrixP [lemma, in matrix]
row_mx [definition, in matrix]
row' [definition, in matrix]
row'Kd [lemma, in matrix]
row'Ku [lemma, in matrix]
row'_const [lemma, in matrix]
row'_row_mx [lemma, in matrix]
row'_linear [definition, in matrix]
row'_additive [definition, in matrix]
row'_eq [lemma, in matrix]
row0 [lemma, in matrix]
row1 [lemma, in matrix]
rrefl [lemma, in ssrfun]
rreg [definition, in poly]
rregM [lemma, in poly]
rregP [lemma, in poly]
rregX [lemma, in poly]
rreg_lead [lemma, in poly]
rreg_size [lemma, in poly]
rreg_div0 [lemma, in poly]
rreg_scale0 [lemma, in poly]
rreg_lead0 [lemma, in poly]
rreg_dvdp_mull [lemma, in poly]
rreg0 [lemma, in poly]
rreg1 [lemma, in poly]
rshift [definition, in fintype]
rshift_subproof [lemma, in fintype]
rshift1 [lemma, in zmodp]
rsimC [abbreviation, in mxrepresentation]
rsimT [abbreviation, in mxrepresentation]
rsim_submod1 [lemma, in mxrepresentation]
rsim_irr_comp [lemma, in mxrepresentation]
rsim_last [definition, in mxrepresentation]
rsim_regular_series [lemma, in mxrepresentation]
rsim_regular_submod [lemma, in mxrepresentation]
rsim_regular_factmod [lemma, in mxrepresentation]
rsim_rcons [definition, in mxrepresentation]
rstab [definition, in mxrepresentation]
rstabS [lemma, in mxrepresentation]
rstabs [definition, in mxrepresentation]
rstabs_morphim [lemma, in mxrepresentation]
rstabs_abelem_rowg_mx [lemma, in mxabelem]
rstabs_abelem [lemma, in mxabelem]
rstabs_group [definition, in mxrepresentation]
rstabs_act [lemma, in mxrepresentation]
rstabs_factmod [lemma, in mxrepresentation]
rstabs_map [lemma, in mxrepresentation]
rstabs_group_set [lemma, in mxrepresentation]
rstabs_eqg [lemma, in mxrepresentation]
rstabs_sub [lemma, in mxrepresentation]
rstabs_conj [lemma, in mxrepresentation]
rstabs_morphpre [lemma, in mxrepresentation]
rstabs_quo [lemma, in mxrepresentation]
rstabs_subg [lemma, in mxrepresentation]
rstabs_submod [lemma, in mxrepresentation]
rstab_factmod [lemma, in mxrepresentation]
rstab_morphpre [lemma, in mxrepresentation]
rstab_eqg [lemma, in mxrepresentation]
rstab_sub [lemma, in mxrepresentation]
rstab_morphim [lemma, in mxrepresentation]
rstab_group [definition, in mxrepresentation]
rstab_conj [lemma, in mxrepresentation]
rstab_subg [lemma, in mxrepresentation]
rstab_map [lemma, in mxrepresentation]
rstab_norm [lemma, in mxrepresentation]
rstab_group_set [lemma, in mxrepresentation]
rstab_submod [lemma, in mxrepresentation]
rstab_abelem [lemma, in mxabelem]
rstab_quo [lemma, in mxrepresentation]
rstab_act [lemma, in mxrepresentation]
rstab_normal [lemma, in mxrepresentation]
rsubmx [definition, in matrix]
rsubmx_linear [definition, in matrix]
rsubmx_additive [definition, in matrix]
rT [abbreviation, in fingroup]
rU [abbreviation, in mxrepresentation]
rU' [abbreviation, in mxrepresentation]
rVabelem [definition, in mxabelem]
rVabelemD [lemma, in mxabelem]
rVabelemJ [lemma, in mxabelem]
rVabelemJmx [definition, in mxabelem]
rVabelemK [lemma, in mxabelem]
rVabelemN [lemma, in mxabelem]
rVabelemS [lemma, in mxabelem]
rVabelemZ [lemma, in mxabelem]
rVabelem_injm [lemma, in mxabelem]
rVabelem_inj [lemma, in mxabelem]
rVabelem_mK [lemma, in mxabelem]
rVabelem_morphism [definition, in mxabelem]
rVabelem_minj [lemma, in mxabelem]
rVabelem0 [lemma, in mxabelem]
rVn [abbreviation, in mxabelem]
rVn [abbreviation, in mxabelem]
rVn [abbreviation, in mxabelem]
rVpoly [definition, in mxpoly]
rVpolyK [lemma, in mxpoly]
rVpoly_delta [lemma, in mxpoly]
rVpoly_linear [definition, in mxpoly]
rVpoly_additive [definition, in mxpoly]
rVpoly_is_linear [lemma, in mxpoly]
rV_eqP [lemma, in mxalgebra]
rV_E [abbreviation, in mxabelem]
rV_abelem_sJ [lemma, in mxabelem]
rV_subP [lemma, in mxalgebra]
rv2v [abbreviation, in vector]
rv2v [abbreviation, in vector]
rv2v [abbreviation, in vector]
rv2v [abbreviation, in vector]
rv2vK [lemma, in vector]
rv2v_linear_proof [lemma, in vector]
rv2v_isomorphism [definition, in vector]
rv2v_proof [lemma, in vector]
rv2v_inj [lemma, in vector]
rv2v_iE [lemma, in vector]
rv2v_bij [lemma, in vector]
rv2v_linear [definition, in vector]
rwP [lemma, in ssrbool]
rwP2 [lemma, in ssrbool]
rZ [definition, in mxabelem]
R_ [abbreviation, in mxrepresentation]
R_G [abbreviation, in mxrepresentation]
r_gt0 [definition, in extremal]
r_gt0 [definition, in extremal]
R_G [abbreviation, 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)