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

ractE [in action]
ractpermE [in action]
ract_is_groupAction [in action]
ract_is_action [in action]
rankJ [in abelian]
rankS [in abelian]
rank_pid_mx [in mxalgebra]
rank_leq_row [in mxalgebra]
rank_irr_comp [in mxrepresentation]
rank_Dn [in extraspecial]
rank_DnQ [in extraspecial]
rank_Ohm1 [in abelian]
rank_Sylow [in abelian]
rank_pgroup [in abelian]
rank_gt0 [in abelian]
rank_copid_mx [in mxalgebra]
rank_leq_col [in mxalgebra]
rank_abelem [in abelian]
rank_witness [in abelian]
rank_irr1 [in mxrepresentation]
rank_cycle [in abelian]
rank_abelian_pgroup [in abelian]
rank_geP [in abelian]
rank_ltmx [in mxalgebra]
rank_Wedderburn_subring [in mxrepresentation]
rank_rV [in mxalgebra]
rank1 [in abelian]
rcent_group_set [in mxrepresentation]
rcent_quo [in mxrepresentation]
rcent_eqg [in mxrepresentation]
rcent_subg [in mxrepresentation]
rcent_sub [in mxrepresentation]
rcent_map [in mxrepresentation]
rcent_conj [in mxrepresentation]
rconj_mxE [in mxrepresentation]
rconj_mxJ [in mxrepresentation]
rconj_mx_repr [in mxrepresentation]
rcons_uniq [in seq]
rcons_cat [in seq]
rcons_cons [in seq]
rcosetE [in fingroup]
rcosetK [in fingroup]
rcosetKV [in fingroup]
rcosetM [in fingroup]
rcosetP [in fingroup]
rcosetS [in fingroup]
rcosetsP [in fingroup]
rcosets_pcycle_transversal_exists [in finmodule]
rcoset_kercosetP [in quotient]
rcoset_repr [in fingroup]
rcoset_transl [in fingroup]
rcoset_sym [in fingroup]
rcoset_id [in fingroup]
rcoset_inj [in fingroup]
rcoset_is_action [in action]
rcoset_refl [in fingroup]
rcoset_mul [in fingroup]
rcoset_index2 [in fingroup]
rcoset_trans [in fingroup]
rcoset_kerP [in morphism]
rcoset_transr [in fingroup]
rcoset1 [in fingroup]
reducible_Socle [in mxrepresentation]
reducible_Socle1 [in mxrepresentation]
regular_op_inj [in mxrepresentation]
regular_norm_coprime [in frobenius]
regular_mx_repr [in mxrepresentation]
regular_module_ideal [in mxrepresentation]
regular_norm_dvd_pred [in frobenius]
regular_mx_faithful [in mxrepresentation]
reindex [in bigop]
reindex_inj [in bigop]
reindex_astabs [in action]
reindex_acts [in action]
reindex_onto [in bigop]
relU_sym [in fingraph]
remgrM [in gproduct]
remgrMid [in gproduct]
remgrMl [in gproduct]
remgrP [in gproduct]
remgr_id [in gproduct]
remgr1 [in gproduct]
reprGLmM [in mxabelem]
repr_coset1 [in quotient]
repr_group [in fingroup]
repr_mxMr [in mxrepresentation]
repr_class [in fingroup]
repr_rcosetP [in fingroup]
repr_set0 [in fingroup]
repr_coset_norm [in quotient]
repr_mxV [in mxrepresentation]
repr_mxVr [in mxrepresentation]
repr_set1 [in fingroup]
repr_mx_unit [in mxrepresentation]
repr_mxKV [in mxrepresentation]
repr_mxM [in mxrepresentation]
repr_mx1 [in mxrepresentation]
repr_mxK [in mxrepresentation]
repr_mxX [in mxrepresentation]
repr_mx_unitr [in mxrepresentation]
repr_mx_free [in mxrepresentation]
reshapeKl [in seq]
reshapeKr [in seq]
restrmP [in morphism]
restr_perm_on [in action]
restr_perm_isom [in action]
restr_perm_Aut [in action]
restr_permE [in action]
resultant_eq0 [in mxpoly]
revK [in seq]
rev_cons [in seq]
rev_tupleP [in tuple]
rev_ord_inj [in fintype]
rev_rcons [in seq]
rev_ordK [in fintype]
rev_ord_proof [in fintype]
rev_rotr [in seq]
rev_trans [in ssrbool]
rev_uniq [in seq]
rev_rot [in seq]
rev_cat [in seq]
rfdP [in alt]
rfd_morph [in alt]
rfd_iso [in alt]
rfd_funP [in alt]
rfd_odd [in alt]
rfix_conj [in mxrepresentation]
rfix_mx_id [in mxrepresentation]
rfix_subg [in mxrepresentation]
rfix_regular [in mxrepresentation]
rfix_mxS [in mxrepresentation]
rfix_mx_rstabC [in mxrepresentation]
rfix_mx_conjsg [in mxrepresentation]
rfix_submod [in mxrepresentation]
rfix_factmod [in mxrepresentation]
rfix_pgroup_char [in mxabelem]
rfix_mxP [in mxrepresentation]
rfix_abelem [in mxabelem]
rfix_morphpre [in mxrepresentation]
rfix_quo [in mxrepresentation]
rfix_morphim [in mxrepresentation]
rfix_eqg [in mxrepresentation]
rfix_mx_module [in mxrepresentation]
rgdP [in alt]
right_arc [in path]
rkerP [in mxrepresentation]
rker_quo [in mxrepresentation]
rker_subg [in mxrepresentation]
rker_morphim [in mxrepresentation]
rker_mx_rsim [in mxrepresentation]
rker_norm [in mxrepresentation]
rker_linear [in mxrepresentation]
rker_abelem [in mxabelem]
rker_factmod [in mxrepresentation]
rker_normal [in mxrepresentation]
rker_map [in mxrepresentation]
rker_eqg [in mxrepresentation]
rker_conj [in mxrepresentation]
rker_submod [in mxrepresentation]
rker_morphpre [in mxrepresentation]
rmorph_unity_root [in poly]
rootP [in fingraph]
roots_root [in fingraph]
root_root [in fingraph]
root_connect [in fingraph]
root_factor_theorem [in poly]
root_field_map_poly [in poly]
root_map_poly [in poly]
root_prod_factors [in poly]
rotK [in seq]
rotrK [in seq]
rotr_inj [in seq]
rotr_uniq [in seq]
rotr_size_cat [in seq]
rotr_rotr [in seq]
rotr_tupleP [in tuple]
rotr1_rcons [in seq]
rotS [in seq]
rot_inj [in seq]
rot_size [in seq]
rot_to [in seq]
rot_size_cat [in seq]
rot_add_mod [in seq]
rot_rot [in seq]
rot_oversize [in seq]
rot_rotr [in seq]
rot_uniq [in seq]
rot_tupleP [in tuple]
rot_to_arc [in path]
rot_addn [in seq]
rot0 [in seq]
rot1_cons [in seq]
rowE [in matrix]
rowgD [in mxabelem]
rowgI [in mxabelem]
rowgK [in mxabelem]
rowgS [in mxabelem]
rowg_mx1 [in mxabelem]
rowg_mx_eq0 [in mxabelem]
rowg_mxS [in mxabelem]
rowg_stable [in mxabelem]
rowg_mxK [in mxabelem]
rowg_group_set [in mxabelem]
rowg_mxSK [in mxabelem]
rowg0 [in mxabelem]
rowg1 [in mxabelem]
rowK [in matrix]
rowKd [in matrix]
rowKu [in matrix]
rowP [in matrix]
rowV0P [in mxalgebra]
rowV0Pn [in mxalgebra]
row_free_unit [in mxalgebra]
row_free_map [in mxalgebra]
row_freeP [in mxalgebra]
row_full_unit [in mxalgebra]
row_mx0 [in matrix]
row_perm_const [in matrix]
row_full_dom_hom [in mxrepresentation]
row_subPn [in mxalgebra]
row_permM [in matrix]
row_perm1 [in matrix]
row_full_inj [in mxalgebra]
row_eq [in matrix]
row_mxEr [in matrix]
row_sub [in mxalgebra]
row_mxEl [in matrix]
row_row_mx [in matrix]
row_id [in matrix]
row_mx_const [in matrix]
row_subP [in mxalgebra]
row_hom_mxP [in mxrepresentation]
row_permE [in matrix]
row_leq_rank [in mxalgebra]
row_ebase_unit [in mxalgebra]
row_full_map [in mxalgebra]
row_base_free [in mxalgebra]
row_mxA [in matrix]
row_free_inj [in mxalgebra]
row_mxKr [in matrix]
row_mxKl [in matrix]
row_fullP [in mxalgebra]
row_mul [in matrix]
row_sum_delta [in matrix]
row_const [in matrix]
row_matrixP [in matrix]
row'Kd [in matrix]
row'Ku [in matrix]
row'_const [in matrix]
row'_row_mx [in matrix]
row'_eq [in matrix]
row0 [in matrix]
row1 [in matrix]
rrefl [in ssrfun]
rregM [in poly]
rregP [in poly]
rregX [in poly]
rreg_lead [in poly]
rreg_size [in poly]
rreg_div0 [in poly]
rreg_scale0 [in poly]
rreg_lead0 [in poly]
rreg_dvdp_mull [in poly]
rreg0 [in poly]
rreg1 [in poly]
rshift_subproof [in fintype]
rshift1 [in zmodp]
rsim_submod1 [in mxrepresentation]
rsim_irr_comp [in mxrepresentation]
rsim_regular_series [in mxrepresentation]
rsim_regular_submod [in mxrepresentation]
rsim_regular_factmod [in mxrepresentation]
rstabS [in mxrepresentation]
rstabs_morphim [in mxrepresentation]
rstabs_abelem_rowg_mx [in mxabelem]
rstabs_abelem [in mxabelem]
rstabs_act [in mxrepresentation]
rstabs_factmod [in mxrepresentation]
rstabs_map [in mxrepresentation]
rstabs_group_set [in mxrepresentation]
rstabs_eqg [in mxrepresentation]
rstabs_sub [in mxrepresentation]
rstabs_conj [in mxrepresentation]
rstabs_morphpre [in mxrepresentation]
rstabs_quo [in mxrepresentation]
rstabs_subg [in mxrepresentation]
rstabs_submod [in mxrepresentation]
rstab_factmod [in mxrepresentation]
rstab_morphpre [in mxrepresentation]
rstab_eqg [in mxrepresentation]
rstab_sub [in mxrepresentation]
rstab_morphim [in mxrepresentation]
rstab_conj [in mxrepresentation]
rstab_subg [in mxrepresentation]
rstab_map [in mxrepresentation]
rstab_norm [in mxrepresentation]
rstab_group_set [in mxrepresentation]
rstab_submod [in mxrepresentation]
rstab_abelem [in mxabelem]
rstab_quo [in mxrepresentation]
rstab_act [in mxrepresentation]
rstab_normal [in mxrepresentation]
rVabelemD [in mxabelem]
rVabelemJ [in mxabelem]
rVabelemK [in mxabelem]
rVabelemN [in mxabelem]
rVabelemS [in mxabelem]
rVabelemZ [in mxabelem]
rVabelem_injm [in mxabelem]
rVabelem_inj [in mxabelem]
rVabelem_mK [in mxabelem]
rVabelem_minj [in mxabelem]
rVabelem0 [in mxabelem]
rVpolyK [in mxpoly]
rVpoly_delta [in mxpoly]
rVpoly_is_linear [in mxpoly]
rV_eqP [in mxalgebra]
rV_abelem_sJ [in mxabelem]
rV_subP [in mxalgebra]
rv2vK [in vector]
rv2v_linear_proof [in vector]
rv2v_proof [in vector]
rv2v_inj [in vector]
rv2v_iE [in vector]
rv2v_bij [in vector]
rwP [in ssrbool]
rwP2 [in ssrbool]



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)