R (Definitions)
| 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 (Definitions)
r012 [def, in mathcomp.solvable.burnside_app]R012 [def, in mathcomp.solvable.burnside_app]
R012f [def, in mathcomp.solvable.burnside_app]
r013 [def, in mathcomp.solvable.burnside_app]
R013 [def, in mathcomp.solvable.burnside_app]
R013f [def, in mathcomp.solvable.burnside_app]
r021 [def, in mathcomp.solvable.burnside_app]
R021 [def, in mathcomp.solvable.burnside_app]
R021f [def, in mathcomp.solvable.burnside_app]
r024 [def, in mathcomp.solvable.burnside_app]
R024 [def, in mathcomp.solvable.burnside_app]
R024f [def, in mathcomp.solvable.burnside_app]
r031 [def, in mathcomp.solvable.burnside_app]
R031 [def, in mathcomp.solvable.burnside_app]
R031f [def, in mathcomp.solvable.burnside_app]
r034 [def, in mathcomp.solvable.burnside_app]
R034 [def, in mathcomp.solvable.burnside_app]
R034f [def, in mathcomp.solvable.burnside_app]
r042 [def, in mathcomp.solvable.burnside_app]
R042 [def, in mathcomp.solvable.burnside_app]
R042f [def, in mathcomp.solvable.burnside_app]
r043 [def, in mathcomp.solvable.burnside_app]
R043 [def, in mathcomp.solvable.burnside_app]
R043f [def, in mathcomp.solvable.burnside_app]
r05 [def, in mathcomp.solvable.burnside_app]
R05 [def, in mathcomp.solvable.burnside_app]
R05f [def, in mathcomp.solvable.burnside_app]
r1 [def, in mathcomp.solvable.burnside_app]
R1 [def, in mathcomp.solvable.burnside_app]
r14 [def, in mathcomp.solvable.burnside_app]
R14 [def, in mathcomp.solvable.burnside_app]
R14f [def, in mathcomp.solvable.burnside_app]
r2 [def, in mathcomp.solvable.burnside_app]
R2 [def, in mathcomp.solvable.burnside_app]
r23 [def, in mathcomp.solvable.burnside_app]
R23 [def, in mathcomp.solvable.burnside_app]
R23f [def, in mathcomp.solvable.burnside_app]
r3 [def, in mathcomp.solvable.burnside_app]
R3 [def, in mathcomp.solvable.burnside_app]
r32 [def, in mathcomp.solvable.burnside_app]
R32 [def, in mathcomp.solvable.burnside_app]
R32f [def, in mathcomp.solvable.burnside_app]
r41 [def, in mathcomp.solvable.burnside_app]
R41 [def, in mathcomp.solvable.burnside_app]
R41f [def, in mathcomp.solvable.burnside_app]
r50 [def, in mathcomp.solvable.burnside_app]
R50 [def, in mathcomp.solvable.burnside_app]
R50f [def, in mathcomp.solvable.burnside_app]
R_isMeasurable [def, in mathcomp.analysis.lebesgue_stieltjes_measure]
ract [def, in mathcomp.finite_group.action]
ract_groupAction [def, in mathcomp.finite_group.action]
raction [def, in mathcomp.finite_group.action]
rad [def, in mathcomp.algebra.sesquilinear]
radius [def, in mathcomp.analysis.normedtype_theory.vitali_lemma]
Radon_Nikodym [def, in mathcomp.analysis.charge]
Radon_Nikodym_SigmaFinite.f [def, in mathcomp.analysis.charge]
random_variable [def, in mathcomp.analysis.probability_theory.random_variable]
range1 [def, in mathcomp.reals.reals]
rank [def, in mathcomp.solvable.abelian]
rat_isSub [def, in mathcomp.algebra.rat]
rat_of_Q [def, in mathcomp.algebra.binnums]
ratArchimedean.ceil [def, in mathcomp.algebra.rat]
ratArchimedean.floor [def, in mathcomp.algebra.rat]
ratArchimedean.truncn [def, in mathcomp.algebra.rat]
Ratio [def, in mathcomp.algebra.fraction]
ratio0 [def, in mathcomp.algebra.fraction]
rational [def, in mathcomp.reals.reals]
ratr [def, in mathcomp.algebra.rat]
ratr_is_additive [def, in mathcomp.algebra.rat]
ratr_is_multiplicative [def, in mathcomp.algebra.rat]
ratz [def, in mathcomp.algebra.rat]
Rceil [def, in mathcomp.reals.reals]
rcons [def, in mathcomp.boot.seq]
rcons_bseq [def, in mathcomp.boot.tuple]
rcons_tuple [def, in mathcomp.boot.tuple]
rcoset [def, in mathcomp.finite_group.fingroup]
rcoset_action [def, in mathcomp.finite_group.action]
rcosets [def, in mathcomp.finite_group.fingroup]
Real.pack_ [def, in mathcomp.reals.reals]
Real.phant_clone [def, in mathcomp.reals.reals]
Real.phant_on_ [def, in mathcomp.reals.reals]
real_domain_typ [def, in mathcomp.reals.signed]
real_field_typ [def, in mathcomp.reals.signed]
real_mulr_infty [def, in mathcomp.reals.constructive_ereal]
reducebig [def, in mathcomp.boot.bigop]
reducef [def, in mathcomp.finmap.finmap]
refBaseField.body [def, in mathcomp.field.fieldext]
refBaseField.unlock [def, in mathcomp.field.fieldext]
refBaseField_unlock_subterm [def, in mathcomp.field.fieldext]
refBaseField_unlockable [def, in mathcomp.field.fieldext]
regclosed [def, in mathcomp.analysis.topology_theory.topology_structure]
regopen [def, in mathcomp.analysis.topology_theory.topology_structure]
regular_space [def, in mathcomp.analysis.topology_theory.separation_axioms]
rel_base [def, in mathcomp.boot.path]
relp [def, in mathcomp.classical.boolp]
rem [def, in mathcomp.boot.seq]
remgr [def, in mathcomp.finite_group.gproduct]
reparameterize [def, in mathcomp.analysis.homotopy_theory.continuous_path]
repr [def, in mathcomp.finite_group.fingroup]
repr.body [def, in mathcomp.boot.generic_quotient]
repr.unlock [def, in mathcomp.boot.generic_quotient]
repr_of [def, in mathcomp.boot.generic_quotient]
repr_unlock [def, in mathcomp.boot.generic_quotient]
repr_unlock_subterm [def, in mathcomp.boot.generic_quotient]
reshape [def, in mathcomp.boot.seq]
reshape_index [def, in mathcomp.boot.seq]
reshape_offset [def, in mathcomp.boot.seq]
restr_perm [def, in mathcomp.finite_group.action]
restr_perm_morphism [def, in mathcomp.finite_group.action]
restrictf [def, in mathcomp.finmap.finmap]
restrm [def, in mathcomp.finite_group.morphism]
restrm_morphism [def, in mathcomp.finite_group.morphism]
resultant [def, in mathcomp.algebra.mxpoly]
rev [def, in mathcomp.boot.seq]
rev_bseq [def, in mathcomp.boot.tuple]
rev_ord [def, in mathcomp.boot.fintype]
rev_tuple [def, in mathcomp.boot.tuple]
rfd [def, in mathcomp.solvable.alt]
rfd_fun [def, in mathcomp.solvable.alt]
rfd_morphism [def, in mathcomp.solvable.alt]
Rfloor [def, in mathcomp.reals.reals]
rgd [def, in mathcomp.solvable.alt]
rgd_fun [def, in mathcomp.solvable.alt]
RGenCInfty.G [def, in mathcomp.analysis.measurable_realfun]
RGenInftyO.G [def, in mathcomp.analysis.measurable_realfun]
RGenOInfty.G [def, in mathcomp.analysis.measurable_realfun]
RGenOpens.G [def, in mathcomp.analysis.measurable_realfun]
rgraph [def, in mathcomp.boot.fingraph]
Rhull [def, in mathcomp.analysis.normedtype_theory.normed_module]
riemannR [def, in mathcomp.analysis.exp]
right_mx_ideal [def, in mathcomp.algebra.mxalgebra]
RingOfSets.pack_ [def, in mathcomp.analysis.measure_theory.measurable_structure]
RingOfSets.phant_clone [def, in mathcomp.analysis.measure_theory.measurable_structure]
RingOfSets.phant_on_ [def, in mathcomp.analysis.measure_theory.measurable_structure]
RingOfSets_isAlgebraOfSets.identity_builder [def, in mathcomp.analysis.measure_theory.measurable_structure]
RingOfSets_isAlgebraOfSets.phant_axioms [def, in mathcomp.analysis.measure_theory.measurable_structure]
RingOfSets_isAlgebraOfSets.phant_Build [def, in mathcomp.analysis.measure_theory.measurable_structure]
Rint [def, in mathcomp.reals.reals]
Rint_pred [def, in mathcomp.reals.reals]
Rintegral [def, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_Rintegral]
root [def, in mathcomp.boot.fingraph]
root [def, in mathcomp.algebra.poly]
root_mean_square [def, in mathcomp.analysis.sequences]
root_of_unity [def, in mathcomp.algebra.poly]
roots [def, in mathcomp.boot.fingraph]
roots_pred [def, in mathcomp.boot.fingraph]
rot [def, in mathcomp.solvable.burnside_app]
rot [def, in mathcomp.boot.seq]
rot_add [def, in mathcomp.boot.seq]
rot_bseq [def, in mathcomp.boot.tuple]
rot_group [def, in mathcomp.solvable.burnside_app]
rot_inv [def, in mathcomp.solvable.burnside_app]
rot_tuple [def, in mathcomp.boot.tuple]
rotations [def, in mathcomp.solvable.burnside_app]
rotations_group [def, in mathcomp.solvable.burnside_app]
rotr [def, in mathcomp.boot.seq]
rotr_bseq [def, in mathcomp.boot.tuple]
rotr_tuple [def, in mathcomp.boot.tuple]
row [def, in mathcomp.algebra.matrix]
row' [def, in mathcomp.algebra.matrix]
row_base [def, in mathcomp.algebra.mxalgebra]
row_ebase [def, in mathcomp.algebra.mxalgebra]
row_free [def, in mathcomp.algebra.mxalgebra]
row_free_injr [def, in mathcomp.algebra.mxalgebra]
row_full [def, in mathcomp.algebra.mxalgebra]
row_mx [def, in mathcomp.algebra.matrix]
row_mxAx [def, in mathcomp.algebra.matrix]
row_perm [def, in mathcomp.algebra.matrix]
rshift [def, in mathcomp.boot.fintype]
rsubmx [def, in mathcomp.algebra.matrix]
Rtoint [def, in mathcomp.reals.reals]
rVnpoly [def, in mathcomp.algebra.qpoly]
rVpoly [def, in mathcomp.algebra.mxpoly]