R (Definitions)
R_choiceMixin [def, in mathcomp.analysis.Rstruct]
R_choiceType [def, in mathcomp.analysis.Rstruct]
R_CompleteNormedModule [def, in mathcomp.analysis.normedtype]
R_completeType [def, in mathcomp.analysis.normedtype]
R_comRingType [def, in mathcomp.analysis.Rstruct]
R_comUnitRingType [def, in mathcomp.analysis.Rstruct]
R_distrLatticeType [def, in mathcomp.analysis.Rstruct]
R_eqMixin [def, in mathcomp.analysis.Rstruct]
R_eqType [def, in mathcomp.analysis.Rstruct]
R_fieldIdomainMixin [def, in mathcomp.analysis.Rstruct]
R_fieldType [def, in mathcomp.analysis.Rstruct]
R_filteredType [def, in mathcomp.analysis.Rstruct]
R_filteredType [def, in mathcomp.analysis.normedtype]
R_idomainType [def, in mathcomp.analysis.Rstruct]
R_isMeasurable [def, in mathcomp.analysis.lebesgue_measure]
R_latticeType [def, in mathcomp.analysis.Rstruct]
R_normedZmodType [def, in mathcomp.analysis.Rstruct]
R_numDomainType [def, in mathcomp.analysis.Rstruct]
R_numFieldType [def, in mathcomp.analysis.Rstruct]
R_numMixin [def, in mathcomp.analysis.Rstruct]
R_orderType [def, in mathcomp.analysis.Rstruct]
R_pointedType [def, in mathcomp.analysis.normedtype]
R_pointedType [def, in mathcomp.analysis.Rstruct]
R_porderType [def, in mathcomp.analysis.Rstruct]
R_pseudoMetricType [def, in mathcomp.analysis.normedtype]
R_pseudoMetricType [def, in mathcomp.analysis.Rstruct]
R_rcfType [def, in mathcomp.analysis.Rstruct]
R_realArchiFieldType [def, in mathcomp.analysis.Rstruct]
R_realDomainType [def, in mathcomp.analysis.Rstruct]
R_realFieldType [def, in mathcomp.analysis.Rstruct]
R_regular_CompleteNormedModule [def, in mathcomp.analysis.normedtype]
R_regular_completeType [def, in mathcomp.analysis.normedtype]
R_ringMixin [def, in mathcomp.analysis.Rstruct]
R_ringType [def, in mathcomp.analysis.Rstruct]
R_topologicalType [def, in mathcomp.analysis.normedtype]
R_topologicalType [def, in mathcomp.analysis.Rstruct]
R_uniformType [def, in mathcomp.analysis.Rstruct]
R_uniformType [def, in mathcomp.analysis.normedtype]
R_unitRing [def, in mathcomp.analysis.Rstruct]
R_unitRingMixin [def, in mathcomp.analysis.Rstruct]
R_zmodMixin [def, in mathcomp.analysis.Rstruct]
R_zmodType [def, in mathcomp.analysis.Rstruct]
rad [def, in mathcomp.analysis.forms]
Radd_add_law [def, in mathcomp.analysis.Rstruct]
Radd_comoid [def, in mathcomp.analysis.Rstruct]
Radd_monoid [def, in mathcomp.analysis.Rstruct]
radius [def, in mathcomp.analysis.normedtype]
Radon_Nikodym [def, in mathcomp.analysis.charge]
Radon_Nikodym_SigmaFinite.f [def, in mathcomp.analysis.charge]
random_variable [def, in mathcomp.analysis.probability]
range1 [def, in mathcomp.analysis.reals]
rat_pointedType [def, in mathcomp.classical.cardinality]
Rceil [def, in mathcomp.analysis.reals]
Real.archimedeanFieldType [def, in mathcomp.analysis.reals]
Real.base_rcf [def, in mathcomp.analysis.reals]
Real.choiceType [def, in mathcomp.analysis.reals]
Real.class [def, in mathcomp.analysis.reals]
Real.clone [def, in mathcomp.analysis.reals]
Real.comRingType [def, in mathcomp.analysis.reals]
Real.comUnitRingType [def, in mathcomp.analysis.reals]
Real.distrLatticeType [def, in mathcomp.analysis.reals]
Real.eqType [def, in mathcomp.analysis.reals]
Real.EtaMixin [def, in mathcomp.analysis.reals]
Real.fieldType [def, in mathcomp.analysis.reals]
Real.idomainType [def, in mathcomp.analysis.reals]
Real.join_rcfType [def, in mathcomp.analysis.reals]
Real.latticeType [def, in mathcomp.analysis.reals]
Real.normedZmodType [def, in mathcomp.analysis.reals]
Real.numDomainType [def, in mathcomp.analysis.reals]
Real.numFieldType [def, in mathcomp.analysis.reals]
Real.orderType [def, in mathcomp.analysis.reals]
Real.pack [def, in mathcomp.analysis.reals]
Real.porderType [def, in mathcomp.analysis.reals]
Real.rcf_axiom [def, in mathcomp.analysis.reals]
Real.rcfType [def, in mathcomp.analysis.reals]
Real.realDomainType [def, in mathcomp.analysis.reals]
Real.realFieldType [def, in mathcomp.analysis.reals]
Real.ringType [def, in mathcomp.analysis.reals]
Real.unitRingType [def, in mathcomp.analysis.reals]
Real.zmodType [def, in mathcomp.analysis.reals]
real_domain_typ [def, in mathcomp.analysis.signed]
real_field_typ [def, in mathcomp.analysis.signed]
real_mulr_infty [def, in mathcomp.analysis.constructive_ereal]
real_realMixin [def, in mathcomp.analysis.Rstruct]
real_realType [def, in mathcomp.analysis.Rstruct]
Real_sort__canonical__measure_AlgebraOfSets [def, in mathcomp.analysis.lebesgue_measure]
Real_sort__canonical__measure_Measurable [def, in mathcomp.analysis.lebesgue_measure]
Real_sort__canonical__measure_RingOfSets [def, in mathcomp.analysis.lebesgue_measure]
Real_sort__canonical__measure_SemiRingOfSets [def, in mathcomp.analysis.lebesgue_measure]
realfun_itvN_oppr__canonical__functions_Fun [def, in mathcomp.analysis.realfun]
regular_space [def, in mathcomp.analysis.topology]
regular_topology.filteredType [def, in mathcomp.analysis.topology]
regular_topology.normedModType [def, in mathcomp.analysis.normedtype]
regular_topology.pointedType [def, in mathcomp.analysis.topology]
regular_topology.pseudoMetricNormedZmodType [def, in mathcomp.analysis.normedtype]
regular_topology.pseudoMetricType [def, in mathcomp.analysis.topology]
regular_topology.topologicalType [def, in mathcomp.analysis.topology]
regular_topology.uniformType [def, in mathcomp.analysis.topology]
relp [def, in mathcomp.classical.boolp]
rev_mulmx [def, in mathcomp.analysis.forms]
rev_mulr [def, in mathcomp.analysis.derive]
Rfloor [def, in mathcomp.analysis.reals]
Rgeb [def, in mathcomp.analysis.Rstruct]
RGenCInfty.G [def, in mathcomp.analysis.lebesgue_measure]
RGenInftyO.G [def, in mathcomp.analysis.lebesgue_measure]
RGenOInfty.G [def, in mathcomp.analysis.lebesgue_measure]
RGenOpens.G [def, in mathcomp.analysis.lebesgue_measure]
Rgtb [def, in mathcomp.analysis.Rstruct]
Rhull [def, in mathcomp.analysis.normedtype]
riemannR [def, in mathcomp.analysis.exp]
RingOfSets.EtaAndMixinExports.HB_unnamed_factory_7 [def, in mathcomp.analysis.measure]
RingOfSets.EtaAndMixinExports.HB_unnamed_mixin_10 [def, in mathcomp.analysis.measure]
RingOfSets.EtaAndMixinExports.measure_RingOfSets__to__measure_isSemiRingOfSets [def, in mathcomp.analysis.measure]
RingOfSets.EtaAndMixinExports.measure_RingOfSets__to__measure_SemiRingOfSets_isRingOfSets [def, in mathcomp.analysis.measure]
RingOfSets.EtaAndMixinExports.structures_eta__canonical__measure_RingOfSets [def, in mathcomp.analysis.measure]
RingOfSets.Exports.measure_RingOfSets__to__measure_SemiRingOfSets [def, in mathcomp.analysis.measure]
RingOfSets.Exports.measure_RingOfSets_class__to__measure_SemiRingOfSets_class [def, in mathcomp.analysis.measure]
RingOfSets.pack_ [def, in mathcomp.analysis.measure]
RingOfSets.phant_clone [def, in mathcomp.analysis.measure]
RingOfSets.phant_on_ [def, in mathcomp.analysis.measure]
ringOfSets_choiceType [def, in mathcomp.analysis.measure]
ringOfSets_eqType [def, in mathcomp.analysis.measure]
RingOfSets_isAlgebraOfSets.identity_builder [def, in mathcomp.analysis.measure]
RingOfSets_isAlgebraOfSets.phant_axioms [def, in mathcomp.analysis.measure]
RingOfSets_isAlgebraOfSets.phant_Build [def, in mathcomp.analysis.measure]
RingOfSets_isAlgebraOfSets.RingOfSets_isAlgebraOfSets_T__canonical__measure_RingOfSets [def, in mathcomp.analysis.measure]
RingOfSets_isAlgebraOfSets.RingOfSets_isAlgebraOfSets_T__canonical__measure_SemiRingOfSets [def, in mathcomp.analysis.measure]
ringOfSets_ptType [def, in mathcomp.analysis.measure]
Rint [def, in mathcomp.analysis.reals]
Rint_addrPred [def, in mathcomp.analysis.reals]
Rint_keyed [def, in mathcomp.analysis.reals]
Rint_mulrPred [def, in mathcomp.analysis.reals]
Rint_opprPred [def, in mathcomp.analysis.reals]
Rint_semiringPred [def, in mathcomp.analysis.reals]
Rint_smulrPred [def, in mathcomp.analysis.reals]
Rint_subringPred [def, in mathcomp.analysis.reals]
Rint_zmodPred [def, in mathcomp.analysis.reals]
Rintegral [def, in mathcomp.analysis.lebesgue_integral]
Rinvx [def, in mathcomp.analysis.Rstruct]
Rleb [def, in mathcomp.analysis.Rstruct]
Rltb [def, in mathcomp.analysis.Rstruct]
Rmul_comoid [def, in mathcomp.analysis.Rstruct]
Rmul_monoid [def, in mathcomp.analysis.Rstruct]
Rmul_mul_law [def, in mathcomp.analysis.Rstruct]
Rnpos [def, in mathcomp.classical.mathcomp_extra]
root_mean_square [def, in mathcomp.analysis.sequences]
Rtoint [def, in mathcomp.analysis.reals]