R (Global Index)
| 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
R [abbrev, in mathcomp.field.finfield]R [abbrev, in mathcomp.field.finfield]
r012 [def, in mathcomp.solvable.burnside_app]
R012 [def, in mathcomp.solvable.burnside_app]
R012_inj [prf, 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]
R013_inj [prf, 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]
R021_inj [prf, 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]
R024_inj [prf, 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]
R031_inj [prf, 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]
R034_inj [prf, 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]
R042_inj [prf, 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]
R043_inj [prf, 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]
R05_inj [prf, in mathcomp.solvable.burnside_app]
r05_inv [prf, 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]
R14_inj [prf, in mathcomp.solvable.burnside_app]
r14_inv [prf, in mathcomp.solvable.burnside_app]
R14f [def, in mathcomp.solvable.burnside_app]
R1_inj [prf, in mathcomp.solvable.burnside_app]
r1_inv [prf, 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]
R23_inj [prf, in mathcomp.solvable.burnside_app]
R23f [def, in mathcomp.solvable.burnside_app]
R2_inj [prf, in mathcomp.solvable.burnside_app]
r2_inv [prf, 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]
R32_inj [prf, in mathcomp.solvable.burnside_app]
R32f [def, in mathcomp.solvable.burnside_app]
R3_inj [prf, in mathcomp.solvable.burnside_app]
r3_inv [prf, in mathcomp.solvable.burnside_app]
r41 [def, in mathcomp.solvable.burnside_app]
R41 [def, in mathcomp.solvable.burnside_app]
R41_inj [prf, in mathcomp.solvable.burnside_app]
r41_inv [prf, 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]
R50_inj [prf, in mathcomp.solvable.burnside_app]
r50_inv [prf, in mathcomp.solvable.burnside_app]
R50f [def, in mathcomp.solvable.burnside_app]
R_complete [prf, in mathcomp.analysis.normedtype_theory.complete_normed_module]
r_gt0 [abbrev, in mathcomp.analysis.normedtype_theory.vitali_lemma]
R_isMeasurable [def, in mathcomp.analysis.lebesgue_stieltjes_measure]
ract [def, in mathcomp.finite_group.action]
ract_groupAction [def, in mathcomp.finite_group.action]
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]
raction [def, in mathcomp.finite_group.action]
ractpermE [prf, in mathcomp.finite_group.action]
rad [def, in mathcomp.algebra.sesquilinear]
rad_ker [prf, in mathcomp.algebra.sesquilinear]
raddf_int_scalable [prf, in mathcomp.algebra.ssrint]
raddfMz [prf, in mathcomp.algebra.ssrint]
radius [def, in mathcomp.analysis.normedtype_theory.vitali_lemma]
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]
radmx [abbrev, in mathcomp.algebra.sesquilinear]
radmxE [prf, in mathcomp.algebra.sesquilinear]
Radon_Nikodym [def, in mathcomp.analysis.charge]
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 [mod, 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 [def, 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]
radv [abbrev, in mathcomp.algebra.sesquilinear]
random_variable [file, in mathcomp.analysis.probability_theory.random_variable]
random_variable [def, in mathcomp.analysis.probability_theory.random_variable]
range [abbrev, in mathcomp.finite_group.action]
range [abbrev, in mathcomp.classical.classical_sets]
range1 [def, in mathcomp.reals.reals]
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]
rank [def, in mathcomp.solvable.abelian]
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]
rat [file, in mathcomp.algebra.rat]
rat [rec, in mathcomp.algebra.rat]
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_isSub [def, in mathcomp.algebra.rat]
rat_linear [prf, in mathcomp.algebra.rat]
rat_of_Q [def, in mathcomp.algebra.binnums]
rat_poly_scale [prf, in mathcomp.algebra.rat]
Rat_spec [constr, in mathcomp.algebra.rat]
rat_spec [ind, in mathcomp.algebra.rat]
rat_vm_compute [prf, in mathcomp.algebra.rat]
ratArchimedean [mod, in mathcomp.algebra.rat]
ratArchimedean.ceil [def, in mathcomp.algebra.rat]
ratArchimedean.ceilP [prf, in mathcomp.algebra.rat]
ratArchimedean.floor [def, 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.truncn [def, in mathcomp.algebra.rat]
ratArchimedean.truncnP [prf, in mathcomp.algebra.rat]
ratCK [prf, in mathcomp.field.algC]
Ratio [def, in mathcomp.algebra.fraction]
ratio [rec, in mathcomp.algebra.fraction]
Ratio0 [prf, in mathcomp.algebra.fraction]
ratio0 [def, in mathcomp.algebra.fraction]
ratio_ind [scheme, in mathcomp.algebra.fraction]
Ratio_numden [prf, in mathcomp.algebra.fraction]
ratio_rec [scheme, in mathcomp.algebra.fraction]
ratio_rect [scheme, in mathcomp.algebra.fraction]
ratio_sind [scheme, in mathcomp.algebra.fraction]
Ratio_spec [ind, in mathcomp.algebra.fraction]
rational [def, in mathcomp.reals.reals]
rationalP [prf, in mathcomp.reals.reals]
RatioNonNull [constr, in mathcomp.algebra.fraction]
RatioNull [constr, in mathcomp.algebra.fraction]
RatioP [prf, in mathcomp.algebra.fraction]
RatK [prf, in mathcomp.algebra.rat]
ratP [prf, in mathcomp.algebra.rat]
ratr [def, in mathcomp.algebra.rat]
ratr_int [prf, in mathcomp.algebra.rat]
ratr_is_additive [def, in mathcomp.algebra.rat]
ratr_is_monoid_morphism [prf, in mathcomp.algebra.rat]
ratr_is_multiplicative [def, 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 [def, 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]
Rceil [def, in mathcomp.reals.reals]
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]
rcons [def, in mathcomp.boot.seq]
rcons2_infix [prf, in mathcomp.boot.seq]
rcons_bseq [def, in mathcomp.boot.tuple]
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_tuple [def, in mathcomp.boot.tuple]
rcons_tupleP [prf, in mathcomp.boot.tuple]
rcons_uniq [prf, in mathcomp.boot.seq]
rcoset [def, in mathcomp.finite_group.fingroup]
rcoset1 [prf, in mathcomp.finite_group.fingroup]
rcoset_action [def, in mathcomp.finite_group.action]
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_repr_spec [ind, 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]
RcosetReprSpec [constr, in mathcomp.finite_group.fingroup]
rcosetS [prf, in mathcomp.finite_group.fingroup]
rcosets [def, 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 [abbrev, in mathcomp.reals.reals]
Real [mod, in mathcomp.reals.reals]
Real.Algebra_AddMagma_isAddSemigroup_mixin [proj, in mathcomp.reals.reals]
Real.Algebra_BaseAddMagma_isAddMagma_mixin [proj, in mathcomp.reals.reals]
Real.Algebra_BaseAddUMagma_isAddUMagma_mixin [proj, in mathcomp.reals.reals]
Real.Algebra_BaseZmoduleNmodule_isZmodule_mixin [proj, in mathcomp.reals.reals]
Real.Algebra_hasAdd_mixin [proj, in mathcomp.reals.reals]
Real.Algebra_hasOpp_mixin [proj, in mathcomp.reals.reals]
Real.Algebra_hasZero_mixin [proj, in mathcomp.reals.reals]
Real.axioms_ [rec, in mathcomp.reals.reals]
Real.choice_hasChoice_mixin [proj, in mathcomp.reals.reals]
Real.class [proj, in mathcomp.reals.reals]
Real.clone [abbrev, in mathcomp.reals.reals]
Real.copy [abbrev, in mathcomp.reals.reals]
Real.eqtype_hasDecEq_mixin [proj, in mathcomp.reals.reals]
Real.Exports [mod, in mathcomp.reals.reals]
Real.Exports.realType [abbrev, in mathcomp.reals.reals]
Real.GRing_ComUnitRing_isIntegral_mixin [proj, in mathcomp.reals.reals]
Real.GRing_Nmodule_isPzSemiRing_mixin [proj, in mathcomp.reals.reals]
Real.GRing_NzRing_hasMulInverse_mixin [proj, in mathcomp.reals.reals]
Real.GRing_PzSemiRing_isNonZero_mixin [proj, in mathcomp.reals.reals]
Real.GRing_SemiRing_hasCommutativeMul_mixin [proj, in mathcomp.reals.reals]
Real.GRing_UnitRing_isField_mixin [proj, in mathcomp.reals.reals]
Real.Num_Add_isHomo_mixin [proj, in mathcomp.reals.reals]
Real.Num_NumDomain_hasFloorCeilTruncn_mixin [proj, in mathcomp.reals.reals]
Real.Num_NumZmod_isNumRing_mixin [proj, in mathcomp.reals.reals]
Real.Num_POrderedZmodule_hasTransCmp_mixin [proj, in mathcomp.reals.reals]
Real.Num_RealField_isClosed_mixin [proj, in mathcomp.reals.reals]
Real.Num_SemiNormedZmodule_isPositiveDefinite_mixin [proj, in mathcomp.reals.reals]
Real.Num_Zmodule_isSemiNormed_mixin [proj, in mathcomp.reals.reals]
Real.on [abbrev, in mathcomp.reals.reals]
Real.on_ [abbrev, in mathcomp.reals.reals]
Real.Order_DistrLattice_isTotal_mixin [proj, in mathcomp.reals.reals]
Real.Order_isDuallyPreorder_mixin [proj, in mathcomp.reals.reals]
Real.Order_Lattice_isDistributive_mixin [proj, in mathcomp.reals.reals]
Real.Order_POrder_isJoinSemilattice_mixin [proj, in mathcomp.reals.reals]
Real.Order_POrder_isMeetSemilattice_mixin [proj, in mathcomp.reals.reals]
Real.Order_Preorder_isDuallyPOrder_mixin [proj, in mathcomp.reals.reals]
Real.pack_ [def, in mathcomp.reals.reals]
Real.phant_clone [def, in mathcomp.reals.reals]
Real.phant_on_ [def, in mathcomp.reals.reals]
Real.reals_ArchimedeanField_isReal_mixin [proj, in mathcomp.reals.reals]
Real.sort [proj, in mathcomp.reals.reals]
Real.type [rec, in mathcomp.reals.reals]
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_domain_typ [def, in mathcomp.reals.signed]
real_field_typ [def, in mathcomp.reals.signed]
real_fine [prf, in mathcomp.reals.constructive_ereal]
real_interval [file, in mathcomp.reals.real_interval]
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_mulr_infty [def, 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]
real_wider_anyreal [inst, in mathcomp.algebra.interval_inference]
realDe [prf, in mathcomp.reals.constructive_ereal]
RealElpiOperations [mod, in mathcomp.reals.reals]
realfun [file, in mathcomp.analysis.realfun]
realMe [prf, in mathcomp.reals.constructive_ereal]
realmx [abbrev, in mathcomp.algebra.spectral]
realmxC [prf, in mathcomp.algebra.spectral]
realmxD [prf, in mathcomp.algebra.spectral]
reals [file, in mathcomp.reals.reals]
realsym_hermsym [prf, in mathcomp.algebra.spectral]
realz [prf, in mathcomp.algebra.ssrint]
reducebig [def, in mathcomp.boot.bigop]
reducef [def, in mathcomp.finmap.finmap]
refBaseField [abbrev, in mathcomp.field.fieldext]
refBaseField [mod, in mathcomp.field.fieldext]
refBaseField.body [def, in mathcomp.field.fieldext]
refBaseField.unlock [def, in mathcomp.field.fieldext]
refBaseField_Locked [modtype, in mathcomp.field.fieldext]
refBaseField_Locked.body [ax, in mathcomp.field.fieldext]
refBaseField_Locked.unlock [ax, in mathcomp.field.fieldext]
refBaseField_unlock_subterm [def, in mathcomp.field.fieldext]
refBaseField_unlockable [def, in mathcomp.field.fieldext]
reflect_eq [prf, in mathcomp.classical.boolp]
regclosed [def, in mathcomp.analysis.topology_theory.topology_structure]
regopen [def, in mathcomp.analysis.topology_theory.topology_structure]
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_space [def, in mathcomp.analysis.topology_theory.separation_axioms]
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_inside [abbrev, in mathcomp.classical.fsbigop]
reindex_inside_setT [abbrev, in mathcomp.classical.fsbigop]
reindex_omap [prf, in mathcomp.boot.bigop]
reindex_onto [prf, in mathcomp.boot.bigop]
reindex_perm [abbrev, in mathcomp.finite_group.perm]
rel_adjunction [abbrev, in mathcomp.boot.fingraph]
rel_adjunction [abbrev, in mathcomp.boot.fingraph]
rel_adjunction_mem [rec, in mathcomp.boot.fingraph]
rel_base [def, in mathcomp.boot.path]
rel_functor [proj, in mathcomp.boot.fingraph]
rel_unit [proj, in mathcomp.boot.fingraph]
relp [def, in mathcomp.classical.boolp]
relpre_trans [prf, in mathcomp.boot.ssrbool]
relU_sym [prf, in mathcomp.boot.fingraph]
rem [def, in mathcomp.boot.seq]
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]
remgr [def, in mathcomp.finite_group.gproduct]
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]
reparameterize [def, in mathcomp.analysis.homotopy_theory.continuous_path]
repr [def, in mathcomp.finite_group.fingroup]
repr [abbrev, in mathcomp.boot.generic_quotient]
repr [mod, in mathcomp.boot.generic_quotient]
repr.body [def, in mathcomp.boot.generic_quotient]
repr.unlock [def, in mathcomp.boot.generic_quotient]
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_Locked [modtype, in mathcomp.boot.generic_quotient]
repr_Locked.body [ax, in mathcomp.boot.generic_quotient]
repr_Locked.unlock [ax, in mathcomp.boot.generic_quotient]
repr_mem_pblock [prf, in mathcomp.boot.finset]
repr_mem_transversal [prf, in mathcomp.boot.finset]
repr_of [def, in mathcomp.boot.generic_quotient]
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]
repr_unlock [def, in mathcomp.boot.generic_quotient]
repr_unlock_subterm [def, in mathcomp.boot.generic_quotient]
reprK [prf, in mathcomp.boot.generic_quotient]
reshape [def, in mathcomp.boot.seq]
reshape_index [def, in mathcomp.boot.seq]
reshape_indexK [prf, in mathcomp.boot.seq]
reshape_indexP [prf, in mathcomp.boot.seq]
reshape_leq [prf, in mathcomp.boot.seq]
reshape_offset [def, 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 [abbrev, in mathcomp.analysis.measure_theory.measure_function]
restr [abbrev, in mathcomp.analysis.measure_theory.measure_function]
restr [abbrev, in mathcomp.analysis.measure_theory.measure_function]
restr [abbrev, in mathcomp.analysis.charge]
restr [abbrev, in mathcomp.analysis.charge]
restr_isom [prf, in mathcomp.finite_group.morphism]
restr_isom_to [prf, in mathcomp.finite_group.morphism]
restr_perm [def, in mathcomp.finite_group.action]
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_morphism [def, in mathcomp.finite_group.action]
restr_perm_on [prf, in mathcomp.finite_group.action]
restr_permE [prf, in mathcomp.finite_group.action]
restrict [abbrev, in mathcomp.classical.functions]
restrict [abbrev, in mathcomp.classical.functions]
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]
restrictf [def, in mathcomp.finmap.finmap]
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]
restrictmx [abbrev, in mathcomp.algebra.mxred]
restrictmx [abbrev, in mathcomp.algebra.mxred]
restrictmx [abbrev, in mathcomp.algebra.mxpoly]
restrictmx [abbrev, in mathcomp.algebra.mxpoly]
restrm [def, in mathcomp.finite_group.morphism]
restrm_morphism [def, in mathcomp.finite_group.morphism]
restrm_quotientE [prf, in mathcomp.finite_group.quotient]
restrmEsub [prf, in mathcomp.finite_group.morphism]
restrmP [prf, in mathcomp.finite_group.morphism]
resultant [def, in mathcomp.algebra.mxpoly]
resultant_eq0 [prf, in mathcomp.algebra.mxpoly]
resultant_in_ideal [prf, in mathcomp.algebra.mxpoly]
rev [def, in mathcomp.boot.seq]
rev_big_rev [prf, in mathcomp.boot.bigop]
rev_bseq [def, in mathcomp.boot.tuple]
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 [def, in mathcomp.boot.fintype]
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_tuple [def, in mathcomp.boot.tuple]
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 [def, in mathcomp.solvable.alt]
rfd_fun [def, in mathcomp.solvable.alt]
rfd_funP [prf, in mathcomp.solvable.alt]
rfd_iso [prf, in mathcomp.solvable.alt]
rfd_morph [prf, in mathcomp.solvable.alt]
rfd_morphism [def, in mathcomp.solvable.alt]
rfd_odd [prf, in mathcomp.solvable.alt]
rfdP [prf, in mathcomp.solvable.alt]
Rfloor [def, in mathcomp.reals.reals]
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]
rgd [def, in mathcomp.solvable.alt]
rgd_fun [def, in mathcomp.solvable.alt]
rgdP [prf, in mathcomp.solvable.alt]
RGenCInfty [mod, in mathcomp.analysis.measurable_realfun]
RGenCInfty.G [def, in mathcomp.analysis.measurable_realfun]
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 [mod, in mathcomp.analysis.measurable_realfun]
RGenInftyO.G [def, 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 [mod, in mathcomp.analysis.measurable_realfun]
RGenOInfty.G [def, 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 [mod, in mathcomp.analysis.measurable_realfun]
RGenOpens.G [def, 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]
rgraph [def, in mathcomp.boot.fingraph]
rgraphK [prf, in mathcomp.boot.fingraph]
Rhausdorff [prf, in mathcomp.analysis.topology_theory.separation_axioms]
Rhull [def, in mathcomp.analysis.normedtype_theory.normed_module]
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 [def, in mathcomp.analysis.exp]
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_continuous [abbrev, in mathcomp.analysis.lebesgue_stieltjes_measure]
right_continuousW [prf, in mathcomp.analysis.lebesgue_stieltjes_measure]
right_mx_ideal [def, in mathcomp.algebra.mxalgebra]
right_trans [prf, in mathcomp.boot.generic_quotient]
ring [file, in mathcomp.algebra.ring]
ring_display [prf, in mathcomp.algebra.numeric_hierarchy.orderedzmod]
ring_quotient [file, in mathcomp.algebra.ring_quotient]
ring_semi_sigma_additive [prf, in mathcomp.analysis.measure_theory.measure_function]
ring_sigma_subadditive [prf, in mathcomp.analysis.measure_theory.measure_function]
ring_tactic [file, in mathcomp.algebra.ring_tactic]
ringmx_ind [prf, in mathcomp.algebra.matrix]
RingOfSets [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
RingOfSets [mod, in mathcomp.analysis.measure_theory.measurable_structure]
RingOfSets.axioms_ [rec, in mathcomp.analysis.measure_theory.measurable_structure]
RingOfSets.choice_hasChoice_mixin [proj, in mathcomp.analysis.measure_theory.measurable_structure]
RingOfSets.class [proj, in mathcomp.analysis.measure_theory.measurable_structure]
RingOfSets.classical_sets_isPointed_mixin [proj, in mathcomp.analysis.measure_theory.measurable_structure]
RingOfSets.clone [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
RingOfSets.copy [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
RingOfSets.eqtype_hasDecEq_mixin [proj, in mathcomp.analysis.measure_theory.measurable_structure]
RingOfSets.Exports [mod, in mathcomp.analysis.measure_theory.measurable_structure]
RingOfSets.Exports.ringOfSetsType [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
RingOfSets.measurable_structure_isSemiRingOfSets_mixin [proj, in mathcomp.analysis.measure_theory.measurable_structure]
RingOfSets.measurable_structure_SemiRingOfSets_isRingOfSets_mixin [proj, in mathcomp.analysis.measure_theory.measurable_structure]
RingOfSets.on [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
RingOfSets.on_ [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
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.sort [proj, in mathcomp.analysis.measure_theory.measurable_structure]
RingOfSets.type [rec, in mathcomp.analysis.measure_theory.measurable_structure]
RingOfSets_isAlgebraOfSets [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
RingOfSets_isAlgebraOfSets [mod, in mathcomp.analysis.measure_theory.measurable_structure]
RingOfSets_isAlgebraOfSets.axioms [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
RingOfSets_isAlgebraOfSets.axioms_ [rec, in mathcomp.analysis.measure_theory.measurable_structure]
RingOfSets_isAlgebraOfSets.Build [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
RingOfSets_isAlgebraOfSets.Exports [mod, in mathcomp.analysis.measure_theory.measurable_structure]
RingOfSets_isAlgebraOfSets.identity_builder [def, in mathcomp.analysis.measure_theory.measurable_structure]
RingOfSets_isAlgebraOfSets.measurableT [proj, 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]
RingOfSetsElpiOperations [mod, in mathcomp.analysis.measure_theory.measurable_structure]
ringQuotType [abbrev, in mathcomp.algebra.ring_quotient]
rings_modules_and_algebras [file, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
ringType [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
Rint [def, in mathcomp.reals.reals]
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_pred [def, in mathcomp.reals.reals]
Rint_subring_closed [prf, in mathcomp.reals.reals]
RintC [prf, in mathcomp.reals.reals]
Rintegral [def, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_Rintegral]
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]
Rintegral_setU_EFin [abbrev, 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]
rl [abbrev, in mathcomp.classical.functions]
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 [abbrev, in mathcomp.analysis.measure_theory.measure_function]
Rmu [abbrev, in mathcomp.analysis.measure_theory.measure_function]
Rmu_ext [prf, in mathcomp.analysis.measure_theory.measure_extension]
Rolle [prf, in mathcomp.analysis.derive]
root [def, in mathcomp.boot.fingraph]
root [def, in mathcomp.algebra.poly]
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_mean_square [def, in mathcomp.analysis.sequences]
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_of_unity [def, in mathcomp.algebra.poly]
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 [def, in mathcomp.boot.fingraph]
roots_geq_poly_eq0 [prf, in mathcomp.algebra.poly]
roots_pred [def, in mathcomp.boot.fingraph]
roots_root [prf, in mathcomp.boot.fingraph]
rootX [prf, in mathcomp.algebra.poly]
rootZ [prf, in mathcomp.algebra.poly]
rot [def, in mathcomp.solvable.burnside_app]
rot [def, in mathcomp.boot.seq]
rot0 [prf, in mathcomp.boot.seq]
rot1_cons [prf, in mathcomp.boot.seq]
rot_add [def, in mathcomp.boot.seq]
rot_add_mod [prf, in mathcomp.boot.seq]
rot_addC [prf, in mathcomp.boot.seq]
rot_bseq [def, in mathcomp.boot.tuple]
rot_bseqP [prf, in mathcomp.boot.tuple]
rot_cycle [prf, in mathcomp.boot.path]
rot_eq_c0 [prf, in mathcomp.solvable.burnside_app]
rot_group [def, in mathcomp.solvable.burnside_app]
rot_index [prf, in mathcomp.boot.seq]
rot_inj [prf, in mathcomp.boot.seq]
rot_inv [def, in mathcomp.solvable.burnside_app]
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_to_arc_spec [ind, in mathcomp.boot.path]
rot_to_spec [ind, in mathcomp.boot.seq]
rot_tuple [def, in mathcomp.boot.tuple]
rot_tupleP [prf, in mathcomp.boot.tuple]
rot_ucycle [prf, in mathcomp.boot.path]
rot_uniq [prf, in mathcomp.boot.seq]
rotations [def, in mathcomp.solvable.burnside_app]
rotations_group [def, in mathcomp.solvable.burnside_app]
rotations_is_rot [prf, in mathcomp.solvable.burnside_app]
rotD [prf, in mathcomp.boot.seq]
rotK [prf, in mathcomp.boot.seq]
rotr [def, in mathcomp.boot.seq]
rotr1_rcons [prf, in mathcomp.boot.seq]
rotr_bseq [def, in mathcomp.boot.tuple]
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_tuple [def, in mathcomp.boot.tuple]
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]
RotToArcSpec [constr, in mathcomp.boot.path]
RotToSpec [constr, in mathcomp.boot.seq]
row [def, in mathcomp.algebra.matrix]
row' [def, in mathcomp.algebra.matrix]
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_base [def, in mathcomp.algebra.mxalgebra]
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 [def, in mathcomp.algebra.mxalgebra]
row_ebase_unit [prf, in mathcomp.algebra.mxalgebra]
row_eq [prf, in mathcomp.algebra.matrix]
row_free [def, in mathcomp.algebra.mxalgebra]
row_free_castmx [prf, in mathcomp.algebra.mxalgebra]
row_free_inj [prf, in mathcomp.algebra.mxalgebra]
row_free_injr [def, 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 [def, 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_mx [def, 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_mxAx [def, 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_perm [def, 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 [abbrev, in mathcomp.algebra.matrix]
rowsub [abbrev, in mathcomp.algebra.matrix]
rowsub [abbrev, 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]
rr [abbrev, in mathcomp.classical.functions]
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]
rshift [def, in mathcomp.boot.fintype]
rshift1 [prf, in mathcomp.boot.nmodule]
rshift_inj [prf, in mathcomp.boot.fintype]
rsubmx [def, in mathcomp.algebra.matrix]
rsubmx_const [prf, in mathcomp.algebra.matrix]
rsubmx_key [prf, in mathcomp.algebra.matrix]
rsubmxEsub [prf, in mathcomp.algebra.matrix]
rT [abbrev, in mathcomp.analysis.measure_theory.measure_extension]
rT [abbrev, in mathcomp.analysis.measure_theory.measure_extension]
Rtoint [def, in mathcomp.reals.reals]
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]
rVnpoly [def, in mathcomp.algebra.qpoly]
rVnpolyK [prf, in mathcomp.algebra.qpoly]
rVpoly [def, in mathcomp.algebra.mxpoly]
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]