| 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 | +(23233 entries) | +
| Notation 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 | +(1373 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 | +(213 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 | +(3475 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 | +(89 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 | +(11853 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 | +(359 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 | +(47 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 | +(103 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 | +(266 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 | +(1118 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 | +(691 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 | +(3461 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 | +(185 entries) | +
R (lemma)
+rabstrX [in mathcomp.field.closed_field]+ractE [in mathcomp.fingroup.action]
+ractpermE [in mathcomp.fingroup.action]
+ract_is_groupAction [in mathcomp.fingroup.action]
+ract_is_action [in mathcomp.fingroup.action]
+raddfMz [in mathcomp.algebra.ssrint]
+raddfZ_Cint [in mathcomp.field.algC]
+raddfZ_Cnat [in mathcomp.field.algC]
+raddf_int_scalable [in mathcomp.algebra.ssrint]
+ramulXnT [in mathcomp.field.closed_field]
+rankJ [in mathcomp.solvable.abelian]
+rankS [in mathcomp.solvable.abelian]
+rank_Wedderburn_subring [in mathcomp.character.mxrepresentation]
+rank_irr_comp [in mathcomp.character.mxrepresentation]
+rank_irr1 [in mathcomp.character.mxrepresentation]
+rank_DnQ [in mathcomp.solvable.extraspecial]
+rank_Dn [in mathcomp.solvable.extraspecial]
+rank_cycle [in mathcomp.solvable.abelian]
+rank_abelian_pgroup [in mathcomp.solvable.abelian]
+rank_Ohm1 [in mathcomp.solvable.abelian]
+rank_geP [in mathcomp.solvable.abelian]
+rank_abelem [in mathcomp.solvable.abelian]
+rank_Sylow [in mathcomp.solvable.abelian]
+rank_pgroup [in mathcomp.solvable.abelian]
+rank_witness [in mathcomp.solvable.abelian]
+rank_gt0 [in mathcomp.solvable.abelian]
+rank_mx_group [in mathcomp.character.mxabelem]
+rank_copid_mx [in mathcomp.algebra.mxalgebra]
+rank_pid_mx [in mathcomp.algebra.mxalgebra]
+rank_ltmx [in mathcomp.algebra.mxalgebra]
+rank_rV [in mathcomp.algebra.mxalgebra]
+rank_leq_col [in mathcomp.algebra.mxalgebra]
+rank_leq_row [in mathcomp.algebra.mxalgebra]
+rank1 [in mathcomp.solvable.abelian]
+ratCK [in mathcomp.field.algC]
+RatioP [in mathcomp.algebra.fraction]
+Ratio_numden [in mathcomp.algebra.fraction]
+Ratio0 [in mathcomp.algebra.fraction]
+RatK [in mathcomp.algebra.rat]
+ratP [in mathcomp.algebra.rat]
+ratr_norm [in mathcomp.algebra.rat]
+ratr_sg [in mathcomp.algebra.rat]
+ratr_is_rmorphism [in mathcomp.algebra.rat]
+ratr_nat [in mathcomp.algebra.rat]
+ratr_int [in mathcomp.algebra.rat]
+ratzD [in mathcomp.algebra.rat]
+ratzE [in mathcomp.algebra.rat]
+ratzM [in mathcomp.algebra.rat]
+ratzN [in mathcomp.algebra.rat]
+ratz_frac [in mathcomp.algebra.rat]
+rat_field_theory [in mathcomp.algebra.rat]
+rat_ring_theory [in mathcomp.algebra.rat]
+rat_lrmorphism [in mathcomp.algebra.rat]
+rat_linear [in mathcomp.algebra.rat]
+rat_archimedean [in mathcomp.algebra.rat]
+rat_field_axiom [in mathcomp.algebra.rat]
+rat_eq [in mathcomp.algebra.rat]
+rat_eqE [in mathcomp.algebra.rat]
+rat_poly_scale [in mathcomp.algebra.intdiv]
+rat_algebraic_decidable [in mathcomp.field.algebraics_fundamentals]
+rat_algebraic_archimedean [in mathcomp.field.algebraics_fundamentals]
+rat0 [in mathcomp.algebra.rat]
+rat1 [in mathcomp.algebra.rat]
+rcenter_normal [in mathcomp.character.mxrepresentation]
+rcenter_group_set [in mathcomp.character.mxrepresentation]
+rcent_map [in mathcomp.character.mxrepresentation]
+rcent_quo [in mathcomp.character.mxrepresentation]
+rcent_conj [in mathcomp.character.mxrepresentation]
+rcent_eqg [in mathcomp.character.mxrepresentation]
+rcent_subg [in mathcomp.character.mxrepresentation]
+rcent_group_set [in mathcomp.character.mxrepresentation]
+rcent_sub [in mathcomp.character.mxrepresentation]
+rconj_mxJ [in mathcomp.character.mxrepresentation]
+rconj_mxE [in mathcomp.character.mxrepresentation]
+rconj_mx_repr [in mathcomp.character.mxrepresentation]
+rcons_path [in mathcomp.ssreflect.path]
+rcons_tupleP [in mathcomp.ssreflect.tuple]
+rcons_uniq [in mathcomp.ssreflect.seq]
+rcons_cat [in mathcomp.ssreflect.seq]
+rcons_cons [in mathcomp.ssreflect.seq]
+rcosetE [in mathcomp.fingroup.fingroup]
+rcosetK [in mathcomp.fingroup.fingroup]
+rcosetKV [in mathcomp.fingroup.fingroup]
+rcosetM [in mathcomp.fingroup.fingroup]
+rcosetP [in mathcomp.fingroup.fingroup]
+rcosetS [in mathcomp.fingroup.fingroup]
+rcosetsP [in mathcomp.fingroup.fingroup]
+rcosets_cycle_transversal [in mathcomp.solvable.finmodule]
+rcosets_cycle_partition [in mathcomp.solvable.finmodule]
+rcosets_partition [in mathcomp.fingroup.fingroup]
+rcosets_partition_mul [in mathcomp.fingroup.fingroup]
+rcosets_id [in mathcomp.fingroup.fingroup]
+rcoset_kercosetP [in mathcomp.fingroup.quotient]
+rcoset_is_action [in mathcomp.fingroup.action]
+rcoset_kerP [in mathcomp.fingroup.morphism]
+rcoset_index2 [in mathcomp.fingroup.fingroup]
+rcoset_mul [in mathcomp.fingroup.fingroup]
+rcoset_repr [in mathcomp.fingroup.fingroup]
+rcoset_id [in mathcomp.fingroup.fingroup]
+rcoset_trans [in mathcomp.fingroup.fingroup]
+rcoset_transl [in mathcomp.fingroup.fingroup]
+rcoset_eqP [in mathcomp.fingroup.fingroup]
+rcoset_sym [in mathcomp.fingroup.fingroup]
+rcoset_refl [in mathcomp.fingroup.fingroup]
+rcoset_inj [in mathcomp.fingroup.fingroup]
+rcoset1 [in mathcomp.fingroup.fingroup]
+realz [in mathcomp.algebra.ssrint]
+real_lersifN [in mathcomp.algebra.interval]
+redivpTP [in mathcomp.field.closed_field]
+redivpT_qf [in mathcomp.field.closed_field]
+redivp_rec_loopP [in mathcomp.field.closed_field]
+redivp_rec_loopT_qf [in mathcomp.field.closed_field]
+redivp_rec_loopTP [in mathcomp.field.closed_field]
+reducible_Socle1 [in mathcomp.character.mxrepresentation]
+reducible_Socle [in mathcomp.character.mxrepresentation]
+refBaseField_key [in mathcomp.field.fieldext]
+regular_splittingAxiom [in mathcomp.field.galois]
+regular_norm_coprime [in mathcomp.solvable.frobenius]
+regular_norm_dvd_pred [in mathcomp.solvable.frobenius]
+regular_op_inj [in mathcomp.character.mxrepresentation]
+regular_module_ideal [in mathcomp.character.mxrepresentation]
+regular_mx_faithful [in mathcomp.character.mxrepresentation]
+regular_mx_repr [in mathcomp.character.mxrepresentation]
+regular_vect_iso [in mathcomp.algebra.vector]
+regular_fullv [in mathcomp.field.falgebra]
+reindex [in mathcomp.ssreflect.bigop]
+reindex_bigcprod [in mathcomp.fingroup.gproduct]
+reindex_irr_class [in mathcomp.character.character]
+reindex_cfclass [in mathcomp.character.inertia]
+reindex_acts [in mathcomp.fingroup.action]
+reindex_astabs [in mathcomp.fingroup.action]
+reindex_dprod [in mathcomp.character.classfun]
+reindex_inj [in mathcomp.ssreflect.bigop]
+reindex_onto [in mathcomp.ssreflect.bigop]
+relU_sym [in mathcomp.ssreflect.fingraph]
+remgrM [in mathcomp.fingroup.gproduct]
+remgrMid [in mathcomp.fingroup.gproduct]
+remgrMl [in mathcomp.fingroup.gproduct]
+remgrP [in mathcomp.fingroup.gproduct]
+remgr_id [in mathcomp.fingroup.gproduct]
+remgr1 [in mathcomp.fingroup.gproduct]
+rem_filter [in mathcomp.ssreflect.seq]
+rem_uniq [in mathcomp.ssreflect.seq]
+rem_subseq [in mathcomp.ssreflect.seq]
+rem_id [in mathcomp.ssreflect.seq]
+reprGLmM [in mathcomp.character.mxabelem]
+reprK [in mathcomp.ssreflect.generic_quotient]
+repr_coset_norm [in mathcomp.fingroup.quotient]
+repr_coset1 [in mathcomp.fingroup.quotient]
+repr_mx_free [in mathcomp.character.mxrepresentation]
+repr_mxX [in mathcomp.character.mxrepresentation]
+repr_mx_unitr [in mathcomp.character.mxrepresentation]
+repr_mxVr [in mathcomp.character.mxrepresentation]
+repr_mxMr [in mathcomp.character.mxrepresentation]
+repr_mxV [in mathcomp.character.mxrepresentation]
+repr_mx_unit [in mathcomp.character.mxrepresentation]
+repr_mxKV [in mathcomp.character.mxrepresentation]
+repr_mxK [in mathcomp.character.mxrepresentation]
+repr_mxM [in mathcomp.character.mxrepresentation]
+repr_mx1 [in mathcomp.character.mxrepresentation]
+repr_ofK [in mathcomp.ssreflect.generic_quotient]
+repr_irr_classK [in mathcomp.character.character]
+repr_rsim_diag [in mathcomp.character.character]
+repr_classesP [in mathcomp.fingroup.fingroup]
+repr_class [in mathcomp.fingroup.fingroup]
+repr_rcosetP [in mathcomp.fingroup.fingroup]
+repr_group [in mathcomp.fingroup.fingroup]
+repr_set0 [in mathcomp.fingroup.fingroup]
+repr_set1 [in mathcomp.fingroup.fingroup]
+repr_mem_transversal [in mathcomp.ssreflect.finset]
+repr_mem_pblock [in mathcomp.ssreflect.finset]
+reshapeKl [in mathcomp.ssreflect.seq]
+reshapeKr [in mathcomp.ssreflect.seq]
+reshape_leq [in mathcomp.ssreflect.seq]
+reshape_indexK [in mathcomp.ssreflect.seq]
+reshape_offsetP [in mathcomp.ssreflect.seq]
+reshape_indexP [in mathcomp.ssreflect.seq]
+reshape_rcons [in mathcomp.ssreflect.seq]
+resize_mask [in mathcomp.ssreflect.seq]
+restrict_aut_to_normal_num_field [in mathcomp.field.algnum]
+restrict_aut_to_num_field [in mathcomp.field.algnum]
+restrmEsub [in mathcomp.fingroup.morphism]
+restrmP [in mathcomp.fingroup.morphism]
+restrm_quotientE [in mathcomp.fingroup.quotient]
+restr_perm_isom [in mathcomp.fingroup.action]
+restr_perm_Aut [in mathcomp.fingroup.action]
+restr_permE [in mathcomp.fingroup.action]
+restr_perm_on [in mathcomp.fingroup.action]
+restr_isom [in mathcomp.fingroup.morphism]
+restr_isom_to [in mathcomp.fingroup.morphism]
+resultant_eq0 [in mathcomp.algebra.mxpoly]
+resultant_in_ideal [in mathcomp.algebra.mxpoly]
+Res_sdprod_irr [in mathcomp.character.character]
+Res_Iirr0 [in mathcomp.character.character]
+Res_irr_neq0 [in mathcomp.character.character]
+revK [in mathcomp.ssreflect.seq]
+rev_sorted [in mathcomp.ssreflect.path]
+rev_path [in mathcomp.ssreflect.path]
+rev_tupleP [in mathcomp.ssreflect.tuple]
+rev_reshape [in mathcomp.ssreflect.seq]
+rev_flatten [in mathcomp.ssreflect.seq]
+rev_zip [in mathcomp.ssreflect.seq]
+rev_rot [in mathcomp.ssreflect.seq]
+rev_rotr [in mathcomp.ssreflect.seq]
+rev_uniq [in mathcomp.ssreflect.seq]
+rev_rcons [in mathcomp.ssreflect.seq]
+rev_cat [in mathcomp.ssreflect.seq]
+rev_cons [in mathcomp.ssreflect.seq]
+rev_ord_inj [in mathcomp.ssreflect.fintype]
+rev_ordK [in mathcomp.ssreflect.fintype]
+rev_ord_proof [in mathcomp.ssreflect.fintype]
+rfdP [in mathcomp.solvable.alt]
+rfd_iso [in mathcomp.solvable.alt]
+rfd_odd [in mathcomp.solvable.alt]
+rfd_morph [in mathcomp.solvable.alt]
+rfd_funP [in mathcomp.solvable.alt]
+rfix_regular [in mathcomp.character.mxrepresentation]
+rfix_quo [in mathcomp.character.mxrepresentation]
+rfix_conj [in mathcomp.character.mxrepresentation]
+rfix_factmod [in mathcomp.character.mxrepresentation]
+rfix_submod [in mathcomp.character.mxrepresentation]
+rfix_morphim [in mathcomp.character.mxrepresentation]
+rfix_morphpre [in mathcomp.character.mxrepresentation]
+rfix_eqg [in mathcomp.character.mxrepresentation]
+rfix_subg [in mathcomp.character.mxrepresentation]
+rfix_mx_rstabC [in mathcomp.character.mxrepresentation]
+rfix_mx_module [in mathcomp.character.mxrepresentation]
+rfix_mx_conjsg [in mathcomp.character.mxrepresentation]
+rfix_mxS [in mathcomp.character.mxrepresentation]
+rfix_mx_id [in mathcomp.character.mxrepresentation]
+rfix_mxP [in mathcomp.character.mxrepresentation]
+rfix_pgroup_char [in mathcomp.character.mxabelem]
+rfix_abelem [in mathcomp.character.mxabelem]
+rgcdpTP [in mathcomp.field.closed_field]
+rgcdpTsP [in mathcomp.field.closed_field]
+rgcdpTs_qf [in mathcomp.field.closed_field]
+rgcdpT_qf [in mathcomp.field.closed_field]
+rgcdp_loopT_qf [in mathcomp.field.closed_field]
+rgcdp_loopP [in mathcomp.field.closed_field]
+rgdcopTP [in mathcomp.field.closed_field]
+rgdcopT_qf [in mathcomp.field.closed_field]
+rgdcop_recT_qf [in mathcomp.field.closed_field]
+rgdcop_recTP [in mathcomp.field.closed_field]
+rgdP [in mathcomp.solvable.alt]
+rgraphK [in mathcomp.ssreflect.fingraph]
+right_arc [in mathcomp.ssreflect.path]
+right_trans [in mathcomp.ssreflect.generic_quotient]
+ring_quot_mixinP [in mathcomp.algebra.ring_quotient]
+rkerP [in mathcomp.character.mxrepresentation]
+rker_map [in mathcomp.character.mxrepresentation]
+rker_mx_rsim [in mathcomp.character.mxrepresentation]
+rker_factmod [in mathcomp.character.mxrepresentation]
+rker_submod [in mathcomp.character.mxrepresentation]
+rker_quo [in mathcomp.character.mxrepresentation]
+rker_conj [in mathcomp.character.mxrepresentation]
+rker_morphim [in mathcomp.character.mxrepresentation]
+rker_morphpre [in mathcomp.character.mxrepresentation]
+rker_eqg [in mathcomp.character.mxrepresentation]
+rker_subg [in mathcomp.character.mxrepresentation]
+rker_linear [in mathcomp.character.mxrepresentation]
+rker_normal [in mathcomp.character.mxrepresentation]
+rker_norm [in mathcomp.character.mxrepresentation]
+rker_abelem [in mathcomp.character.mxabelem]
+rmorphMz [in mathcomp.algebra.ssrint]
+rmorphXz [in mathcomp.algebra.ssrint]
+rmorphzP [in mathcomp.algebra.ssrint]
+rmorphZ_num [in mathcomp.field.algnum]
+rmorph_unity_root [in mathcomp.algebra.poly]
+rmorph_root [in mathcomp.algebra.poly]
+rmorph_int [in mathcomp.algebra.ssrint]
+rmulpT [in mathcomp.field.closed_field]
+rootC [in mathcomp.algebra.poly]
+rootE [in mathcomp.algebra.poly]
+rootM [in mathcomp.algebra.poly]
+rootN [in mathcomp.algebra.poly]
+rootP [in mathcomp.algebra.poly]
+rootP [in mathcomp.ssreflect.fingraph]
+rootPf [in mathcomp.algebra.poly]
+rootPt [in mathcomp.algebra.poly]
+roots_root [in mathcomp.ssreflect.fingraph]
+rootX [in mathcomp.algebra.poly]
+rootZ [in mathcomp.algebra.poly]
+root_minPoly_gal [in mathcomp.field.galois]
+root_minCpoly [in mathcomp.field.algC]
+root_small_adjoin_poly [in mathcomp.field.fieldext]
+root_minPoly [in mathcomp.field.fieldext]
+root_annihilant [in mathcomp.algebra.polyXY]
+root_cyclotomic [in mathcomp.field.cyclotomic]
+root_monic_Aint [in mathcomp.field.algnum]
+root_exp_XsubC [in mathcomp.algebra.poly]
+root_prod_XsubC [in mathcomp.algebra.poly]
+root_comp [in mathcomp.algebra.poly]
+root_polyC [in mathcomp.algebra.poly]
+root_XaddC [in mathcomp.algebra.poly]
+root_XsubC [in mathcomp.algebra.poly]
+root_size_gt1 [in mathcomp.algebra.poly]
+root_connect [in mathcomp.ssreflect.fingraph]
+root_root [in mathcomp.ssreflect.fingraph]
+root0 [in mathcomp.algebra.poly]
+root1 [in mathcomp.algebra.poly]
+rotations_is_rot [in mathcomp.solvable.burnside_app]
+rotK [in mathcomp.ssreflect.seq]
+rotrK [in mathcomp.ssreflect.seq]
+rotr_ucycle [in mathcomp.ssreflect.path]
+rotr_cycle [in mathcomp.ssreflect.path]
+rotr_tupleP [in mathcomp.ssreflect.tuple]
+rotr_rotr [in mathcomp.ssreflect.seq]
+rotr_inj [in mathcomp.ssreflect.seq]
+rotr_uniq [in mathcomp.ssreflect.seq]
+rotr_size_cat [in mathcomp.ssreflect.seq]
+rotr1_rcons [in mathcomp.ssreflect.seq]
+rotS [in mathcomp.ssreflect.seq]
+rot_to_arc [in mathcomp.ssreflect.path]
+rot_ucycle [in mathcomp.ssreflect.path]
+rot_cycle [in mathcomp.ssreflect.path]
+rot_tupleP [in mathcomp.ssreflect.tuple]
+rot_rotr [in mathcomp.ssreflect.seq]
+rot_rot [in mathcomp.ssreflect.seq]
+rot_add_mod [in mathcomp.ssreflect.seq]
+rot_addn [in mathcomp.ssreflect.seq]
+rot_to [in mathcomp.ssreflect.seq]
+rot_uniq [in mathcomp.ssreflect.seq]
+rot_inj [in mathcomp.ssreflect.seq]
+rot_size_cat [in mathcomp.ssreflect.seq]
+rot_size [in mathcomp.ssreflect.seq]
+rot_oversize [in mathcomp.ssreflect.seq]
+rot_is_rot [in mathcomp.solvable.burnside_app]
+rot_r1 [in mathcomp.solvable.burnside_app]
+rot_eq_c0 [in mathcomp.solvable.burnside_app]
+rot0 [in mathcomp.ssreflect.seq]
+rot1_cons [in mathcomp.ssreflect.seq]
+rowE [in mathcomp.algebra.matrix]
+rowgD [in mathcomp.character.mxabelem]
+rowgI [in mathcomp.character.mxabelem]
+rowgK [in mathcomp.character.mxabelem]
+rowgS [in mathcomp.character.mxabelem]
+rowg_mxSK [in mathcomp.character.mxabelem]
+rowg_mxK [in mathcomp.character.mxabelem]
+rowg_mx_eq0 [in mathcomp.character.mxabelem]
+rowg_mx1 [in mathcomp.character.mxabelem]
+rowg_mxS [in mathcomp.character.mxabelem]
+rowg_stable [in mathcomp.character.mxabelem]
+rowg_group_set [in mathcomp.character.mxabelem]
+rowg0 [in mathcomp.character.mxabelem]
+rowg1 [in mathcomp.character.mxabelem]
+rowK [in mathcomp.algebra.matrix]
+rowKd [in mathcomp.algebra.matrix]
+rowKu [in mathcomp.algebra.matrix]
+rowP [in mathcomp.algebra.matrix]
+rowV0P [in mathcomp.algebra.mxalgebra]
+rowV0Pn [in mathcomp.algebra.mxalgebra]
+row_full_dom_hom [in mathcomp.character.mxrepresentation]
+row_hom_mxP [in mathcomp.character.mxrepresentation]
+row_permE [in mathcomp.algebra.matrix]
+row_mul [in mathcomp.algebra.matrix]
+row_sum_delta [in mathcomp.algebra.matrix]
+row_mx_eq0 [in mathcomp.algebra.matrix]
+row_mx0 [in mathcomp.algebra.matrix]
+row_row_mx [in mathcomp.algebra.matrix]
+row_mxA [in mathcomp.algebra.matrix]
+row_mx_const [in mathcomp.algebra.matrix]
+row_mxKr [in mathcomp.algebra.matrix]
+row_mxEr [in mathcomp.algebra.matrix]
+row_mxKl [in mathcomp.algebra.matrix]
+row_mxEl [in mathcomp.algebra.matrix]
+row_mx_key [in mathcomp.algebra.matrix]
+row_eq [in mathcomp.algebra.matrix]
+row_id [in mathcomp.algebra.matrix]
+row_permM [in mathcomp.algebra.matrix]
+row_perm1 [in mathcomp.algebra.matrix]
+row_const [in mathcomp.algebra.matrix]
+row_matrixP [in mathcomp.algebra.matrix]
+row_perm_const [in mathcomp.algebra.matrix]
+row_perm_key [in mathcomp.algebra.matrix]
+row_full_map [in mathcomp.algebra.mxalgebra]
+row_free_map [in mathcomp.algebra.mxalgebra]
+row_base_free [in mathcomp.algebra.mxalgebra]
+row_full_unit [in mathcomp.algebra.mxalgebra]
+row_free_unit [in mathcomp.algebra.mxalgebra]
+row_free_inj [in mathcomp.algebra.mxalgebra]
+row_freeP [in mathcomp.algebra.mxalgebra]
+row_full_inj [in mathcomp.algebra.mxalgebra]
+row_fullP [in mathcomp.algebra.mxalgebra]
+row_subPn [in mathcomp.algebra.mxalgebra]
+row_subP [in mathcomp.algebra.mxalgebra]
+row_sub [in mathcomp.algebra.mxalgebra]
+row_ebase_unit [in mathcomp.algebra.mxalgebra]
+row_leq_rank [in mathcomp.algebra.mxalgebra]
+row'Kd [in mathcomp.algebra.matrix]
+row'Ku [in mathcomp.algebra.matrix]
+row'_row_mx [in mathcomp.algebra.matrix]
+row'_eq [in mathcomp.algebra.matrix]
+row'_const [in mathcomp.algebra.matrix]
+row0 [in mathcomp.algebra.matrix]
+row1 [in mathcomp.algebra.matrix]
+rpoly_map_mul [in mathcomp.field.closed_field]
+rpredMz [in mathcomp.algebra.ssrint]
+rpredXsign [in mathcomp.algebra.ssrint]
+rpredXz [in mathcomp.algebra.ssrint]
+rpredZint [in mathcomp.algebra.ssrint]
+rpredZ_Cint [in mathcomp.field.algC]
+rpredZ_Cnat [in mathcomp.field.algC]
+rpred_rat [in mathcomp.algebra.rat]
+rpred_Crat [in mathcomp.field.algC]
+rpred_Cnat [in mathcomp.field.algC]
+rpred_Cint [in mathcomp.field.algC]
+rpred_horner [in mathcomp.algebra.poly]
+rpred_int [in mathcomp.algebra.ssrint]
+rreg_div0 [in mathcomp.algebra.poly]
+rreg_polyMC_eq0 [in mathcomp.algebra.poly]
+rreg_size [in mathcomp.algebra.poly]
+rreg_lead0 [in mathcomp.algebra.poly]
+rreg_lead [in mathcomp.algebra.poly]
+rseq_poly_map [in mathcomp.field.closed_field]
+rshift_subproof [in mathcomp.ssreflect.fintype]
+rshift1 [in mathcomp.algebra.zmodp]
+rsim_irr_comp [in mathcomp.character.mxrepresentation]
+rsim_regular_submod [in mathcomp.character.mxrepresentation]
+rsim_regular_series [in mathcomp.character.mxrepresentation]
+rsim_regular_factmod [in mathcomp.character.mxrepresentation]
+rsim_submod1 [in mathcomp.character.mxrepresentation]
+rsim_abelem_subg [in mathcomp.character.mxabelem]
+rstabS [in mathcomp.character.mxrepresentation]
+rstabs_map [in mathcomp.character.mxrepresentation]
+rstabs_quo [in mathcomp.character.mxrepresentation]
+rstabs_conj [in mathcomp.character.mxrepresentation]
+rstabs_factmod [in mathcomp.character.mxrepresentation]
+rstabs_submod [in mathcomp.character.mxrepresentation]
+rstabs_morphim [in mathcomp.character.mxrepresentation]
+rstabs_morphpre [in mathcomp.character.mxrepresentation]
+rstabs_eqg [in mathcomp.character.mxrepresentation]
+rstabs_subg [in mathcomp.character.mxrepresentation]
+rstabs_act [in mathcomp.character.mxrepresentation]
+rstabs_group_set [in mathcomp.character.mxrepresentation]
+rstabs_sub [in mathcomp.character.mxrepresentation]
+rstabs_abelemG [in mathcomp.character.mxabelem]
+rstabs_abelem [in mathcomp.character.mxabelem]
+rstab_map [in mathcomp.character.mxrepresentation]
+rstab_normal [in mathcomp.character.mxrepresentation]
+rstab_norm [in mathcomp.character.mxrepresentation]
+rstab_factmod [in mathcomp.character.mxrepresentation]
+rstab_submod [in mathcomp.character.mxrepresentation]
+rstab_act [in mathcomp.character.mxrepresentation]
+rstab_quo [in mathcomp.character.mxrepresentation]
+rstab_conj [in mathcomp.character.mxrepresentation]
+rstab_morphim [in mathcomp.character.mxrepresentation]
+rstab_morphpre [in mathcomp.character.mxrepresentation]
+rstab_eqg [in mathcomp.character.mxrepresentation]
+rstab_subg [in mathcomp.character.mxrepresentation]
+rstab_group_set [in mathcomp.character.mxrepresentation]
+rstab_sub [in mathcomp.character.mxrepresentation]
+rstab_abelem [in mathcomp.character.mxabelem]
+rsubmx_key [in mathcomp.algebra.matrix]
+rsumpT [in mathcomp.field.closed_field]
+rVabelemD [in mathcomp.character.mxabelem]
+rVabelemJ [in mathcomp.character.mxabelem]
+rVabelemK [in mathcomp.character.mxabelem]
+rVabelemN [in mathcomp.character.mxabelem]
+rVabelemS [in mathcomp.character.mxabelem]
+rVabelemZ [in mathcomp.character.mxabelem]
+rVabelem_minj [in mathcomp.character.mxabelem]
+rVabelem_mK [in mathcomp.character.mxabelem]
+rVabelem_injm [in mathcomp.character.mxabelem]
+rVabelem_inj [in mathcomp.character.mxabelem]
+rVabelem0 [in mathcomp.character.mxabelem]
+rVpolyK [in mathcomp.algebra.mxpoly]
+rVpoly_is_linear [in mathcomp.algebra.mxpoly]
+rVpoly_delta [in mathcomp.algebra.mxpoly]
+rV_abelem_sJ [in mathcomp.character.mxabelem]
+rV_eqP [in mathcomp.algebra.mxalgebra]
+rV_subP [in mathcomp.algebra.mxalgebra]
+R012_inj [in mathcomp.solvable.burnside_app]
+R013_inj [in mathcomp.solvable.burnside_app]
+R021_inj [in mathcomp.solvable.burnside_app]
+R024_inj [in mathcomp.solvable.burnside_app]
+R031_inj [in mathcomp.solvable.burnside_app]
+R034_inj [in mathcomp.solvable.burnside_app]
+R042_inj [in mathcomp.solvable.burnside_app]
+R043_inj [in mathcomp.solvable.burnside_app]
+r05_inv [in mathcomp.solvable.burnside_app]
+R05_inj [in mathcomp.solvable.burnside_app]
+r1_inv [in mathcomp.solvable.burnside_app]
+R1_inj [in mathcomp.solvable.burnside_app]
+r14_inv [in mathcomp.solvable.burnside_app]
+R14_inj [in mathcomp.solvable.burnside_app]
+r2_inv [in mathcomp.solvable.burnside_app]
+R2_inj [in mathcomp.solvable.burnside_app]
+R23_inj [in mathcomp.solvable.burnside_app]
+r3_inv [in mathcomp.solvable.burnside_app]
+R3_inj [in mathcomp.solvable.burnside_app]
+R32_inj [in mathcomp.solvable.burnside_app]
+r41_inv [in mathcomp.solvable.burnside_app]
+R41_inj [in mathcomp.solvable.burnside_app]
+r50_inv [in mathcomp.solvable.burnside_app]
+R50_inj [in mathcomp.solvable.burnside_app]
+
| 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 | +(23233 entries) | +
| Notation 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 | +(1373 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 | +(213 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 | +(3475 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 | +(89 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 | +(11853 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 | +(359 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 | +(47 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 | +(103 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 | +(266 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 | +(1118 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 | +(691 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 | +(3461 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 | +(185 entries) | +