R (Lemmas)
| Files | 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 | _ |
| Definitions | 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 | _ |
| Lemmas | 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 | _ |
| Abbreviations | 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 | _ |
| 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 | _ |
| Notations |
R (Lemmas)
R012_inj [prf, in mathcomp.solvable.burnside_app]R013_inj [prf, in mathcomp.solvable.burnside_app]
R021_inj [prf, in mathcomp.solvable.burnside_app]
R024_inj [prf, in mathcomp.solvable.burnside_app]
R031_inj [prf, in mathcomp.solvable.burnside_app]
R034_inj [prf, in mathcomp.solvable.burnside_app]
R042_inj [prf, in mathcomp.solvable.burnside_app]
R043_inj [prf, in mathcomp.solvable.burnside_app]
R05_inj [prf, in mathcomp.solvable.burnside_app]
r05_inv [prf, in mathcomp.solvable.burnside_app]
R14_inj [prf, in mathcomp.solvable.burnside_app]
r14_inv [prf, in mathcomp.solvable.burnside_app]
R1_inj [prf, in mathcomp.solvable.burnside_app]
r1_inv [prf, in mathcomp.solvable.burnside_app]
R23_inj [prf, in mathcomp.solvable.burnside_app]
R2_inj [prf, in mathcomp.solvable.burnside_app]
r2_inv [prf, in mathcomp.solvable.burnside_app]
R32_inj [prf, in mathcomp.solvable.burnside_app]
R3_inj [prf, in mathcomp.solvable.burnside_app]
r3_inv [prf, in mathcomp.solvable.burnside_app]
R41_inj [prf, in mathcomp.solvable.burnside_app]
r41_inv [prf, in mathcomp.solvable.burnside_app]
R50_inj [prf, in mathcomp.solvable.burnside_app]
r50_inv [prf, in mathcomp.solvable.burnside_app]
ract_is_action [prf, in mathcomp.finite_group.action]
ract_is_groupAction [prf, in mathcomp.finite_group.action]
ractE [prf, in mathcomp.finite_group.action]
ractpermE [prf, in mathcomp.finite_group.action]
rad_ker [prf, in mathcomp.algebra.sesquilinear]
raddf_int_scalable [prf, in mathcomp.algebra.ssrint]
raddfMz [prf, in mathcomp.algebra.ssrint]
radmxE [prf, in mathcomp.algebra.sesquilinear]
rank1 [prf, in mathcomp.solvable.abelian]
rank_abelem [prf, in mathcomp.solvable.abelian]
rank_abelian_pgroup [prf, in mathcomp.solvable.abelian]
rank_col_0mx [prf, in mathcomp.algebra.mxalgebra]
rank_col_mx0 [prf, in mathcomp.algebra.mxalgebra]
rank_copid_mx [prf, in mathcomp.algebra.mxalgebra]
rank_cycle [prf, in mathcomp.solvable.abelian]
rank_diag_block_mx [prf, in mathcomp.algebra.mxalgebra]
rank_Dn [prf, in mathcomp.solvable.extraspecial]
rank_DnQ [prf, in mathcomp.solvable.extraspecial]
rank_geP [prf, in mathcomp.solvable.abelian]
rank_gt0 [prf, in mathcomp.solvable.abelian]
rank_irr1 [prf, in mathcomp.group_representation.mxrepresentation]
rank_irr_comp_pchar [prf, in mathcomp.group_representation.mxrepresentation]
rank_leq_col [prf, in mathcomp.algebra.mxalgebra]
rank_leq_row [prf, in mathcomp.algebra.mxalgebra]
rank_ltmx [prf, in mathcomp.algebra.mxalgebra]
rank_mx_group [prf, in mathcomp.group_representation.mxabelem]
rank_mxdiag [prf, in mathcomp.algebra.mxalgebra]
rank_normal [prf, in mathcomp.algebra.sesquilinear]
rank_Ohm1 [prf, in mathcomp.solvable.abelian]
rank_ortho [prf, in mathcomp.algebra.spectral]
rank_orthomx [prf, in mathcomp.algebra.sesquilinear]
rank_pgroup [prf, in mathcomp.solvable.abelian]
rank_pid_mx [prf, in mathcomp.algebra.mxalgebra]
rank_row_0mx [prf, in mathcomp.algebra.mxalgebra]
rank_row_mx0 [prf, in mathcomp.algebra.mxalgebra]
rank_rV [prf, in mathcomp.algebra.mxalgebra]
rank_Sylow [prf, in mathcomp.solvable.abelian]
rank_Wedderburn_subring_pchar [prf, in mathcomp.group_representation.mxrepresentation]
rank_witness [prf, in mathcomp.solvable.abelian]
rankJ [prf, in mathcomp.solvable.abelian]
rankS [prf, in mathcomp.solvable.abelian]
rat0 [prf, in mathcomp.algebra.rat]
rat1 [prf, in mathcomp.algebra.rat]
rat_algebraic_archimedean [prf, in mathcomp.field.algebraics_fundamentals]
rat_algebraic_decidable [prf, in mathcomp.field.algebraics_fundamentals]
rat_eq [prf, in mathcomp.algebra.rat]
rat_eqE [prf, in mathcomp.algebra.rat]
rat_linear [prf, in mathcomp.algebra.rat]
rat_poly_scale [prf, in mathcomp.algebra.rat]
rat_vm_compute [prf, in mathcomp.algebra.rat]
ratArchimedean.ceilP [prf, in mathcomp.algebra.rat]
ratArchimedean.floorP [prf, in mathcomp.algebra.rat]
ratArchimedean.intrP [prf, in mathcomp.algebra.rat]
ratArchimedean.natrP [prf, in mathcomp.algebra.rat]
ratArchimedean.truncnP [prf, in mathcomp.algebra.rat]
ratCK [prf, in mathcomp.field.algC]
Ratio0 [prf, in mathcomp.algebra.fraction]
Ratio_numden [prf, in mathcomp.algebra.fraction]
RatioP [prf, in mathcomp.algebra.fraction]
RatK [prf, in mathcomp.algebra.rat]
ratP [prf, in mathcomp.algebra.rat]
ratr_int [prf, in mathcomp.algebra.rat]
ratr_is_monoid_morphism [prf, in mathcomp.algebra.rat]
ratr_is_zmod_morphism [prf, in mathcomp.algebra.rat]
ratr_nat [prf, in mathcomp.algebra.rat]
ratr_norm [prf, in mathcomp.algebra.rat]
ratr_sg [prf, in mathcomp.algebra.rat]
ratz_frac [prf, in mathcomp.algebra.rat]
ratzD [prf, in mathcomp.algebra.rat]
ratzE [prf, in mathcomp.algebra.rat]
ratzM [prf, in mathcomp.algebra.rat]
ratzN [prf, in mathcomp.algebra.rat]
rcent_conj [prf, in mathcomp.group_representation.mxrepresentation]
rcent_eqg [prf, in mathcomp.group_representation.mxrepresentation]
rcent_group_set [prf, in mathcomp.group_representation.mxrepresentation]
rcent_map [prf, in mathcomp.group_representation.mxrepresentation]
rcent_quo [prf, in mathcomp.group_representation.mxrepresentation]
rcent_sub [prf, in mathcomp.group_representation.mxrepresentation]
rcent_subg [prf, in mathcomp.group_representation.mxrepresentation]
rcenter_group_set [prf, in mathcomp.group_representation.mxrepresentation]
rcenter_normal [prf, in mathcomp.group_representation.mxrepresentation]
rconj_mx_repr [prf, in mathcomp.group_representation.mxrepresentation]
rconj_mxE [prf, in mathcomp.group_representation.mxrepresentation]
rconj_mxJ [prf, in mathcomp.group_representation.mxrepresentation]
rcons2_infix [prf, in mathcomp.boot.seq]
rcons_bseqP [prf, in mathcomp.boot.tuple]
rcons_cat [prf, in mathcomp.boot.seq]
rcons_cons [prf, in mathcomp.boot.seq]
rcons_inj [prf, in mathcomp.boot.seq]
rcons_injl [prf, in mathcomp.boot.seq]
rcons_injr [prf, in mathcomp.boot.seq]
rcons_path [prf, in mathcomp.boot.path]
rcons_tupleP [prf, in mathcomp.boot.tuple]
rcons_uniq [prf, in mathcomp.boot.seq]
rcoset1 [prf, in mathcomp.finite_group.fingroup]
rcoset_eqP [prf, in mathcomp.finite_group.fingroup]
rcoset_id [prf, in mathcomp.finite_group.fingroup]
rcoset_index2 [prf, in mathcomp.finite_group.fingroup]
rcoset_inj [prf, in mathcomp.finite_group.fingroup]
rcoset_is_action [prf, in mathcomp.finite_group.action]
rcoset_kercosetP [prf, in mathcomp.finite_group.quotient]
rcoset_kerP [prf, in mathcomp.finite_group.morphism]
rcoset_mul [prf, in mathcomp.finite_group.fingroup]
rcoset_refl [prf, in mathcomp.finite_group.fingroup]
rcoset_repr [prf, in mathcomp.finite_group.fingroup]
rcoset_sym [prf, in mathcomp.finite_group.fingroup]
rcoset_trans [prf, in mathcomp.finite_group.fingroup]
rcoset_transl [prf, in mathcomp.finite_group.fingroup]
rcosetE [prf, in mathcomp.finite_group.fingroup]
rcosetK [prf, in mathcomp.finite_group.fingroup]
rcosetKV [prf, in mathcomp.finite_group.fingroup]
rcosetM [prf, in mathcomp.finite_group.fingroup]
rcosetP [prf, in mathcomp.finite_group.fingroup]
rcosetS [prf, in mathcomp.finite_group.fingroup]
rcosets_cycle_partition [prf, in mathcomp.solvable.finmodule]
rcosets_cycle_transversal [prf, in mathcomp.solvable.finmodule]
rcosets_id [prf, in mathcomp.finite_group.fingroup]
rcosets_partition [prf, in mathcomp.finite_group.fingroup]
rcosets_partition_mul [prf, in mathcomp.finite_group.fingroup]
rcosetsP [prf, in mathcomp.finite_group.fingroup]
real_similar [prf, in mathcomp.algebra.spectral]
realmxC [prf, in mathcomp.algebra.spectral]
realmxD [prf, in mathcomp.algebra.spectral]
realsym_hermsym [prf, in mathcomp.algebra.spectral]
realz [prf, in mathcomp.algebra.ssrint]
reducible_Socle [prf, in mathcomp.group_representation.mxrepresentation]
reducible_Socle1 [prf, in mathcomp.group_representation.mxrepresentation]
regular_fullv [prf, in mathcomp.field.falgebra]
regular_module_ideal [prf, in mathcomp.group_representation.mxrepresentation]
regular_mx_faithful [prf, in mathcomp.group_representation.mxrepresentation]
regular_mx_repr [prf, in mathcomp.group_representation.mxrepresentation]
regular_norm_coprime [prf, in mathcomp.solvable.frobenius]
regular_norm_dvd_pred [prf, in mathcomp.solvable.frobenius]
regular_op_inj_pchar [prf, in mathcomp.group_representation.mxrepresentation]
regular_splittingAxiom [prf, in mathcomp.field.galois]
regular_vect_iso [prf, in mathcomp.algebra.vector]
reindex [prf, in mathcomp.boot.bigop]
reindex_acts [prf, in mathcomp.finite_group.action]
reindex_astabs [prf, in mathcomp.finite_group.action]
reindex_bigcprod [prf, in mathcomp.finite_group.gproduct]
reindex_cfclass [prf, in mathcomp.group_representation.inertia]
reindex_dprod [prf, in mathcomp.group_representation.classfun]
reindex_inj [prf, in mathcomp.boot.bigop]
reindex_irr_class [prf, in mathcomp.group_representation.character]
reindex_omap [prf, in mathcomp.boot.bigop]
reindex_onto [prf, in mathcomp.boot.bigop]
relpre_trans [prf, in mathcomp.boot.ssrbool]
relU_sym [prf, in mathcomp.boot.fingraph]
rem_cons [prf, in mathcomp.boot.seq]
rem_filter [prf, in mathcomp.boot.seq]
rem_id [prf, in mathcomp.boot.seq]
rem_mem [prf, in mathcomp.boot.seq]
rem_subseq [prf, in mathcomp.boot.seq]
rem_uniq [prf, in mathcomp.boot.seq]
remE [prf, in mathcomp.boot.seq]
remgr1 [prf, in mathcomp.finite_group.gproduct]
remgr_id [prf, in mathcomp.finite_group.gproduct]
remgrM [prf, in mathcomp.finite_group.gproduct]
remgrMid [prf, in mathcomp.finite_group.gproduct]
remgrMl [prf, in mathcomp.finite_group.gproduct]
remgrP [prf, in mathcomp.finite_group.gproduct]
Remx_rect [prf, in mathcomp.algebra.spectral]
repr_class [prf, in mathcomp.finite_group.fingroup]
repr_classesP [prf, in mathcomp.finite_group.fingroup]
repr_coset1 [prf, in mathcomp.finite_group.quotient]
repr_coset_norm [prf, in mathcomp.finite_group.quotient]
repr_group [prf, in mathcomp.finite_group.fingroup]
repr_irr_classK [prf, in mathcomp.group_representation.character]
repr_mem_pblock [prf, in mathcomp.boot.finset]
repr_mem_transversal [prf, in mathcomp.boot.finset]
repr_mx1 [prf, in mathcomp.group_representation.mxrepresentation]
repr_mx_free [prf, in mathcomp.group_representation.mxrepresentation]
repr_mx_unit [prf, in mathcomp.group_representation.mxrepresentation]
repr_mx_unitr [prf, in mathcomp.group_representation.mxrepresentation]
repr_mxK [prf, in mathcomp.group_representation.mxrepresentation]
repr_mxKV [prf, in mathcomp.group_representation.mxrepresentation]
repr_mxM [prf, in mathcomp.group_representation.mxrepresentation]
repr_mxMr [prf, in mathcomp.group_representation.mxrepresentation]
repr_mxV [prf, in mathcomp.group_representation.mxrepresentation]
repr_mxVr [prf, in mathcomp.group_representation.mxrepresentation]
repr_mxX [prf, in mathcomp.group_representation.mxrepresentation]
repr_ofK [prf, in mathcomp.boot.generic_quotient]
repr_rcosetP [prf, in mathcomp.finite_group.fingroup]
repr_rsim_diag [prf, in mathcomp.group_representation.character]
repr_set0 [prf, in mathcomp.finite_group.fingroup]
repr_set1 [prf, in mathcomp.finite_group.fingroup]
reprGLmM [prf, in mathcomp.group_representation.mxabelem]
reprK [prf, in mathcomp.boot.generic_quotient]
Res_Iirr0 [prf, in mathcomp.group_representation.character]
Res_irr_neq0 [prf, in mathcomp.group_representation.character]
Res_sdprod_irr [prf, in mathcomp.group_representation.character]
reshape_indexK [prf, in mathcomp.boot.seq]
reshape_indexP [prf, in mathcomp.boot.seq]
reshape_leq [prf, in mathcomp.boot.seq]
reshape_offsetP [prf, in mathcomp.boot.seq]
reshape_rcons [prf, in mathcomp.boot.seq]
reshapeKl [prf, in mathcomp.boot.seq]
reshapeKr [prf, in mathcomp.boot.seq]
resize_mask [prf, in mathcomp.boot.seq]
restr_isom [prf, in mathcomp.finite_group.morphism]
restr_isom_to [prf, in mathcomp.finite_group.morphism]
restr_perm_Aut [prf, in mathcomp.finite_group.action]
restr_perm_commute [prf, in mathcomp.finite_group.action]
restr_perm_isom [prf, in mathcomp.finite_group.action]
restr_perm_on [prf, in mathcomp.finite_group.action]
restr_permE [prf, in mathcomp.finite_group.action]
restrict_aut_to_normal_num_field [prf, in mathcomp.field.algnum]
restrict_aut_to_num_field [prf, in mathcomp.field.algnum]
restrm_quotientE [prf, in mathcomp.finite_group.quotient]
restrmEsub [prf, in mathcomp.finite_group.morphism]
restrmP [prf, in mathcomp.finite_group.morphism]
resultant_eq0 [prf, in mathcomp.algebra.mxpoly]
resultant_in_ideal [prf, in mathcomp.algebra.mxpoly]
rev_big_rev [prf, in mathcomp.boot.bigop]
rev_bseqP [prf, in mathcomp.boot.tuple]
rev_cat [prf, in mathcomp.boot.seq]
rev_cons [prf, in mathcomp.boot.seq]
rev_cycle [prf, in mathcomp.boot.path]
rev_drop [prf, in mathcomp.boot.seq]
rev_flatten [prf, in mathcomp.boot.seq]
rev_mask [prf, in mathcomp.boot.seq]
rev_nilp [prf, in mathcomp.boot.seq]
rev_nseq [prf, in mathcomp.boot.seq]
rev_ord_inj [prf, in mathcomp.boot.fintype]
rev_ord_proof [prf, in mathcomp.boot.fintype]
rev_ordK [prf, in mathcomp.boot.fintype]
rev_path [prf, in mathcomp.boot.path]
rev_pivot [prf, in mathcomp.boot.seq]
rev_rcons [prf, in mathcomp.boot.seq]
rev_reshape [prf, in mathcomp.boot.seq]
rev_rot [prf, in mathcomp.boot.seq]
rev_rotr [prf, in mathcomp.boot.seq]
rev_sorted [prf, in mathcomp.boot.path]
rev_take [prf, in mathcomp.boot.seq]
rev_tupleP [prf, in mathcomp.boot.tuple]
rev_uniq [prf, in mathcomp.boot.seq]
rev_zip [prf, in mathcomp.boot.seq]
revK [prf, in mathcomp.boot.seq]
rfd_funP [prf, in mathcomp.solvable.alt]
rfd_iso [prf, in mathcomp.solvable.alt]
rfd_morph [prf, in mathcomp.solvable.alt]
rfd_odd [prf, in mathcomp.solvable.alt]
rfdP [prf, in mathcomp.solvable.alt]
rfix_abelem [prf, in mathcomp.group_representation.mxabelem]
rfix_conj [prf, in mathcomp.group_representation.mxrepresentation]
rfix_eqg [prf, in mathcomp.group_representation.mxrepresentation]
rfix_factmod [prf, in mathcomp.group_representation.mxrepresentation]
rfix_morphim [prf, in mathcomp.group_representation.mxrepresentation]
rfix_morphpre [prf, in mathcomp.group_representation.mxrepresentation]
rfix_mx_conjsg [prf, in mathcomp.group_representation.mxrepresentation]
rfix_mx_id [prf, in mathcomp.group_representation.mxrepresentation]
rfix_mx_module [prf, in mathcomp.group_representation.mxrepresentation]
rfix_mx_rstabC [prf, in mathcomp.group_representation.mxrepresentation]
rfix_mxP [prf, in mathcomp.group_representation.mxrepresentation]
rfix_mxS [prf, in mathcomp.group_representation.mxrepresentation]
rfix_pgroup_pchar [prf, in mathcomp.group_representation.mxabelem]
rfix_quo [prf, in mathcomp.group_representation.mxrepresentation]
rfix_regular [prf, in mathcomp.group_representation.mxrepresentation]
rfix_subg [prf, in mathcomp.group_representation.mxrepresentation]
rfix_submod [prf, in mathcomp.group_representation.mxrepresentation]
rgdP [prf, in mathcomp.solvable.alt]
rgraphK [prf, in mathcomp.boot.fingraph]
right_arc [prf, in mathcomp.boot.path]
right_trans [prf, in mathcomp.boot.generic_quotient]
ring_display [prf, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
ringmx_ind [prf, in mathcomp.algebra.matrix]
rker_abelem [prf, in mathcomp.group_representation.mxabelem]
rker_conj [prf, in mathcomp.group_representation.mxrepresentation]
rker_eqg [prf, in mathcomp.group_representation.mxrepresentation]
rker_factmod [prf, in mathcomp.group_representation.mxrepresentation]
rker_linear [prf, in mathcomp.group_representation.mxrepresentation]
rker_map [prf, in mathcomp.group_representation.mxrepresentation]
rker_morphim [prf, in mathcomp.group_representation.mxrepresentation]
rker_morphpre [prf, in mathcomp.group_representation.mxrepresentation]
rker_mx_rsim [prf, in mathcomp.group_representation.mxrepresentation]
rker_norm [prf, in mathcomp.group_representation.mxrepresentation]
rker_normal [prf, in mathcomp.group_representation.mxrepresentation]
rker_quo [prf, in mathcomp.group_representation.mxrepresentation]
rker_subg [prf, in mathcomp.group_representation.mxrepresentation]
rker_submod [prf, in mathcomp.group_representation.mxrepresentation]
rkerP [prf, in mathcomp.group_representation.mxrepresentation]
rmorph_int [prf, in mathcomp.algebra.ssrint]
rmorph_root [prf, in mathcomp.algebra.poly]
rmorph_unity_root [prf, in mathcomp.algebra.poly]
rmorphK [prf, in mathcomp.algebra.sesquilinear]
rmorphMz [prf, in mathcomp.algebra.ssrint]
rmorphXz [prf, in mathcomp.algebra.ssrint]
rmorphZ_num [prf, in mathcomp.field.algnum]
rmorphzP [prf, in mathcomp.algebra.ssrint]
root0 [prf, in mathcomp.algebra.poly]
root1 [prf, in mathcomp.algebra.poly]
root_annihilant [prf, in mathcomp.algebra.polyXY]
root_comp [prf, in mathcomp.algebra.poly]
root_connect [prf, in mathcomp.boot.fingraph]
root_cyclotomic [prf, in mathcomp.field.cyclotomic]
root_exp [prf, in mathcomp.algebra.poly]
root_exp_XsubC [prf, in mathcomp.algebra.poly]
root_minCpoly [prf, in mathcomp.field.algC]
root_minPoly [prf, in mathcomp.field.fieldext]
root_minPoly_gal [prf, in mathcomp.field.galois]
root_monic_Aint [prf, in mathcomp.field.algnum]
root_mxminpoly [prf, in mathcomp.algebra.mxpoly]
root_polyC [prf, in mathcomp.algebra.poly]
root_prod_XsubC [prf, in mathcomp.algebra.poly]
root_root [prf, in mathcomp.boot.fingraph]
root_size_gt1 [prf, in mathcomp.algebra.poly]
root_small_adjoin_poly [prf, in mathcomp.field.fieldext]
root_XaddC [prf, in mathcomp.algebra.poly]
root_XsubC [prf, in mathcomp.algebra.poly]
root_ZXsubC [prf, in mathcomp.algebra.poly]
rootC [prf, in mathcomp.algebra.poly]
rootE [prf, in mathcomp.algebra.poly]
rootM [prf, in mathcomp.algebra.poly]
rootN [prf, in mathcomp.algebra.poly]
rootP [prf, in mathcomp.boot.fingraph]
rootP [prf, in mathcomp.algebra.poly]
rootPf [prf, in mathcomp.algebra.poly]
rootPt [prf, in mathcomp.algebra.poly]
roots_geq_poly_eq0 [prf, in mathcomp.algebra.poly]
roots_root [prf, in mathcomp.boot.fingraph]
rootX [prf, in mathcomp.algebra.poly]
rootZ [prf, in mathcomp.algebra.poly]
rot0 [prf, in mathcomp.boot.seq]
rot1_cons [prf, in mathcomp.boot.seq]
rot_add_mod [prf, in mathcomp.boot.seq]
rot_addC [prf, in mathcomp.boot.seq]
rot_bseqP [prf, in mathcomp.boot.tuple]
rot_cycle [prf, in mathcomp.boot.path]
rot_eq_c0 [prf, in mathcomp.solvable.burnside_app]
rot_index [prf, in mathcomp.boot.seq]
rot_inj [prf, in mathcomp.boot.seq]
rot_is_rot [prf, in mathcomp.solvable.burnside_app]
rot_minn [prf, in mathcomp.boot.seq]
rot_oversize [prf, in mathcomp.boot.seq]
rot_r1 [prf, in mathcomp.solvable.burnside_app]
rot_rot [prf, in mathcomp.boot.seq]
rot_rot_add [prf, in mathcomp.boot.seq]
rot_rotr [prf, in mathcomp.boot.seq]
rot_size [prf, in mathcomp.boot.seq]
rot_size_cat [prf, in mathcomp.boot.seq]
rot_to [prf, in mathcomp.boot.seq]
rot_to_arc [prf, in mathcomp.boot.path]
rot_tupleP [prf, in mathcomp.boot.tuple]
rot_ucycle [prf, in mathcomp.boot.path]
rot_uniq [prf, in mathcomp.boot.seq]
rotations_is_rot [prf, in mathcomp.solvable.burnside_app]
rotD [prf, in mathcomp.boot.seq]
rotK [prf, in mathcomp.boot.seq]
rotr1_rcons [prf, in mathcomp.boot.seq]
rotr_bseqP [prf, in mathcomp.boot.tuple]
rotr_cycle [prf, in mathcomp.boot.path]
rotr_inj [prf, in mathcomp.boot.seq]
rotr_rotr [prf, in mathcomp.boot.seq]
rotr_size_cat [prf, in mathcomp.boot.seq]
rotr_tupleP [prf, in mathcomp.boot.tuple]
rotr_ucycle [prf, in mathcomp.boot.path]
rotr_uniq [prf, in mathcomp.boot.seq]
rotrK [prf, in mathcomp.boot.seq]
rotS [prf, in mathcomp.boot.seq]
row'_col'_char_poly_mx [prf, in mathcomp.algebra.mxpoly]
row'_const [prf, in mathcomp.algebra.matrix]
row'_eq [prf, in mathcomp.algebra.matrix]
row'_row_mx [prf, in mathcomp.algebra.matrix]
row'Esub [prf, in mathcomp.algebra.matrix]
row'Kd [prf, in mathcomp.algebra.matrix]
row'Ku [prf, in mathcomp.algebra.matrix]
row0 [prf, in mathcomp.algebra.matrix]
row1 [prf, in mathcomp.algebra.matrix]
row_base0 [prf, in mathcomp.algebra.mxalgebra]
row_base_free [prf, in mathcomp.algebra.mxalgebra]
row_const [prf, in mathcomp.algebra.matrix]
row_diag_mx [prf, in mathcomp.algebra.matrix]
row_dsubmx [prf, in mathcomp.algebra.matrix]
row_ebase_unit [prf, in mathcomp.algebra.mxalgebra]
row_eq [prf, in mathcomp.algebra.matrix]
row_free_castmx [prf, in mathcomp.algebra.mxalgebra]
row_free_inj [prf, in mathcomp.algebra.mxalgebra]
row_free_map [prf, in mathcomp.algebra.mxalgebra]
row_free_unit [prf, in mathcomp.algebra.mxalgebra]
row_freeP [prf, in mathcomp.algebra.mxalgebra]
row_freePn [prf, in mathcomp.algebra.mxalgebra]
row_full_castmx [prf, in mathcomp.algebra.mxalgebra]
row_full_dom_hom [prf, in mathcomp.group_representation.mxrepresentation]
row_full_inj [prf, in mathcomp.algebra.mxalgebra]
row_full_map [prf, in mathcomp.algebra.mxalgebra]
row_full_unit [prf, in mathcomp.algebra.mxalgebra]
row_fullP [prf, in mathcomp.algebra.mxalgebra]
row_hom_mxP [prf, in mathcomp.group_representation.mxrepresentation]
row_id [prf, in mathcomp.algebra.matrix]
row_ind [prf, in mathcomp.algebra.matrix]
row_leq_rank [prf, in mathcomp.algebra.mxalgebra]
row_matrixP [prf, in mathcomp.algebra.matrix]
row_mul [prf, in mathcomp.algebra.matrix]
row_mx0 [prf, in mathcomp.algebra.matrix]
row_mx_const [prf, in mathcomp.algebra.matrix]
row_mx_eq0 [prf, in mathcomp.algebra.matrix]
row_mx_key [prf, in mathcomp.algebra.matrix]
row_mxA [prf, in mathcomp.algebra.matrix]
row_mxblock [prf, in mathcomp.algebra.matrix]
row_mxcol [prf, in mathcomp.algebra.matrix]
row_mxdiag [prf, in mathcomp.algebra.matrix]
row_mxEl [prf, in mathcomp.algebra.matrix]
row_mxEr [prf, in mathcomp.algebra.matrix]
row_mxKl [prf, in mathcomp.algebra.matrix]
row_mxKr [prf, in mathcomp.algebra.matrix]
row_mxrow [prf, in mathcomp.algebra.matrix]
row_mxsub [prf, in mathcomp.algebra.matrix]
row_perm1 [prf, in mathcomp.algebra.matrix]
row_perm_const [prf, in mathcomp.algebra.matrix]
row_perm_key [prf, in mathcomp.algebra.matrix]
row_permE [prf, in mathcomp.algebra.matrix]
row_permEsub [prf, in mathcomp.algebra.matrix]
row_permM [prf, in mathcomp.algebra.matrix]
row_row_mx [prf, in mathcomp.algebra.matrix]
row_rowsub [prf, in mathcomp.algebra.matrix]
row_schmidt_sub [prf, in mathcomp.algebra.spectral]
row_sub [prf, in mathcomp.algebra.mxalgebra]
row_subP [prf, in mathcomp.algebra.mxalgebra]
row_subPn [prf, in mathcomp.algebra.mxalgebra]
row_sum_delta [prf, in mathcomp.algebra.matrix]
row_thin_mx [prf, in mathcomp.algebra.matrix]
row_unitarymxP [prf, in mathcomp.algebra.spectral]
row_usubmx [prf, in mathcomp.algebra.matrix]
rowE [prf, in mathcomp.algebra.matrix]
rowEsub [prf, in mathcomp.algebra.matrix]
rowg0 [prf, in mathcomp.group_representation.mxabelem]
rowg1 [prf, in mathcomp.group_representation.mxabelem]
rowg_group_set [prf, in mathcomp.group_representation.mxabelem]
rowg_mx1 [prf, in mathcomp.group_representation.mxabelem]
rowg_mx_eq0 [prf, in mathcomp.group_representation.mxabelem]
rowg_mxK [prf, in mathcomp.group_representation.mxabelem]
rowg_mxS [prf, in mathcomp.group_representation.mxabelem]
rowg_mxSK [prf, in mathcomp.group_representation.mxabelem]
rowg_stable [prf, in mathcomp.group_representation.mxabelem]
rowgD [prf, in mathcomp.group_representation.mxabelem]
rowgI [prf, in mathcomp.group_representation.mxabelem]
rowgK [prf, in mathcomp.group_representation.mxabelem]
rowgS [prf, in mathcomp.group_representation.mxabelem]
rowK [prf, in mathcomp.algebra.matrix]
rowKd [prf, in mathcomp.algebra.matrix]
rowKu [prf, in mathcomp.algebra.matrix]
rowP [prf, in mathcomp.algebra.matrix]
rowsub_cast [prf, in mathcomp.algebra.matrix]
rowsub_comp [prf, in mathcomp.algebra.matrix]
rowsub_comp_sub [prf, in mathcomp.algebra.mxalgebra]
rowsub_sub [prf, in mathcomp.algebra.mxalgebra]
rowsubE [prf, in mathcomp.algebra.matrix]
rowV0P [prf, in mathcomp.algebra.mxalgebra]
rowV0Pn [prf, in mathcomp.algebra.mxalgebra]
rpred_Crat [prf, in mathcomp.field.algC]
rpred_horner [prf, in mathcomp.algebra.poly]
rpred_int [prf, in mathcomp.algebra.ssrint]
rpred_rat [prf, in mathcomp.algebra.rat]
rpredMz [prf, in mathcomp.algebra.ssrint]
rpredXsign [prf, in mathcomp.algebra.ssrint]
rpredXz [prf, in mathcomp.algebra.ssrint]
rpredZint [prf, in mathcomp.algebra.ssrint]
rreg_div0 [prf, in mathcomp.algebra.poly]
rreg_lead [prf, in mathcomp.algebra.poly]
rreg_lead0 [prf, in mathcomp.algebra.poly]
rreg_polyMC_eq0 [prf, in mathcomp.algebra.poly]
rreg_size [prf, in mathcomp.algebra.poly]
rshift1 [prf, in mathcomp.boot.nmodule]
rshift_inj [prf, in mathcomp.boot.fintype]
rsim_abelem_subg [prf, in mathcomp.group_representation.mxabelem]
rsim_irr_comp_pchar [prf, in mathcomp.group_representation.mxrepresentation]
rsim_regular_factmod [prf, in mathcomp.group_representation.mxrepresentation]
rsim_regular_series [prf, in mathcomp.group_representation.mxrepresentation]
rsim_regular_submod_pchar [prf, in mathcomp.group_representation.mxrepresentation]
rsim_submod1 [prf, in mathcomp.group_representation.mxrepresentation]
rstab_abelem [prf, in mathcomp.group_representation.mxabelem]
rstab_act [prf, in mathcomp.group_representation.mxrepresentation]
rstab_conj [prf, in mathcomp.group_representation.mxrepresentation]
rstab_eqg [prf, in mathcomp.group_representation.mxrepresentation]
rstab_factmod [prf, in mathcomp.group_representation.mxrepresentation]
rstab_group_set [prf, in mathcomp.group_representation.mxrepresentation]
rstab_map [prf, in mathcomp.group_representation.mxrepresentation]
rstab_morphim [prf, in mathcomp.group_representation.mxrepresentation]
rstab_morphpre [prf, in mathcomp.group_representation.mxrepresentation]
rstab_norm [prf, in mathcomp.group_representation.mxrepresentation]
rstab_normal [prf, in mathcomp.group_representation.mxrepresentation]
rstab_quo [prf, in mathcomp.group_representation.mxrepresentation]
rstab_sub [prf, in mathcomp.group_representation.mxrepresentation]
rstab_subg [prf, in mathcomp.group_representation.mxrepresentation]
rstab_submod [prf, in mathcomp.group_representation.mxrepresentation]
rstabS [prf, in mathcomp.group_representation.mxrepresentation]
rstabs_abelem [prf, in mathcomp.group_representation.mxabelem]
rstabs_abelemG [prf, in mathcomp.group_representation.mxabelem]
rstabs_act [prf, in mathcomp.group_representation.mxrepresentation]
rstabs_conj [prf, in mathcomp.group_representation.mxrepresentation]
rstabs_eqg [prf, in mathcomp.group_representation.mxrepresentation]
rstabs_factmod [prf, in mathcomp.group_representation.mxrepresentation]
rstabs_group_set [prf, in mathcomp.group_representation.mxrepresentation]
rstabs_map [prf, in mathcomp.group_representation.mxrepresentation]
rstabs_morphim [prf, in mathcomp.group_representation.mxrepresentation]
rstabs_morphpre [prf, in mathcomp.group_representation.mxrepresentation]
rstabs_quo [prf, in mathcomp.group_representation.mxrepresentation]
rstabs_sub [prf, in mathcomp.group_representation.mxrepresentation]
rstabs_subg [prf, in mathcomp.group_representation.mxrepresentation]
rstabs_submod [prf, in mathcomp.group_representation.mxrepresentation]
rsubmx_const [prf, in mathcomp.algebra.matrix]
rsubmx_key [prf, in mathcomp.algebra.matrix]
rsubmxEsub [prf, in mathcomp.algebra.matrix]
rV0Pn [prf, in mathcomp.algebra.matrix]
rV_abelem_sJ [prf, in mathcomp.group_representation.mxabelem]
rV_eqP [prf, in mathcomp.algebra.mxalgebra]
rV_form0_eq0 [prf, in mathcomp.algebra.sesquilinear]
rV_formee [prf, in mathcomp.algebra.sesquilinear]
rV_subP [prf, in mathcomp.algebra.mxalgebra]
rVabelem0 [prf, in mathcomp.group_representation.mxabelem]
rVabelem_inj [prf, in mathcomp.group_representation.mxabelem]
rVabelem_injm [prf, in mathcomp.group_representation.mxabelem]
rVabelem_minj [prf, in mathcomp.group_representation.mxabelem]
rVabelem_mK [prf, in mathcomp.group_representation.mxabelem]
rVabelemD [prf, in mathcomp.group_representation.mxabelem]
rVabelemJ [prf, in mathcomp.group_representation.mxabelem]
rVabelemK [prf, in mathcomp.group_representation.mxabelem]
rVabelemN [prf, in mathcomp.group_representation.mxabelem]
rVabelemS [prf, in mathcomp.group_representation.mxabelem]
rVabelemZ [prf, in mathcomp.group_representation.mxabelem]
rVnpolyK [prf, in mathcomp.algebra.qpoly]
rVpoly_delta [prf, in mathcomp.algebra.mxpoly]
rvPoly_is_linear [prf, in mathcomp.algebra.mxpoly]
rVpoly_is_semilinear [prf, in mathcomp.algebra.mxpoly]
rVpolyK [prf, in mathcomp.algebra.mxpoly]