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]
R_complete [prf, in mathcomp.analysis.normedtype_theory.complete_normed_module]
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]
radius0 [prf, in mathcomp.analysis.normedtype_theory.vitali_lemma]
radius_ball [prf, in mathcomp.analysis.normedtype_theory.vitali_lemma]
radius_ball_num [prf, in mathcomp.analysis.normedtype_theory.vitali_lemma]
radius_scale_ball [prf, in mathcomp.analysis.normedtype_theory.vitali_lemma]
radmxE [prf, in mathcomp.algebra.sesquilinear]
Radon_Nikodym0 [prf, in mathcomp.analysis.charge]
Radon_Nikodym_cadd [prf, in mathcomp.analysis.charge]
Radon_Nikodym_chain_rule [prf, in mathcomp.analysis.charge]
Radon_Nikodym_change_of_variables [prf, in mathcomp.analysis.charge]
Radon_Nikodym_cscale [prf, in mathcomp.analysis.charge]
Radon_Nikodym_fin_num [prf, in mathcomp.analysis.charge]
radon_nikodym_finite [prf, in mathcomp.analysis.charge]
Radon_Nikodym_integrable [prf, in mathcomp.analysis.charge]
Radon_Nikodym_integral [prf, in mathcomp.analysis.charge]
radon_nikodym_sigma_finite [prf, in mathcomp.analysis.charge]
Radon_Nikodym_SigmaFinite.chain_rule [prf, in mathcomp.analysis.charge]
Radon_Nikodym_SigmaFinite.change_of_variables [prf, in mathcomp.analysis.charge]
Radon_Nikodym_SigmaFinite.f_fin_num [prf, in mathcomp.analysis.charge]
Radon_Nikodym_SigmaFinite.f_ge0 [prf, in mathcomp.analysis.charge]
Radon_Nikodym_SigmaFinite.f_integrable [prf, in mathcomp.analysis.charge]
Radon_Nikodym_SigmaFinite.f_integral [prf, in mathcomp.analysis.charge]
Radon_Nikodym_SigmaFinite.integrableM [prf, in mathcomp.analysis.charge]
Radon_NikodymE [prf, in mathcomp.analysis.charge]
range1rr [prf, in mathcomp.reals.reals]
range1z_inj [prf, in mathcomp.reals.reals]
range1zP [prf, in mathcomp.reals.reals]
range_factor [prf, in mathcomp.classical.set_interval]
range_line_path [prf, in mathcomp.classical.set_interval]
range_oppe [prf, in mathcomp.analysis.ereal]
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_leq_col [prf, in mathcomp.algebra.mxalgebra]
rank_leq_row [prf, in mathcomp.algebra.mxalgebra]
rank_ltmx [prf, in mathcomp.algebra.mxalgebra]
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_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_in_itvoo [prf, in mathcomp.reals.reals]
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]
rationalP [prf, in mathcomp.reals.reals]
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]
Rceil0 [prf, in mathcomp.reals.reals]
Rceil_ge [prf, in mathcomp.reals.reals]
Rceil_ge0 [prf, in mathcomp.reals.reals]
RceilE [prf, in mathcomp.reals.reals]
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_cvgr_ge [prf, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
real_cvgr_gt [prf, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
real_cvgr_le [prf, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
real_cvgr_lt [prf, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
real_fine [prf, in mathcomp.reals.constructive_ereal]
real_leey [prf, in mathcomp.reals.constructive_ereal]
real_leNye [prf, in mathcomp.reals.constructive_ereal]
real_ltNyr [prf, in mathcomp.reals.constructive_ereal]
real_ltr_bound [prf, in mathcomp.classical.unstable]
real_ltr_distlC [prf, in mathcomp.classical.unstable]
real_ltrNbound [prf, in mathcomp.classical.unstable]
real_ltry [prf, in mathcomp.reals.constructive_ereal]
real_maxey [prf, in mathcomp.reals.constructive_ereal]
real_maxNye [prf, in mathcomp.reals.constructive_ereal]
real_miney [prf, in mathcomp.reals.constructive_ereal]
real_minNye [prf, in mathcomp.reals.constructive_ereal]
real_muleN [prf, in mathcomp.reals.constructive_ereal]
real_muleNN [prf, in mathcomp.reals.constructive_ereal]
real_mulNe [prf, in mathcomp.reals.constructive_ereal]
real_mulNyr [prf, in mathcomp.reals.constructive_ereal]
real_mulrNy [prf, in mathcomp.reals.constructive_ereal]
real_mulry [prf, in mathcomp.reals.constructive_ereal]
real_mulyr [prf, in mathcomp.reals.constructive_ereal]
real_order_nbhsE [prf, in mathcomp.analysis.topology_theory.num_topology]
real_similar [prf, in mathcomp.algebra.spectral]
realDe [prf, in mathcomp.reals.constructive_ereal]
realMe [prf, in mathcomp.reals.constructive_ereal]
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]
reflect_eq [prf, in mathcomp.classical.boolp]
regular_fullv [prf, in mathcomp.field.falgebra]
regular_norm_coprime [prf, in mathcomp.solvable.frobenius]
regular_norm_dvd_pred [prf, in mathcomp.solvable.frobenius]
regular_openP [prf, in mathcomp.analysis.normedtype_theory.urysohn]
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_bigcap [prf, in mathcomp.classical.functions]
reindex_bigcprod [prf, in mathcomp.finite_group.gproduct]
reindex_bigcup [prf, in mathcomp.classical.functions]
reindex_esum [prf, in mathcomp.analysis.esum]
reindex_fsbig [prf, in mathcomp.classical.fsbigop]
reindex_fsbigT [prf, in mathcomp.classical.fsbigop]
reindex_inj [prf, in mathcomp.boot.bigop]
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]
remf0 [prf, in mathcomp.finmap.finmap]
remf1_id [prf, in mathcomp.finmap.finmap]
remf1_set [prf, in mathcomp.finmap.finmap]
remf_cat [prf, in mathcomp.finmap.finmap]
remf_comp [prf, in mathcomp.finmap.finmap]
remf_id [prf, in mathcomp.finmap.finmap]
remf_set [prf, in mathcomp.finmap.finmap]
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]
rename_key [prf, in mathcomp.finmap.finperm]
repr_class [prf, in mathcomp.finite_group.fingroup]
repr_classesP [prf, in mathcomp.finite_group.fingroup]
repr_comp_continuous [prf, in mathcomp.analysis.topology_theory.quotient_topology]
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_mem_pblock [prf, in mathcomp.boot.finset]
repr_mem_transversal [prf, in mathcomp.boot.finset]
repr_ofK [prf, in mathcomp.boot.generic_quotient]
repr_rcosetP [prf, in mathcomp.finite_group.fingroup]
repr_set0 [prf, in mathcomp.finite_group.fingroup]
repr_set1 [prf, in mathcomp.finite_group.fingroup]
reprK [prf, in mathcomp.boot.generic_quotient]
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_abse [prf, in mathcomp.analysis.ereal]
restrict_aut_to_normal_num_field [prf, in mathcomp.field.algnum]
restrict_aut_to_num_field [prf, in mathcomp.field.algnum]
restrict_catfsI [prf, in mathcomp.finmap.finmap]
restrict_comp [prf, in mathcomp.classical.functions]
restrict_EFin [prf, in mathcomp.analysis.ereal]
restrict_ge0 [prf, in mathcomp.analysis.numfun]
restrict_indic [prf, in mathcomp.analysis.numfun]
restrict_lee [prf, in mathcomp.analysis.numfun]
restrict_normr [prf, in mathcomp.analysis.numfun]
restrict_set0 [prf, in mathcomp.analysis.numfun]
restricted_cvgE [prf, in mathcomp.analysis.topology_theory.function_spaces]
restrictf0 [prf, in mathcomp.finmap.finmap]
restrictf_cat [prf, in mathcomp.finmap.finmap]
restrictf_cat_domr [prf, in mathcomp.finmap.finmap]
restrictf_comp [prf, in mathcomp.finmap.finmap]
restrictf_id [prf, in mathcomp.finmap.finmap]
restrictf_mkdom [prf, in mathcomp.finmap.finmap]
restrictf_set [prf, in mathcomp.finmap.finmap]
restrictfT [prf, in mathcomp.finmap.finmap]
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]
Rfloor0 [prf, in mathcomp.reals.reals]
Rfloor1 [prf, in mathcomp.reals.reals]
Rfloor_ge_int [prf, in mathcomp.reals.reals]
Rfloor_le [prf, in mathcomp.reals.reals]
Rfloor_le0 [prf, in mathcomp.reals.reals]
Rfloor_lt0 [prf, in mathcomp.reals.reals]
Rfloor_lt_int [prf, in mathcomp.reals.reals]
Rfloor_natz [prf, in mathcomp.reals.reals]
RfloorE [prf, in mathcomp.reals.reals]
rgdP [prf, in mathcomp.solvable.alt]
RGenCInfty.measurable_itv_bnd_infty [prf, in mathcomp.analysis.measurable_realfun]
RGenCInfty.measurable_itv_bounded [prf, in mathcomp.analysis.measurable_realfun]
RGenCInfty.measurableE [prf, in mathcomp.analysis.measurable_realfun]
RGenInftyO.measurable_itv_bnd_infty [prf, in mathcomp.analysis.measurable_realfun]
RGenInftyO.measurable_itv_bounded [prf, in mathcomp.analysis.measurable_realfun]
RGenInftyO.measurableE [prf, in mathcomp.analysis.measurable_realfun]
RGenOInfty.measurable_itv_bnd_infty [prf, in mathcomp.analysis.measurable_realfun]
RGenOInfty.measurable_itv_bounded [prf, in mathcomp.analysis.measurable_realfun]
RGenOInfty.measurableE [prf, in mathcomp.analysis.measurable_realfun]
RGenOpens.measurable_itv_bnd_infty [prf, in mathcomp.analysis.measurable_realfun]
RGenOpens.measurable_itv_bounded [prf, in mathcomp.analysis.measurable_realfun]
RGenOpens.measurable_itv_infty_bnd [prf, in mathcomp.analysis.measurable_realfun]
RGenOpens.measurable_itv_o_infty [prf, in mathcomp.analysis.measurable_realfun]
RGenOpens.measurable_itvoo [prf, in mathcomp.analysis.measurable_realfun]
RGenOpens.measurableE [prf, in mathcomp.analysis.measurable_realfun]
rgraphK [prf, in mathcomp.boot.fingraph]
Rhausdorff [prf, in mathcomp.analysis.topology_theory.separation_axioms]
Rhull0 [prf, in mathcomp.analysis.normedtype_theory.normed_module]
Rhull_involutive [prf, in mathcomp.analysis.normedtype_theory.normed_module]
Rhull_smallest [prf, in mathcomp.analysis.normedtype_theory.normed_module]
RhullK [prf, in mathcomp.analysis.normedtype_theory.normed_module]
RhullT [prf, in mathcomp.analysis.normedtype_theory.normed_module]
riemannR_gt0 [prf, in mathcomp.analysis.exp]
right_arc [prf, in mathcomp.boot.path]
right_bounded_interior [prf, in mathcomp.analysis.topology_theory.num_topology]
right_continuousW [prf, in mathcomp.analysis.lebesgue_stieltjes_measure]
right_trans [prf, in mathcomp.boot.generic_quotient]
ring_display [prf, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
ring_semi_sigma_additive [prf, in mathcomp.analysis.measure_theory.measure_function]
ring_sigma_subadditive [prf, in mathcomp.analysis.measure_theory.measure_function]
ringmx_ind [prf, in mathcomp.algebra.matrix]
Rint0 [prf, in mathcomp.reals.reals]
Rint1 [prf, in mathcomp.reals.reals]
Rint_def [prf, in mathcomp.reals.reals]
Rint_ler_addr1 [prf, in mathcomp.reals.reals]
Rint_ltr_addr1 [prf, in mathcomp.reals.reals]
Rint_subring_closed [prf, in mathcomp.reals.reals]
RintC [prf, in mathcomp.reals.reals]
Rintegral_cst [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_Rintegral]
Rintegral_ge0 [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_Rintegral]
Rintegral_ge0_continuous_FTC2y [prf, in mathcomp.analysis.ftc]
Rintegral_itv_bndo_bndc [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_Rintegral]
Rintegral_itv_obnd_cbnd [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_Rintegral]
Rintegral_itvB [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_Rintegral]
Rintegral_mkcond [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_Rintegral]
Rintegral_mkcondl [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_Rintegral]
Rintegral_mkcondr [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_Rintegral]
Rintegral_onemXn [prf, in mathcomp.analysis.probability_theory.beta_distribution]
Rintegral_set0 [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_Rintegral]
Rintegral_set1 [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_Rintegral]
Rintegral_setU [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_Rintegral]
RintegralB [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_Rintegral]
RintegralD [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_Rintegral]
RintegralZl [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_Rintegral]
RintegralZr [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_Rintegral]
Rintegration_by_parts [prf, in mathcomp.analysis.ftc]
Rintegration_by_substitution_onem [prf, in mathcomp.analysis.ftc]
RintP [prf, in mathcomp.reals.reals]
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]
Rmu_ext [prf, in mathcomp.analysis.measure_theory.measure_extension]
Rolle [prf, in mathcomp.analysis.derive]
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_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_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]
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]
rray_closed [prf, in mathcomp.analysis.topology_theory.order_topology]
rray_open [prf, in mathcomp.analysis.topology_theory.order_topology]
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]
rsubmx_const [prf, in mathcomp.algebra.matrix]
rsubmx_key [prf, in mathcomp.algebra.matrix]
rsubmxEsub [prf, in mathcomp.algebra.matrix]
RtointK [prf, in mathcomp.reals.reals]
RtointN [prf, in mathcomp.reals.reals]
Rtointn [prf, in mathcomp.reals.reals]
Rtointz [prf, in mathcomp.reals.reals]
rV0Pn [prf, in mathcomp.algebra.matrix]
rV_compact [prf, in mathcomp.analysis.normedtype_theory.matrix_normedtype]
rV_compact_nondegenerate [prf, in mathcomp.analysis.normedtype_theory.matrix_normedtype]
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]
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]