Files

  • mathcomp

    • Top source

    S (Global Index)

    Files ABCDEFGHIJKLMNOPQRSTUVWXYZ_
    Definitions ABCDEFGHIJKLMNOPQRSTUVWXYZ_
    Lemmas ABCDEFGHIJKLMNOPQRSTUVWXYZ_
    Abbreviations ABCDEFGHIJKLMNOPQRSTUVWXYZ_
    Global Index ABCDEFGHIJKLMNOPQRSTUVWXYZ_
    Notations

    S

    S [abbrev, in mathcomp.analysis.topology_theory.supremum_topology]
    S [abbrev, in mathcomp.analysis.topology_theory.separation_axioms]
    S [abbrev, in mathcomp.analysis.topology_theory.initial_topology]
    s0 [def, in mathcomp.solvable.burnside_app]
    S0 [def, in mathcomp.solvable.burnside_app]
    s05 [def, in mathcomp.solvable.burnside_app]
    S05 [def, in mathcomp.solvable.burnside_app]
    S05_inj [prf, in mathcomp.solvable.burnside_app]
    S05f [def, in mathcomp.solvable.burnside_app]
    S0_inv [prf, in mathcomp.solvable.burnside_app]
    S0f [def, in mathcomp.solvable.burnside_app]
    s1 [def, in mathcomp.solvable.burnside_app]
    S1 [def, in mathcomp.solvable.burnside_app]
    s14 [def, in mathcomp.solvable.burnside_app]
    S14 [def, in mathcomp.solvable.burnside_app]
    S14_inj [prf, in mathcomp.solvable.burnside_app]
    S14f [def, in mathcomp.solvable.burnside_app]
    S1_inv [prf, in mathcomp.solvable.burnside_app]
    S1f [def, in mathcomp.solvable.burnside_app]
    s2 [def, in mathcomp.solvable.burnside_app]
    S2 [def, in mathcomp.solvable.burnside_app]
    s23 [def, in mathcomp.solvable.burnside_app]
    S23 [def, in mathcomp.solvable.burnside_app]
    s23_inv [prf, in mathcomp.solvable.burnside_app]
    S23_inv [prf, in mathcomp.solvable.burnside_app]
    S23f [def, in mathcomp.solvable.burnside_app]
    S2_inv [prf, in mathcomp.solvable.burnside_app]
    S2f [def, in mathcomp.solvable.burnside_app]
    s3 [def, in mathcomp.solvable.burnside_app]
    S3 [def, in mathcomp.solvable.burnside_app]
    S3_inv [prf, in mathcomp.solvable.burnside_app]
    S3f [def, in mathcomp.solvable.burnside_app]
    s4 [def, in mathcomp.solvable.burnside_app]
    S4 [def, in mathcomp.solvable.burnside_app]
    S4_inv [prf, in mathcomp.solvable.burnside_app]
    S4f [def, in mathcomp.solvable.burnside_app]
    s5 [def, in mathcomp.solvable.burnside_app]
    S5 [def, in mathcomp.solvable.burnside_app]
    S5_inv [prf, in mathcomp.solvable.burnside_app]
    S5f [def, in mathcomp.solvable.burnside_app]
    s6 [def, in mathcomp.solvable.burnside_app]
    S6 [def, in mathcomp.solvable.burnside_app]
    S6_inv [prf, in mathcomp.solvable.burnside_app]
    S6f [def, in mathcomp.solvable.burnside_app]
    s_finite [def, in mathcomp.analysis.measure_theory.measure_function]
    same_connect [prf, in mathcomp.boot.fingraph]
    same_connect1 [prf, in mathcomp.boot.fingraph]
    same_connect1r [prf, in mathcomp.boot.fingraph]
    same_connect_r [prf, in mathcomp.boot.fingraph]
    same_connect_rev [prf, in mathcomp.boot.fingraph]
    same_connected_component [prf, in mathcomp.analysis.topology_theory.connected]
    same_fconnect1 [prf, in mathcomp.boot.fingraph]
    same_fconnect1_r [prf, in mathcomp.boot.fingraph]
    same_fconnect_finv [prf, in mathcomp.boot.fingraph]
    same_pblock [prf, in mathcomp.boot.finset]
    same_prefix [def, in mathcomp.classical.classical_orders]
    same_prefix0 [prf, in mathcomp.classical.classical_orders]
    same_prefix_leq [prf, in mathcomp.classical.classical_orders]
    same_prefix_refl [prf, in mathcomp.classical.classical_orders]
    same_prefix_sym [prf, in mathcomp.classical.classical_orders]
    same_prefix_trans [prf, in mathcomp.classical.classical_orders]
    scalar_mx [def, in mathcomp.algebra.matrix]
    scalar_mx_block [prf, in mathcomp.algebra.matrix]
    scalar_mx_cent [prf, in mathcomp.algebra.mxalgebra]
    scalar_mx_is_additive [def, in mathcomp.algebra.matrix]
    scalar_mx_is_diag [prf, in mathcomp.algebra.matrix]
    scalar_mx_is_monoid_morphism [prf, in mathcomp.algebra.matrix]
    scalar_mx_is_multiplicative [def, in mathcomp.algebra.matrix]
    scalar_mx_is_nmod_morphism [prf, in mathcomp.algebra.matrix]
    scalar_mx_is_scalar [prf, in mathcomp.algebra.matrix]
    scalar_mx_is_semi_additive [def, in mathcomp.algebra.matrix]
    scalar_mx_is_trig [prf, in mathcomp.algebra.matrix]
    scalar_mx_is_zmod_morphism [prf, in mathcomp.algebra.matrix]
    scalar_mx_key [prf, in mathcomp.algebra.matrix]
    scalar_mx_sum_delta [prf, in mathcomp.algebra.matrix]
    scalar_mxC [prf, in mathcomp.algebra.matrix]
    scalar_mxM [prf, in mathcomp.algebra.matrix]
    scale [abbrev, in mathcomp.analysis.measure_theory.measure_function]
    scale0mx [prf, in mathcomp.algebra.matrix]
    scale1mx [prf, in mathcomp.algebra.matrix]
    scale_0poly [prf, in mathcomp.algebra.poly]
    scale_1poly [prf, in mathcomp.algebra.poly]
    scale_ball [def, in mathcomp.analysis.normedtype_theory.vitali_lemma]
    scale_ball0 [prf, in mathcomp.analysis.normedtype_theory.vitali_lemma]
    scale_ball1 [prf, in mathcomp.analysis.normedtype_theory.vitali_lemma]
    scale_ball_set0 [prf, in mathcomp.analysis.normedtype_theory.vitali_lemma]
    scale_ballE [prf, in mathcomp.analysis.normedtype_theory.vitali_lemma]
    scale_block_mx [prf, in mathcomp.algebra.matrix]
    scale_col_mx [prf, in mathcomp.algebra.matrix]
    scale_continuous [def, in mathcomp.analysis.normedtype_theory.tvs]
    scale_fimfun [def, in mathcomp.analysis.numfun]
    scale_lfun [def, in mathcomp.algebra.vector]
    scale_lfunE [prf, in mathcomp.algebra.vector]
    scale_littleo [def, in mathcomp.analysis.landau]
    scale_mfun [def, in mathcomp.analysis.measurable_realfun]
    scale_nnsfun [def, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
    scale_pair [def, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
    scale_poly [def, in mathcomp.algebra.poly]
    scale_poly_def [def, in mathcomp.algebra.poly]
    scale_poly_eq0 [prf, in mathcomp.algebra.poly]
    scale_poly_key [prf, in mathcomp.algebra.poly]
    scale_poly_unlockable [def, in mathcomp.algebra.poly]
    scale_polyA [prf, in mathcomp.algebra.poly]
    scale_polyAl [prf, in mathcomp.algebra.poly]
    scale_polyC [prf, in mathcomp.algebra.poly]
    scale_polyDl [prf, in mathcomp.algebra.poly]
    scale_polyDr [prf, in mathcomp.algebra.poly]
    scale_polyE [prf, in mathcomp.algebra.poly]
    scale_row_mx [prf, in mathcomp.algebra.matrix]
    scale_scalar_mx [prf, in mathcomp.algebra.matrix]
    scale_sfun [def, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
    scale_unif_continuous [def, in mathcomp.analysis.normedtype_theory.tvs]
    scalel_continuous [prf, in mathcomp.analysis.normedtype_theory.normed_module]
    scalemx [def, in mathcomp.algebra.matrix]
    scalemx1 [prf, in mathcomp.algebra.matrix]
    scalemx_const [prf, in mathcomp.algebra.matrix]
    scalemx_eq0 [prf, in mathcomp.algebra.matrix]
    scalemx_inj [prf, in mathcomp.algebra.matrix]
    scalemx_key [prf, in mathcomp.algebra.matrix]
    scalemx_sub [prf, in mathcomp.algebra.mxalgebra]
    scalemxA [prf, in mathcomp.algebra.matrix]
    scalemxAl [prf, in mathcomp.algebra.matrix]
    scalemxAr [prf, in mathcomp.algebra.matrix]
    scalemxDl [prf, in mathcomp.algebra.matrix]
    scalemxDr [prf, in mathcomp.algebra.matrix]
    scaleo [prf, in mathcomp.analysis.landau]
    scaleolx [prf, in mathcomp.analysis.landau]
    scaleox [prf, in mathcomp.analysis.landau]
    scaler1 [prf, in mathcomp.analysis.normedtype_theory.normed_module]
    scaler_continuous [prf, in mathcomp.analysis.normedtype_theory.normed_module]
    scaler_int [prf, in mathcomp.algebra.ssrint]
    scalerMzl [prf, in mathcomp.algebra.ssrint]
    scalerMzr [prf, in mathcomp.algebra.ssrint]
    scalezrE [prf, in mathcomp.algebra.ssrint]
    scalq [def, in mathcomp.algebra.rat]
    scalq_def [prf, in mathcomp.algebra.rat]
    scalq_eq0 [prf, in mathcomp.algebra.rat]
    scalqE [prf, in mathcomp.algebra.rat]
    scalrfctE [prf, in mathcomp.classical.functions]
    scanl [def, in mathcomp.boot.seq]
    scanl_bseq [def, in mathcomp.boot.tuple]
    scanl_bseqP [prf, in mathcomp.boot.tuple]
    scanl_cat [prf, in mathcomp.boot.seq]
    scanl_rcons [prf, in mathcomp.boot.seq]
    scanl_tuple [def, in mathcomp.boot.tuple]
    scanl_tupleP [prf, in mathcomp.boot.tuple]
    scanlK [prf, in mathcomp.boot.seq]
    schmidt [def, in mathcomp.algebra.spectral]
    schmidt_complete [def, in mathcomp.algebra.spectral]
    schmidt_complete_unitarymx [prf, in mathcomp.algebra.spectral]
    schmidt_sub [prf, in mathcomp.algebra.spectral]
    schmidt_unitarymx [prf, in mathcomp.algebra.spectral]
    Schur [prf, in mathcomp.algebra.spectral]
    SchurZassenhaus_split [prf, in mathcomp.solvable.hall]
    SchurZassenhaus_trans_actsol [prf, in mathcomp.solvable.hall]
    SchurZassenhaus_trans_sol [prf, in mathcomp.solvable.hall]
    SCN [def, in mathcomp.solvable.maximal]
    SCN_abelian [prf, in mathcomp.solvable.maximal]
    SCN_at [def, in mathcomp.solvable.maximal]
    SCN_max [prf, in mathcomp.solvable.maximal]
    SCN_P [prf, in mathcomp.solvable.maximal]
    sd1 [def, in mathcomp.solvable.burnside_app]
    Sd1 [def, in mathcomp.solvable.burnside_app]
    Sd1_inj [prf, in mathcomp.solvable.burnside_app]
    sd1_inv [prf, in mathcomp.solvable.burnside_app]
    sd2 [def, in mathcomp.solvable.burnside_app]
    Sd2 [def, in mathcomp.solvable.burnside_app]
    Sd2_inj [prf, in mathcomp.solvable.burnside_app]
    sd2_inv [prf, in mathcomp.solvable.burnside_app]
    SdPair [constr, in mathcomp.finite_group.gproduct]
    sdpair1 [def, in mathcomp.finite_group.gproduct]
    sdpair1_morphism [def, in mathcomp.finite_group.gproduct]
    sdpair1_morphM [prf, in mathcomp.finite_group.gproduct]
    sdpair2 [def, in mathcomp.finite_group.gproduct]
    sdpair2_morphism [def, in mathcomp.finite_group.gproduct]
    sdpair2_morphM [prf, in mathcomp.finite_group.gproduct]
    sdpair_act [prf, in mathcomp.finite_group.gproduct]
    sdpair_setact [prf, in mathcomp.finite_group.gproduct]
    sdpairE [prf, in mathcomp.finite_group.gproduct]
    sdprod [abbrev, in mathcomp.finite_group.gproduct]
    sdprod [abbrev, in mathcomp.finite_group.gproduct]
    sdprod1g [prf, in mathcomp.finite_group.gproduct]
    sdprod_by [ind, in mathcomp.finite_group.gproduct]
    sdprod_by_ind [scheme, in mathcomp.finite_group.gproduct]
    sdprod_by_rec [scheme, in mathcomp.finite_group.gproduct]
    sdprod_by_rect [scheme, in mathcomp.finite_group.gproduct]
    sdprod_by_sind [scheme, in mathcomp.finite_group.gproduct]
    sdprod_card [prf, in mathcomp.finite_group.gproduct]
    sdprod_compl [prf, in mathcomp.finite_group.gproduct]
    sdprod_context [prf, in mathcomp.finite_group.gproduct]
    sdprod_groupType [def, in mathcomp.finite_group.gproduct]
    sdprod_Hall [prf, in mathcomp.solvable.pgroup]
    sdprod_Hall_p'coreP [prf, in mathcomp.solvable.pgroup]
    sdprod_Hall_pcoreP [prf, in mathcomp.solvable.pgroup]
    sdprod_inv [def, in mathcomp.finite_group.gproduct]
    sdprod_inv_proof [prf, in mathcomp.finite_group.gproduct]
    sdprod_isog [prf, in mathcomp.finite_group.gproduct]
    sdprod_isom [prf, in mathcomp.finite_group.gproduct]
    sdprod_modl [prf, in mathcomp.finite_group.gproduct]
    sdprod_modr [prf, in mathcomp.finite_group.gproduct]
    sdprod_mul [def, in mathcomp.finite_group.gproduct]
    sdprod_mul1g [prf, in mathcomp.finite_group.gproduct]
    sdprod_mul_proof [prf, in mathcomp.finite_group.gproduct]
    sdprod_mulgA [prf, in mathcomp.finite_group.gproduct]
    sdprod_mulVg [prf, in mathcomp.finite_group.gproduct]
    sdprod_normal_complP [prf, in mathcomp.finite_group.gproduct]
    sdprod_normal_p'HallP [prf, in mathcomp.solvable.pgroup]
    sdprod_normal_pHallP [prf, in mathcomp.solvable.pgroup]
    sdprod_one [def, in mathcomp.finite_group.gproduct]
    sdprod_p'core_HallP [prf, in mathcomp.solvable.pgroup]
    sdprod_pcore_HallP [prf, in mathcomp.solvable.pgroup]
    sdprod_recl [prf, in mathcomp.finite_group.gproduct]
    sdprod_recr [prf, in mathcomp.finite_group.gproduct]
    sdprod_sdpair [prf, in mathcomp.finite_group.gproduct]
    sdprod_subr [prf, in mathcomp.finite_group.gproduct]
    sdprodE [prf, in mathcomp.finite_group.gproduct]
    sdprodEY [prf, in mathcomp.finite_group.gproduct]
    sdprodg1 [prf, in mathcomp.finite_group.gproduct]
    sdprodJ [prf, in mathcomp.finite_group.gproduct]
    sdprodm [def, in mathcomp.finite_group.gproduct]
    sdprodm_eqf [prf, in mathcomp.finite_group.gproduct]
    sdprodm_morphism [def, in mathcomp.finite_group.gproduct]
    sdprodm_norm [prf, in mathcomp.finite_group.gproduct]
    sdprodm_sub [prf, in mathcomp.finite_group.gproduct]
    sdprodmE [prf, in mathcomp.finite_group.gproduct]
    sdprodmEl [prf, in mathcomp.finite_group.gproduct]
    sdprodmEr [prf, in mathcomp.finite_group.gproduct]
    sdprodP [prf, in mathcomp.finite_group.gproduct]
    sdprodW [prf, in mathcomp.finite_group.gproduct]
    sdprodWC [prf, in mathcomp.finite_group.gproduct]
    sdprodWpp [prf, in mathcomp.finite_group.gproduct]
    sdprodWY [prf, in mathcomp.finite_group.gproduct]
    sdrop [def, in mathcomp.analysis.sequences]
    sdT [abbrev, in mathcomp.finite_group.gproduct]
    sdval [abbrev, in mathcomp.finite_group.gproduct]
    second_countable [def, in mathcomp.analysis.topology_theory.topology_structure]
    second_derivative_convex [prf, in mathcomp.analysis.realfun]
    second_isog [prf, in mathcomp.finite_group.quotient]
    second_isom [prf, in mathcomp.finite_group.quotient]
    section [ind, in mathcomp.solvable.jordanholder]
    section_group [def, in mathcomp.solvable.jordanholder]
    section_ind [scheme, in mathcomp.solvable.jordanholder]
    section_isog [def, in mathcomp.solvable.jordanholder]
    section_rec [scheme, in mathcomp.solvable.jordanholder]
    section_rect [scheme, in mathcomp.solvable.jordanholder]
    section_repr [def, in mathcomp.solvable.jordanholder]
    section_repr_isog [prf, in mathcomp.solvable.jordanholder]
    section_reprP [prf, in mathcomp.solvable.jordanholder]
    section_sind [scheme, in mathcomp.solvable.jordanholder]
    sedDI_closedP [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
    segment_can_continuous [prf, in mathcomp.analysis.realfun]
    segment_can_ge [prf, in mathcomp.analysis.realfun]
    segment_can_ge_continuous [prf, in mathcomp.analysis.realfun]
    segment_can_le [prf, in mathcomp.analysis.realfun]
    segment_can_le_continuous [prf, in mathcomp.analysis.realfun]
    segment_can_mono [prf, in mathcomp.analysis.realfun]
    segment_compact [prf, in mathcomp.analysis.normedtype_theory.normed_module]
    segment_connected [prf, in mathcomp.analysis.normedtype_theory.normed_module]
    segment_continuous_can_sym [prf, in mathcomp.analysis.realfun]
    segment_continuous_ge_can_sym [prf, in mathcomp.analysis.realfun]
    segment_continuous_ge_surjective [prf, in mathcomp.analysis.realfun]
    segment_continuous_inj_ge [prf, in mathcomp.analysis.realfun]
    segment_continuous_inj_le [prf, in mathcomp.analysis.realfun]
    segment_continuous_le_can_sym [prf, in mathcomp.analysis.realfun]
    segment_continuous_le_surjective [prf, in mathcomp.analysis.realfun]
    segment_continuous_surjective [prf, in mathcomp.analysis.realfun]
    segment_dec_surj_continuous [prf, in mathcomp.analysis.realfun]
    segment_inc_surj_continuous [prf, in mathcomp.analysis.realfun]
    segment_mono_surj_continuous [prf, in mathcomp.analysis.realfun]
    self_sub [def, in mathcomp.analysis.normedtype_theory.normed_module]
    selfFiltered [abbrev, in mathcomp.classical.filter]
    selfFiltered [mod, in mathcomp.classical.filter]
    selfFiltered.axioms [abbrev, in mathcomp.classical.filter]
    selfFiltered.axioms_ [rec, in mathcomp.classical.filter]
    selfFiltered.Build [abbrev, in mathcomp.classical.filter]
    selfFiltered.Exports [mod, in mathcomp.classical.filter]
    selfFiltered.identity_builder [def, in mathcomp.classical.filter]
    selfFiltered.phant_axioms [def, in mathcomp.classical.filter]
    selfFiltered.phant_Build [def, in mathcomp.classical.filter]
    selfPbij [abbrev, in mathcomp.classical.functions]
    semi_additive [def, in mathcomp.analysis.measure_theory.measure_function]
    semi_additive2 [def, in mathcomp.analysis.measure_theory.measure_function]
    semi_additive2E [prf, in mathcomp.analysis.measure_theory.measure_function]
    semi_additiveE [prf, in mathcomp.analysis.measure_theory.measure_function]
    semi_additiveW [prf, in mathcomp.analysis.measure_theory.measure_function]
    semi_measurableD [def, in mathcomp.analysis.measure_theory.measurable_structure]
    semi_setD_closed [def, in mathcomp.analysis.measure_theory.measurable_structure]
    semi_sigma_additive [def, in mathcomp.analysis.measure_theory.measure_function]
    semi_sigma_additive_elebesgue_measure [prf, in mathcomp.analysis.lebesgue_measure]
    semi_sigma_additive_is_additive [prf, in mathcomp.analysis.measure_theory.measure_function]
    semi_sigma_additive_kproduct [prf, in mathcomp.analysis.kernel]
    semi_sigma_additive_nng_induced [prf, in mathcomp.analysis.charge]
    semi_sigma_additiveE [prf, in mathcomp.analysis.measure_theory.measure_function]
    semiAlgType [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
    SemiDihedral [constr, in mathcomp.solvable.extremal]
    semidihedral_classP [prf, in mathcomp.solvable.extremal]
    semidihedral_gtype [def, in mathcomp.solvable.extremal]
    semidihedral_structure [prf, in mathcomp.solvable.extremal]
    semidirect_product [def, in mathcomp.finite_group.gproduct]
    Semigroup [abbrev, in mathcomp.boot.monoid]
    Semigroup [mod, in mathcomp.boot.monoid]
    SemiGroup [mod, in mathcomp.boot.bigop]
    Semigroup.axioms_ [rec, in mathcomp.boot.monoid]
    SemiGroup.Builders_1 [mod, in mathcomp.boot.bigop]
    SemiGroup.Builders_1.Builders_Export_7 [mod, in mathcomp.boot.bigop]
    SemiGroup.Builders_1.opA [abbrev, in mathcomp.boot.bigop]
    SemiGroup.Builders_1.opC [abbrev, in mathcomp.boot.bigop]
    SemiGroup.Builders_1.Super [mod, in mathcomp.boot.bigop]
    Semigroup.choice_hasChoice_mixin [proj, in mathcomp.boot.monoid]
    Semigroup.class [proj, in mathcomp.boot.monoid]
    Semigroup.clone [abbrev, in mathcomp.boot.monoid]
    SemiGroup.com_law [abbrev, in mathcomp.boot.bigop]
    SemiGroup.ComLaw [abbrev, in mathcomp.boot.bigop]
    SemiGroup.ComLaw [mod, in mathcomp.boot.bigop]
    SemiGroup.ComLaw.axioms_ [rec, in mathcomp.boot.bigop]
    SemiGroup.ComLaw.class [proj, in mathcomp.boot.bigop]
    SemiGroup.ComLaw.clone [abbrev, in mathcomp.boot.bigop]
    SemiGroup.ComLaw.copy [abbrev, in mathcomp.boot.bigop]
    SemiGroup.ComLaw.Exports [mod, in mathcomp.boot.bigop]
    SemiGroup.ComLaw.on [abbrev, in mathcomp.boot.bigop]
    SemiGroup.ComLaw.on_ [abbrev, in mathcomp.boot.bigop]
    SemiGroup.ComLaw.pack_ [def, in mathcomp.boot.bigop]
    SemiGroup.ComLaw.phant_clone [def, in mathcomp.boot.bigop]
    SemiGroup.ComLaw.phant_on_ [def, in mathcomp.boot.bigop]
    SemiGroup.ComLaw.SemiGroup_isCommutativeLaw_mixin [proj, in mathcomp.boot.bigop]
    SemiGroup.ComLaw.SemiGroup_isLaw_mixin [proj, in mathcomp.boot.bigop]
    SemiGroup.ComLaw.sort [proj, in mathcomp.boot.bigop]
    SemiGroup.ComLaw.type [rec, in mathcomp.boot.bigop]
    SemiGroup.ComLawElpiOperations [mod, in mathcomp.boot.bigop]
    Semigroup.copy [abbrev, in mathcomp.boot.monoid]
    Semigroup.eqtype_hasDecEq_mixin [proj, in mathcomp.boot.monoid]
    Semigroup.Exports [mod, in mathcomp.boot.monoid]
    SemiGroup.Exports [mod, in mathcomp.boot.bigop]
    Semigroup.Exports.semigroupType [abbrev, in mathcomp.boot.monoid]
    SemiGroup.isComLaw [abbrev, in mathcomp.boot.bigop]
    SemiGroup.isComLaw [mod, in mathcomp.boot.bigop]
    SemiGroup.isComLaw.axioms [abbrev, in mathcomp.boot.bigop]
    SemiGroup.isComLaw.axioms_ [rec, in mathcomp.boot.bigop]
    SemiGroup.isComLaw.Build [abbrev, in mathcomp.boot.bigop]
    SemiGroup.isComLaw.Exports [mod, in mathcomp.boot.bigop]
    SemiGroup.isComLaw.opA [proj, in mathcomp.boot.bigop]
    SemiGroup.isComLaw.opC [proj, in mathcomp.boot.bigop]
    SemiGroup.isComLaw.phant_axioms [def, in mathcomp.boot.bigop]
    SemiGroup.isComLaw.phant_Build [def, in mathcomp.boot.bigop]
    SemiGroup.isCommutativeLaw [abbrev, in mathcomp.boot.bigop]
    SemiGroup.isCommutativeLaw [mod, in mathcomp.boot.bigop]
    SemiGroup.isCommutativeLaw.axioms [abbrev, in mathcomp.boot.bigop]
    SemiGroup.isCommutativeLaw.axioms_ [rec, in mathcomp.boot.bigop]
    SemiGroup.isCommutativeLaw.Build [abbrev, in mathcomp.boot.bigop]
    SemiGroup.isCommutativeLaw.Exports [mod, in mathcomp.boot.bigop]
    SemiGroup.isCommutativeLaw.identity_builder [def, in mathcomp.boot.bigop]
    SemiGroup.isCommutativeLaw.opC [proj, in mathcomp.boot.bigop]
    SemiGroup.isCommutativeLaw.phant_axioms [def, in mathcomp.boot.bigop]
    SemiGroup.isCommutativeLaw.phant_Build [def, in mathcomp.boot.bigop]
    SemiGroup.isLaw [abbrev, in mathcomp.boot.bigop]
    SemiGroup.isLaw [mod, in mathcomp.boot.bigop]
    SemiGroup.isLaw.axioms [abbrev, in mathcomp.boot.bigop]
    SemiGroup.isLaw.axioms_ [rec, in mathcomp.boot.bigop]
    SemiGroup.isLaw.Build [abbrev, in mathcomp.boot.bigop]
    SemiGroup.isLaw.Exports [mod, in mathcomp.boot.bigop]
    SemiGroup.isLaw.identity_builder [def, in mathcomp.boot.bigop]
    SemiGroup.isLaw.opA [proj, in mathcomp.boot.bigop]
    SemiGroup.isLaw.phant_axioms [def, in mathcomp.boot.bigop]
    SemiGroup.isLaw.phant_Build [def, in mathcomp.boot.bigop]
    SemiGroup.law [abbrev, in mathcomp.boot.bigop]
    SemiGroup.Law [abbrev, in mathcomp.boot.bigop]
    SemiGroup.Law [mod, in mathcomp.boot.bigop]
    SemiGroup.Law.axioms_ [rec, in mathcomp.boot.bigop]
    SemiGroup.Law.class [proj, in mathcomp.boot.bigop]
    SemiGroup.Law.clone [abbrev, in mathcomp.boot.bigop]
    SemiGroup.Law.copy [abbrev, in mathcomp.boot.bigop]
    SemiGroup.Law.Exports [mod, in mathcomp.boot.bigop]
    SemiGroup.Law.on [abbrev, in mathcomp.boot.bigop]
    SemiGroup.Law.on_ [abbrev, in mathcomp.boot.bigop]
    SemiGroup.Law.pack_ [def, in mathcomp.boot.bigop]
    SemiGroup.Law.phant_clone [def, in mathcomp.boot.bigop]
    SemiGroup.Law.phant_on_ [def, in mathcomp.boot.bigop]
    SemiGroup.Law.SemiGroup_isLaw_mixin [proj, in mathcomp.boot.bigop]
    SemiGroup.Law.sort [proj, in mathcomp.boot.bigop]
    SemiGroup.Law.type [rec, in mathcomp.boot.bigop]
    SemiGroup.LawElpiOperations [mod, in mathcomp.boot.bigop]
    Semigroup.monoid_hasMul_mixin [proj, in mathcomp.boot.monoid]
    Semigroup.monoid_Magma_isSemigroup_mixin [proj, in mathcomp.boot.monoid]
    Semigroup.on [abbrev, in mathcomp.boot.monoid]
    Semigroup.on_ [abbrev, in mathcomp.boot.monoid]
    SemiGroup.opA [def, in mathcomp.boot.bigop]
    SemiGroup.opC [def, in mathcomp.boot.bigop]
    Semigroup.pack_ [def, in mathcomp.boot.monoid]
    Semigroup.phant_clone [def, in mathcomp.boot.monoid]
    Semigroup.phant_on_ [def, in mathcomp.boot.monoid]
    Semigroup.sort [proj, in mathcomp.boot.monoid]
    SemiGroup.Theory [mod, in mathcomp.boot.bigop]
    SemiGroup.Theory.mulmA [prf, in mathcomp.boot.bigop]
    SemiGroup.Theory.mulmAC [prf, in mathcomp.boot.bigop]
    SemiGroup.Theory.mulmACA [prf, in mathcomp.boot.bigop]
    SemiGroup.Theory.mulmC [prf, in mathcomp.boot.bigop]
    SemiGroup.Theory.mulmCA [prf, in mathcomp.boot.bigop]
    Semigroup.type [rec, in mathcomp.boot.monoid]
    Semigroup_isMonoid [abbrev, in mathcomp.boot.monoid]
    Semigroup_isMonoid [mod, in mathcomp.boot.monoid]
    Semigroup_isMonoid.axioms [abbrev, in mathcomp.boot.monoid]
    Semigroup_isMonoid.axioms_ [rec, in mathcomp.boot.monoid]
    Semigroup_isMonoid.Build [abbrev, in mathcomp.boot.monoid]
    Semigroup_isMonoid.Exports [mod, in mathcomp.boot.monoid]
    Semigroup_isMonoid.mul1g [proj, in mathcomp.boot.monoid]
    Semigroup_isMonoid.mulg1 [proj, in mathcomp.boot.monoid]
    Semigroup_isMonoid.one [proj, in mathcomp.boot.monoid]
    Semigroup_isMonoid.phant_axioms [def, in mathcomp.boot.monoid]
    Semigroup_isMonoid.phant_Build [def, in mathcomp.boot.monoid]
    SemigroupElpiOperations [mod, in mathcomp.boot.monoid]
    semiprime [def, in mathcomp.solvable.frobenius]
    semiprime_regular [prf, in mathcomp.solvable.frobenius]
    semiprimeJ [prf, in mathcomp.solvable.frobenius]
    semiprimeS [prf, in mathcomp.solvable.frobenius]
    semiregular [def, in mathcomp.solvable.frobenius]
    semiregular1l [prf, in mathcomp.solvable.frobenius]
    semiregular1r [prf, in mathcomp.solvable.frobenius]
    semiregular_prime [prf, in mathcomp.solvable.frobenius]
    semiregular_sym [prf, in mathcomp.solvable.frobenius]
    semiregularJ [prf, in mathcomp.solvable.frobenius]
    semiregularS [prf, in mathcomp.solvable.frobenius]
    semiring_sigma_additive [prf, in mathcomp.analysis.measure_theory.measure_function]
    SemiRingOfSets [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
    SemiRingOfSets [mod, in mathcomp.analysis.measure_theory.measurable_structure]
    SemiRingOfSets.axioms_ [rec, in mathcomp.analysis.measure_theory.measurable_structure]
    SemiRingOfSets.choice_hasChoice_mixin [proj, in mathcomp.analysis.measure_theory.measurable_structure]
    SemiRingOfSets.class [proj, in mathcomp.analysis.measure_theory.measurable_structure]
    SemiRingOfSets.classical_sets_isPointed_mixin [proj, in mathcomp.analysis.measure_theory.measurable_structure]
    SemiRingOfSets.clone [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
    SemiRingOfSets.copy [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
    SemiRingOfSets.eqtype_hasDecEq_mixin [proj, in mathcomp.analysis.measure_theory.measurable_structure]
    SemiRingOfSets.Exports [mod, in mathcomp.analysis.measure_theory.measurable_structure]
    SemiRingOfSets.Exports.semiRingOfSetsType [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
    SemiRingOfSets.measurable_structure_isSemiRingOfSets_mixin [proj, in mathcomp.analysis.measure_theory.measurable_structure]
    SemiRingOfSets.on [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
    SemiRingOfSets.on_ [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
    SemiRingOfSets.pack_ [def, in mathcomp.analysis.measure_theory.measurable_structure]
    SemiRingOfSets.phant_clone [def, in mathcomp.analysis.measure_theory.measurable_structure]
    SemiRingOfSets.phant_on_ [def, in mathcomp.analysis.measure_theory.measurable_structure]
    SemiRingOfSets.sort [proj, in mathcomp.analysis.measure_theory.measurable_structure]
    SemiRingOfSets.type [rec, in mathcomp.analysis.measure_theory.measurable_structure]
    SemiRingOfSets_isRingOfSets [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
    SemiRingOfSets_isRingOfSets [mod, in mathcomp.analysis.measure_theory.measurable_structure]
    SemiRingOfSets_isRingOfSets.axioms [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
    SemiRingOfSets_isRingOfSets.axioms_ [rec, in mathcomp.analysis.measure_theory.measurable_structure]
    SemiRingOfSets_isRingOfSets.Build [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
    SemiRingOfSets_isRingOfSets.Exports [mod, in mathcomp.analysis.measure_theory.measurable_structure]
    SemiRingOfSets_isRingOfSets.identity_builder [def, in mathcomp.analysis.measure_theory.measurable_structure]
    SemiRingOfSets_isRingOfSets.measurableU [proj, in mathcomp.analysis.measure_theory.measurable_structure]
    SemiRingOfSets_isRingOfSets.phant_axioms [def, in mathcomp.analysis.measure_theory.measurable_structure]
    SemiRingOfSets_isRingOfSets.phant_Build [def, in mathcomp.analysis.measure_theory.measurable_structure]
    SemiRingOfSetsElpiOperations [mod, in mathcomp.analysis.measure_theory.measurable_structure]
    semiRingType [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
    SemiVector [abbrev, in mathcomp.algebra.vector]
    SemiVector [mod, in mathcomp.algebra.vector]
    SemiVector.Algebra_AddMagma_isAddSemigroup_mixin [proj, in mathcomp.algebra.vector]
    SemiVector.Algebra_BaseAddMagma_isAddMagma_mixin [proj, in mathcomp.algebra.vector]
    SemiVector.Algebra_BaseAddUMagma_isAddUMagma_mixin [proj, in mathcomp.algebra.vector]
    SemiVector.Algebra_hasAdd_mixin [proj, in mathcomp.algebra.vector]
    SemiVector.Algebra_hasZero_mixin [proj, in mathcomp.algebra.vector]
    SemiVector.axioms_ [rec, in mathcomp.algebra.vector]
    SemiVector.choice_hasChoice_mixin [proj, in mathcomp.algebra.vector]
    SemiVector.class [proj, in mathcomp.algebra.vector]
    SemiVector.clone [abbrev, in mathcomp.algebra.vector]
    SemiVector.copy [abbrev, in mathcomp.algebra.vector]
    SemiVector.eqtype_hasDecEq_mixin [proj, in mathcomp.algebra.vector]
    SemiVector.Exports [mod, in mathcomp.algebra.vector]
    SemiVector.Exports.semiVectType [abbrev, in mathcomp.algebra.vector]
    SemiVector.GRing_Nmodule_isLSemiModule_mixin [proj, in mathcomp.algebra.vector]
    SemiVector.on [abbrev, in mathcomp.algebra.vector]
    SemiVector.on_ [abbrev, in mathcomp.algebra.vector]
    SemiVector.pack_ [def, in mathcomp.algebra.vector]
    SemiVector.phant_clone [def, in mathcomp.algebra.vector]
    SemiVector.phant_on_ [def, in mathcomp.algebra.vector]
    SemiVector.sort [proj, in mathcomp.algebra.vector]
    SemiVector.type [rec, in mathcomp.algebra.vector]
    SemiVector.vector_LSemiModule_hasFinDim_mixin [proj, in mathcomp.algebra.vector]
    semivector_axiom_def [rec, in mathcomp.algebra.vector]
    SemiVector_isProper [abbrev, in mathcomp.algebra.vector]
    SemiVector_isProper [mod, in mathcomp.algebra.vector]
    SemiVector_isProper.axioms [abbrev, in mathcomp.algebra.vector]
    SemiVector_isProper.axioms_ [rec, in mathcomp.algebra.vector]
    SemiVector_isProper.Build [abbrev, in mathcomp.algebra.vector]
    SemiVector_isProper.dim_gt0 [proj, in mathcomp.algebra.vector]
    SemiVector_isProper.Exports [mod, in mathcomp.algebra.vector]
    SemiVector_isProper.identity_builder [def, in mathcomp.algebra.vector]
    SemiVector_isProper.phant_axioms [def, in mathcomp.algebra.vector]
    SemiVector_isProper.phant_Build [def, in mathcomp.algebra.vector]
    SemiVectorElpiOperations [mod, in mathcomp.algebra.vector]
    separable [file, in mathcomp.field.separable]
    separable [def, in mathcomp.field.separable]
    separable [abbrev, in mathcomp.field.separable]
    separable_add [prf, in mathcomp.field.separable]
    separable_coprime [prf, in mathcomp.field.separable]
    separable_deriv_eq0 [prf, in mathcomp.field.separable]
    separable_element [def, in mathcomp.field.separable]
    separable_elementP [prf, in mathcomp.field.separable]
    separable_elementS [prf, in mathcomp.field.separable]
    separable_exponent [abbrev, in mathcomp.field.separable]
    separable_exponent_pchar [prf, in mathcomp.field.separable]
    separable_Fadjoin_seq [prf, in mathcomp.field.separable]
    separable_generator [def, in mathcomp.field.separable]
    separable_generator_maximal [prf, in mathcomp.field.separable]
    separable_generator_mem [prf, in mathcomp.field.separable]
    separable_generatorP [prf, in mathcomp.field.separable]
    separable_inseparable_decomposition [prf, in mathcomp.field.separable]
    separable_inseparable_element [prf, in mathcomp.field.separable]
    separable_map [prf, in mathcomp.field.separable]
    separable_mul [prf, in mathcomp.field.separable]
    separable_nosquare [prf, in mathcomp.field.separable]
    separable_nz_der [prf, in mathcomp.field.separable]
    separable_poly [abbrev, in mathcomp.field.separable]
    separable_poly [mod, in mathcomp.field.separable]
    separable_poly.body [def, in mathcomp.field.separable]
    separable_poly.unlock [def, in mathcomp.field.separable]
    separable_poly_Locked [modtype, in mathcomp.field.separable]
    separable_poly_Locked.body [ax, in mathcomp.field.separable]
    separable_poly_Locked.unlock [ax, in mathcomp.field.separable]
    separable_poly_neq0 [prf, in mathcomp.field.separable]
    separable_poly_unlock_subterm [def, in mathcomp.field.separable]
    separable_poly_unlockable [def, in mathcomp.field.separable]
    separable_polyP [prf, in mathcomp.field.separable]
    separable_prod_XsubC [prf, in mathcomp.field.separable]
    separable_refl [prf, in mathcomp.field.separable]
    separable_root [prf, in mathcomp.field.separable]
    separable_root_der [prf, in mathcomp.field.separable]
    separable_sum [prf, in mathcomp.field.separable]
    separable_trans [prf, in mathcomp.field.separable]
    separable_Xn_sub_1 [prf, in mathcomp.field.cyclotomic]
    separableP [prf, in mathcomp.field.separable]
    separablePn [abbrev, in mathcomp.field.separable]
    separablePn_pchar [prf, in mathcomp.field.separable]
    separableS [prf, in mathcomp.field.separable]
    separableSl [prf, in mathcomp.field.separable]
    separableSr [prf, in mathcomp.field.separable]
    separate_points_from_closed [def, in mathcomp.analysis.topology_theory.function_spaces]
    separated [def, in mathcomp.analysis.topology_theory.connected]
    separated_closed_ball_countable [prf, in mathcomp.analysis.normedtype_theory.vitali_lemma]
    separated_disjoint [prf, in mathcomp.analysis.topology_theory.connected]
    separated_open_countable [prf, in mathcomp.analysis.topology_theory.num_topology]
    separatedC [prf, in mathcomp.analysis.topology_theory.connected]
    separation_axioms [file, in mathcomp.analysis.topology_theory.separation_axioms]
    seq [file, in mathcomp.boot.seq]
    seq [abbrev, in mathcomp.boot.seq]
    seq1_basis [prf, in mathcomp.algebra.vector]
    seq1_free [prf, in mathcomp.algebra.vector]
    seq_eqclass [def, in mathcomp.boot.seq]
    seq_finpredType [def, in mathcomp.finmap.finmap]
    seq_fset [abbrev, in mathcomp.finmap.finmap]
    seq_fset [abbrev, in mathcomp.finmap.finmap]
    seq_fset [mod, in mathcomp.finmap.finmap]
    seq_fset.body [def, in mathcomp.finmap.finmap]
    seq_fset.unlock [def, in mathcomp.finmap.finmap]
    seq_fset_Locked [modtype, in mathcomp.finmap.finmap]
    seq_fset_Locked.body [ax, in mathcomp.finmap.finmap]
    seq_fset_Locked.unlock [ax, in mathcomp.finmap.finmap]
    seq_fset_perm [prf, in mathcomp.finmap.finmap]
    seq_fset_uniq [prf, in mathcomp.finmap.finmap]
    seq_fset_unlock_subterm [def, in mathcomp.finmap.finmap]
    seq_fsetE [prf, in mathcomp.finmap.finmap]
    seq_hasChoice [prf, in mathcomp.boot.choice]
    seq_ind2 [prf, in mathcomp.boot.seq]
    seq_iso3_L [def, in mathcomp.solvable.burnside_app]
    seq_iso_L [def, in mathcomp.solvable.burnside_app]
    seq_mset [def, in mathcomp.finmap.multiset]
    seq_mset_id [prf, in mathcomp.finmap.multiset]
    seq_mset_key [prf, in mathcomp.finmap.multiset]
    seq_of_is_finite [proj, in mathcomp.finmap.finmap]
    seq_of_opt [def, in mathcomp.boot.choice]
    seq_of_optK [prf, in mathcomp.boot.choice]
    seq_predType [def, in mathcomp.boot.seq]
    seq_psume_eq0 [prf, in mathcomp.reals.constructive_ereal]
    seq_sub [rec, in mathcomp.boot.fintype]
    seq_sub_axiom [prf, in mathcomp.boot.fintype]
    seq_sub_default [prf, in mathcomp.boot.fintype]
    seq_sub_enum [def, in mathcomp.boot.fintype]
    seq_sub_isCountable [def, in mathcomp.boot.fintype]
    seq_sub_isFinite [def, in mathcomp.boot.fintype]
    seq_sub_pickle [def, in mathcomp.boot.fintype]
    seq_sub_pickleK [prf, in mathcomp.boot.fintype]
    seq_sub_unpickle [def, in mathcomp.boot.fintype]
    seq_subE [prf, in mathcomp.boot.fintype]
    seq_tnthP [prf, in mathcomp.boot.tuple]
    seqD [def, in mathcomp.analysis.sequences]
    seqDU [def, in mathcomp.analysis.sequences]
    seqDU_bigcup_eq [prf, in mathcomp.analysis.sequences]
    seqDU_measurable [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    seqDU_seqD [prf, in mathcomp.analysis.sequences]
    seqDUE [prf, in mathcomp.analysis.sequences]
    seqDUIE [prf, in mathcomp.analysis.sequences]
    seqn [def, in mathcomp.boot.seq]
    seqn_rec [def, in mathcomp.boot.seq]
    seqn_type [def, in mathcomp.boot.seq]
    seqs1 [prf, in mathcomp.solvable.burnside_app]
    sequence [def, in mathcomp.analysis.sequences]
    sequences [file, in mathcomp.analysis.sequences]
    seqv_sub_adjoin [prf, in mathcomp.field.falgebra]
    series [def, in mathcomp.analysis.sequences]
    series_addn [prf, in mathcomp.analysis.sequences]
    series_cos_coeff0 [prf, in mathcomp.analysis.trigo]
    series_exp_coeff0 [prf, in mathcomp.analysis.sequences]
    series_le_cvg [prf, in mathcomp.analysis.sequences]
    series_sin_coeff0 [prf, in mathcomp.analysis.trigo]
    series_sol [prf, in mathcomp.solvable.nilpotent]
    seriesD [prf, in mathcomp.analysis.sequences]
    seriesEnat [prf, in mathcomp.analysis.sequences]
    seriesEord [prf, in mathcomp.analysis.sequences]
    seriesK [prf, in mathcomp.analysis.sequences]
    seriesN [prf, in mathcomp.analysis.sequences]
    seriesS [prf, in mathcomp.analysis.sequences]
    seriesSB [prf, in mathcomp.analysis.sequences]
    seriesSr [prf, in mathcomp.analysis.sequences]
    seriesZ [prf, in mathcomp.analysis.sequences]
    sesqui [def, in mathcomp.algebra.sesquilinear]
    sesqui_key [prf, in mathcomp.algebra.sesquilinear]
    sesqui_keyed [def, in mathcomp.algebra.sesquilinear]
    sesquiE [prf, in mathcomp.algebra.sesquilinear]
    sesquilinear [file, in mathcomp.algebra.sesquilinear]
    sesquiP [prf, in mathcomp.algebra.sesquilinear]
    set [def, in mathcomp.classical.classical_sets]
    set0 [def, in mathcomp.classical.classical_sets]
    set0 [def, in mathcomp.boot.finset]
    set0_Nexists [prf, in mathcomp.boot.finset]
    set0D [prf, in mathcomp.classical.classical_sets]
    set0D [prf, in mathcomp.boot.finset]
    set0fun [prf, in mathcomp.classical.classical_sets]
    set0fun_inj [prf, in mathcomp.classical.functions]
    set0I [prf, in mathcomp.classical.classical_sets]
    set0I [prf, in mathcomp.boot.finset]
    set0P [prf, in mathcomp.classical.classical_sets]
    set0Pn [prf, in mathcomp.boot.finset]
    set0U [prf, in mathcomp.classical.classical_sets]
    set0U [prf, in mathcomp.boot.finset]
    set0X [prf, in mathcomp.classical.classical_sets]
    set0Y [prf, in mathcomp.classical.classical_sets]
    set1 [def, in mathcomp.classical.classical_sets]
    set1 [abbrev, in mathcomp.boot.finset]
    set1 [mod, in mathcomp.boot.finset]
    set1.body [def, in mathcomp.boot.finset]
    set1.unlock [def, in mathcomp.boot.finset]
    set11 [prf, in mathcomp.boot.finset]
    set1_bigcap_oc [prf, in mathcomp.reals.real_interval]
    set1_group [def, in mathcomp.finite_group.fingroup]
    set1_inj [prf, in mathcomp.boot.finset]
    set1_Locked [modtype, in mathcomp.boot.finset]
    set1_Locked.body [ax, in mathcomp.boot.finset]
    set1_Locked.unlock [ax, in mathcomp.boot.finset]
    set1_unlock_subterm [def, in mathcomp.boot.finset]
    set1gE [prf, in mathcomp.finite_group.fingroup]
    set1gP [prf, in mathcomp.finite_group.fingroup]
    set1gXn [def, in mathcomp.finite_group.gproduct]
    set1gXn_commute [prf, in mathcomp.finite_group.gproduct]
    set1gXn_group_set [prf, in mathcomp.finite_group.gproduct]
    set1gXn_key [prf, in mathcomp.finite_group.gproduct]
    set1gXnE [prf, in mathcomp.finite_group.gproduct]
    set1gXnP [prf, in mathcomp.finite_group.gproduct]
    set1I [prf, in mathcomp.classical.classical_sets]
    set1K [prf, in mathcomp.boot.finset]
    set1P [prf, in mathcomp.boot.finset]
    set1Ul [prf, in mathcomp.boot.finset]
    set1Ur [prf, in mathcomp.boot.finset]
    set21 [prf, in mathcomp.boot.finset]
    set22 [prf, in mathcomp.boot.finset]
    set2P [prf, in mathcomp.boot.finset]
    set_0Vmem [prf, in mathcomp.boot.finset]
    set_action [def, in mathcomp.finite_group.action]
    set_andb [prf, in mathcomp.classical.classical_sets]
    set_base_group [def, in mathcomp.finite_group.fingroup]
    set_bij [def, in mathcomp.classical.functions]
    set_bij00 [prf, in mathcomp.classical.functions]
    set_bij_bijfun [def, in mathcomp.classical.functions]
    set_bij_comp [prf, in mathcomp.classical.functions]
    set_bij_homo [prf, in mathcomp.classical.functions]
    set_bij_inj [prf, in mathcomp.classical.functions]
    set_bij_sub [prf, in mathcomp.classical.functions]
    set_bij_surj [prf, in mathcomp.classical.functions]
    set_bool [prf, in mathcomp.classical.classical_sets]
    set_compose_diag [prf, in mathcomp.classical.classical_sets]
    set_compose_subset [prf, in mathcomp.classical.classical_sets]
    set_cons [prf, in mathcomp.boot.finset]
    set_cons1 [prf, in mathcomp.classical.classical_sets]
    set_cst [prf, in mathcomp.classical.classical_sets]
    set_display [prf, in mathcomp.classical.classical_sets]
    set_enum [prf, in mathcomp.boot.finset]
    set_eq_le [prf, in mathcomp.classical.classical_sets]
    set_false [prf, in mathcomp.classical.classical_sets]
    set_Frobenius_compl [prf, in mathcomp.solvable.frobenius]
    set_fset0 [prf, in mathcomp.classical.classical_sets]
    set_fset1 [prf, in mathcomp.classical.classical_sets]
    set_fset_eq0 [prf, in mathcomp.classical.classical_sets]
    set_fsetD [prf, in mathcomp.classical.classical_sets]
    set_fsetD1 [prf, in mathcomp.classical.classical_sets]
    set_fsetI [prf, in mathcomp.classical.classical_sets]
    set_fsetIr [prf, in mathcomp.classical.classical_sets]
    set_fsetK [prf, in mathcomp.classical.cardinality]
    set_fsetU [prf, in mathcomp.classical.classical_sets]
    set_fsetU1 [prf, in mathcomp.classical.classical_sets]
    set_fun [def, in mathcomp.classical.functions]
    set_fun_image [prf, in mathcomp.classical.functions]
    set_imfset [prf, in mathcomp.classical.classical_sets]
    set_inj [def, in mathcomp.classical.functions]
    set_interval [file, in mathcomp.classical.set_interval]
    set_invg [def, in mathcomp.finite_group.fingroup]
    set_invgK [prf, in mathcomp.finite_group.fingroup]
    set_invgM [prf, in mathcomp.finite_group.fingroup]
    set_isSub [def, in mathcomp.boot.finset]
    set_iterF_mono [prf, in mathcomp.finmap.finmap]
    set_iterF_sub [prf, in mathcomp.finmap.finmap]
    set_itv1 [prf, in mathcomp.classical.set_interval]
    set_itv_bnd_ninfty [abbrev, in mathcomp.classical.set_interval]
    set_itv_bndNy [prf, in mathcomp.classical.set_interval]
    set_itv_c_infty [abbrev, in mathcomp.classical.set_interval]
    set_itv_ge [prf, in mathcomp.classical.set_interval]
    set_itv_infty_c [abbrev, in mathcomp.classical.set_interval]
    set_itv_infty_infty [abbrev, in mathcomp.classical.set_interval]
    set_itv_infty_o [abbrev, in mathcomp.classical.set_interval]
    set_itv_infty_set0 [def, in mathcomp.classical.set_interval]
    set_itv_o_infty [abbrev, in mathcomp.classical.set_interval]
    set_itv_pinfty_bnd [abbrev, in mathcomp.classical.set_interval]
    set_itv_setT [prf, in mathcomp.analysis.normedtype_theory.normed_module]
    set_itv_splitD [prf, in mathcomp.classical.set_interval]
    set_itv_splitI [prf, in mathcomp.classical.set_interval]
    set_itv_splitU [prf, in mathcomp.classical.set_interval]
    set_itv_ybnd [prf, in mathcomp.classical.set_interval]
    set_itvcc [prf, in mathcomp.classical.set_interval]
    set_itvco [prf, in mathcomp.classical.set_interval]
    set_itvco0 [prf, in mathcomp.classical.set_interval]
    set_itvcy [prf, in mathcomp.classical.set_interval]
    set_itvE [def, in mathcomp.classical.set_interval]
    set_itvI [prf, in mathcomp.classical.set_interval]
    set_itvK [prf, in mathcomp.analysis.normedtype_theory.normed_module]
    set_itvNyc [prf, in mathcomp.classical.set_interval]
    set_itvNyo [prf, in mathcomp.classical.set_interval]
    set_itvNyy [prf, in mathcomp.classical.set_interval]
    set_itvoc [prf, in mathcomp.classical.set_interval]
    set_itvoc0 [prf, in mathcomp.classical.set_interval]
    set_itvoo [prf, in mathcomp.classical.set_interval]
    set_itvoo0 [prf, in mathcomp.classical.set_interval]
    set_itvoy [prf, in mathcomp.classical.set_interval]
    set_itvP [prf, in mathcomp.classical.set_interval]
    set_itvxx [prf, in mathcomp.classical.set_interval]
    set_last_default [prf, in mathcomp.boot.seq]
    set_lte_bigcup [prf, in mathcomp.reals.real_interval]
    set_mem [prf, in mathcomp.classical.classical_sets]
    set_mem_set [prf, in mathcomp.classical.classical_sets]
    set_memK [prf, in mathcomp.classical.classical_sets]
    set_mul1g [prf, in mathcomp.finite_group.fingroup]
    set_mulg [def, in mathcomp.finite_group.fingroup]
    set_mulgA [prf, in mathcomp.finite_group.fingroup]
    set_nbhs [def, in mathcomp.analysis.topology_theory.separation_axioms]
    set_nbhs_filter [inst, in mathcomp.analysis.topology_theory.separation_axioms]
    set_nbhs_pfilter [inst, in mathcomp.analysis.topology_theory.separation_axioms]
    set_nbhsP [prf, in mathcomp.analysis.topology_theory.separation_axioms]
    set_neq_lt [prf, in mathcomp.classical.classical_sets]
    set_nil [prf, in mathcomp.classical.classical_sets]
    set_nil [prf, in mathcomp.boot.finset]
    set_nth [def, in mathcomp.boot.seq]
    set_nth_default [prf, in mathcomp.boot.seq]
    set_nth_nil [prf, in mathcomp.boot.seq]
    set_nthE [prf, in mathcomp.boot.seq]
    set_of [def, in mathcomp.boot.finset]
    set_of_coset [proj, in mathcomp.finite_group.quotient]
    set_of_fset [def, in mathcomp.finmap.finmap]
    set_orb [prf, in mathcomp.classical.classical_sets]
    set_partition_big [prf, in mathcomp.boot.finset]
    set_partition_big_cond [prf, in mathcomp.boot.finset]
    set_predC [prf, in mathcomp.classical.classical_sets]
    set_predType [def, in mathcomp.classical.classical_sets]
    set_predType [def, in mathcomp.boot.finset]
    set_prod_invK [prf, in mathcomp.classical.classical_sets]
    set_seq1 [prf, in mathcomp.boot.finset]
    set_seq_eq0 [prf, in mathcomp.classical.classical_sets]
    set_set_nth [prf, in mathcomp.boot.seq]
    set_surj [def, in mathcomp.classical.functions]
    set_system [def, in mathcomp.classical.classical_sets]
    set_true [prf, in mathcomp.classical.classical_sets]
    set_type [def, in mathcomp.classical.classical_sets]
    set_type [ind, in mathcomp.boot.finset]
    set_type_ind [scheme, in mathcomp.boot.finset]
    set_type_rec [scheme, in mathcomp.boot.finset]
    set_type_rect [scheme, in mathcomp.boot.finset]
    set_type_sind [scheme, in mathcomp.boot.finset]
    set_unit [prf, in mathcomp.classical.classical_sets]
    set_val [def, in mathcomp.classical.functions]
    set_valE [prf, in mathcomp.classical.functions]
    set_valP [prf, in mathcomp.classical.classical_sets]
    setact [def, in mathcomp.finite_group.action]
    setact_is_action [prf, in mathcomp.finite_group.action]
    setact_orbit [prf, in mathcomp.finite_group.action]
    setactE [prf, in mathcomp.finite_group.action]
    setactJ [prf, in mathcomp.finite_group.action]
    setactVin [prf, in mathcomp.finite_group.action]
    setC [def, in mathcomp.classical.classical_sets]
    setC [def, in mathcomp.boot.finset]
    setC0 [prf, in mathcomp.classical.classical_sets]
    setC0 [prf, in mathcomp.boot.finset]
    setC11 [prf, in mathcomp.boot.finset]
    setC_bigcap [prf, in mathcomp.classical.classical_sets]
    setC_bigcap [prf, in mathcomp.boot.finset]
    setC_bigcup [prf, in mathcomp.classical.classical_sets]
    setC_bigcup [prf, in mathcomp.boot.finset]
    setC_bigsetI [prf, in mathcomp.classical.classical_sets]
    setC_bigsetU [prf, in mathcomp.classical.classical_sets]
    setC_closed [def, in mathcomp.analysis.measure_theory.measurable_structure]
    setC_I [prf, in mathcomp.classical.classical_sets]
    setC_inj [def, in mathcomp.classical.classical_sets]
    setC_inj [prf, in mathcomp.boot.finset]
    setCD [prf, in mathcomp.classical.classical_sets]
    setCD [prf, in mathcomp.boot.finset]
    setCI [prf, in mathcomp.classical.classical_sets]
    setCI [prf, in mathcomp.boot.finset]
    setCitv [prf, in mathcomp.classical.set_interval]
    setCitvl [prf, in mathcomp.classical.set_interval]
    setCitvr [prf, in mathcomp.classical.set_interval]
    setCK [prf, in mathcomp.classical.classical_sets]
    setCK [prf, in mathcomp.boot.finset]
    setCP [prf, in mathcomp.boot.finset]
    setCS [prf, in mathcomp.classical.classical_sets]
    setCS [prf, in mathcomp.boot.finset]
    setCT [prf, in mathcomp.classical.classical_sets]
    setCT [prf, in mathcomp.boot.finset]
    setCU [prf, in mathcomp.classical.classical_sets]
    setCU [prf, in mathcomp.boot.finset]
    setCU_Efin [prf, in mathcomp.analysis.measurable_realfun]
    setCYT [prf, in mathcomp.classical.classical_sets]
    setD [def, in mathcomp.classical.classical_sets]
    setD [def, in mathcomp.boot.finset]
    setD0 [prf, in mathcomp.classical.classical_sets]
    setD0 [prf, in mathcomp.boot.finset]
    setD11 [prf, in mathcomp.boot.finset]
    setD1K [prf, in mathcomp.classical.classical_sets]
    setD1K [prf, in mathcomp.boot.finset]
    setD1P [prf, in mathcomp.boot.finset]
    setD_bigcup [prf, in mathcomp.classical.classical_sets]
    setD_bigcupl [prf, in mathcomp.classical.classical_sets]
    setD_bndc_Nybnd [prf, in mathcomp.classical.set_interval]
    setD_cbnd_bndy [prf, in mathcomp.classical.set_interval]
    setD_closed [def, in mathcomp.analysis.measure_theory.measurable_structure]
    setD_closedP [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    setD_eq0 [prf, in mathcomp.finmap.multiset]
    setD_eq0 [prf, in mathcomp.classical.classical_sets]
    setD_eq0 [prf, in mathcomp.boot.finset]
    setD_semi_setD_closed [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    setDccitv [prf, in mathcomp.classical.set_interval]
    setDD [prf, in mathcomp.classical.classical_sets]
    setDDl [prf, in mathcomp.classical.classical_sets]
    setDDl [prf, in mathcomp.boot.finset]
    setDDr [prf, in mathcomp.classical.classical_sets]
    setDDr [prf, in mathcomp.boot.finset]
    setDE [prf, in mathcomp.classical.classical_sets]
    setDE [prf, in mathcomp.boot.finset]
    setDI_closed [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
    setDI_semi_setD_closed [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
    setDidl [prf, in mathcomp.classical.classical_sets]
    setDidPl [prf, in mathcomp.classical.classical_sets]
    setDidPl [prf, in mathcomp.boot.finset]
    setDIK [prf, in mathcomp.classical.classical_sets]
    setDIl [prf, in mathcomp.boot.finset]
    setDIr [prf, in mathcomp.classical.classical_sets]
    setDIr [prf, in mathcomp.boot.finset]
    setDitv1l [prf, in mathcomp.classical.set_interval]
    setDitv1r [prf, in mathcomp.classical.set_interval]
    setDitv_set2 [prf, in mathcomp.classical.set_interval]
    setDitvNyo [prf, in mathcomp.classical.set_interval]
    setDitvoo [prf, in mathcomp.classical.set_interval]
    setDitvoy [prf, in mathcomp.classical.set_interval]
    setDKI [prf, in mathcomp.classical.classical_sets]
    setDKU [prf, in mathcomp.classical.classical_sets]
    setDP [prf, in mathcomp.boot.finset]
    setDS [prf, in mathcomp.classical.classical_sets]
    setDS [prf, in mathcomp.boot.finset]
    setDSS [prf, in mathcomp.classical.classical_sets]
    setDSS [prf, in mathcomp.boot.finset]
    setDT [prf, in mathcomp.classical.classical_sets]
    setDT [prf, in mathcomp.boot.finset]
    setDU [prf, in mathcomp.classical.classical_sets]
    setDUD [prf, in mathcomp.classical.classical_sets]
    setDUK [prf, in mathcomp.classical.classical_sets]
    setDUl [prf, in mathcomp.classical.classical_sets]
    setDUl [prf, in mathcomp.boot.finset]
    setDUr [prf, in mathcomp.classical.classical_sets]
    setDUr [prf, in mathcomp.boot.finset]
    setDv [prf, in mathcomp.classical.classical_sets]
    setDv [prf, in mathcomp.boot.finset]
    seteqfun [def, in mathcomp.classical.functions]
    seteqP [prf, in mathcomp.classical.classical_sets]
    setf [def, in mathcomp.finmap.finmap]
    setf_catl [prf, in mathcomp.finmap.finmap]
    setf_catr [prf, in mathcomp.finmap.finmap]
    setF_eq0 [prf, in mathcomp.classical.classical_sets]
    setf_get [prf, in mathcomp.finmap.finmap]
    setf_inj [prf, in mathcomp.finmap.finmap]
    setf_rem [prf, in mathcomp.finmap.finmap]
    setf_rem1 [prf, in mathcomp.finmap.finmap]
    setf_restrict [prf, in mathcomp.finmap.finmap]
    setfC [prf, in mathcomp.finmap.finmap]
    setfK [prf, in mathcomp.finmap.finmap]
    setfNK [prf, in mathcomp.finmap.finmap]
    setI [def, in mathcomp.classical.classical_sets]
    setI [def, in mathcomp.boot.finset]
    setI0 [prf, in mathcomp.classical.classical_sets]
    setI0 [prf, in mathcomp.boot.finset]
    setI1 [prf, in mathcomp.classical.classical_sets]
    setI1g [prf, in mathcomp.finite_group.fingroup]
    setI_bigcupl [prf, in mathcomp.classical.classical_sets]
    setI_bigcupr [prf, in mathcomp.classical.classical_sets]
    setI_closed [def, in mathcomp.classical.classical_sets]
    setI_closed_g_dynkin_g_sigma_algebra [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    setI_eq0 [prf, in mathcomp.boot.finset]
    setI_g_sigma_ring [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    setI_group [def, in mathcomp.finite_group.fingroup]
    setI_II [prf, in mathcomp.classical.classical_sets]
    setI_im_cpair [prf, in mathcomp.solvable.center]
    setI_normal_Hall [prf, in mathcomp.solvable.pgroup]
    setI_powerset [prf, in mathcomp.boot.finset]
    setI_subnormal [prf, in mathcomp.solvable.gseries]
    setI_transversal_pblock [prf, in mathcomp.boot.finset]
    setIA [prf, in mathcomp.classical.classical_sets]
    setIA [prf, in mathcomp.boot.finset]
    setIAC [prf, in mathcomp.classical.classical_sets]
    setIAC [prf, in mathcomp.boot.finset]
    setIACA [prf, in mathcomp.classical.classical_sets]
    setIACA [prf, in mathcomp.boot.finset]
    setIC [prf, in mathcomp.classical.classical_sets]
    setIC [prf, in mathcomp.boot.finset]
    setICA [prf, in mathcomp.classical.classical_sets]
    setICA [prf, in mathcomp.boot.finset]
    setICK [prf, in mathcomp.classical.classical_sets]
    setICl [prf, in mathcomp.classical.classical_sets]
    setICr [prf, in mathcomp.classical.classical_sets]
    setICr [prf, in mathcomp.boot.finset]
    setID [prf, in mathcomp.boot.finset]
    setId2P [prf, in mathcomp.boot.finset]
    setIDA [prf, in mathcomp.classical.classical_sets]
    setIDA [prf, in mathcomp.boot.finset]
    setIDAC [prf, in mathcomp.classical.classical_sets]
    setIDAC [prf, in mathcomp.boot.finset]
    setIdE [prf, in mathcomp.boot.finset]
    setIdP [prf, in mathcomp.boot.finset]
    setIg1 [prf, in mathcomp.finite_group.fingroup]
    setIid [prf, in mathcomp.classical.classical_sets]
    setIid [prf, in mathcomp.boot.finset]
    setIidl [prf, in mathcomp.classical.classical_sets]
    setIidPl [prf, in mathcomp.classical.classical_sets]
    setIidPl [prf, in mathcomp.boot.finset]
    setIidPr [prf, in mathcomp.classical.classical_sets]
    setIidPr [prf, in mathcomp.boot.finset]
    setIidr [prf, in mathcomp.classical.classical_sets]
    setIIl [prf, in mathcomp.classical.classical_sets]
    setIIl [prf, in mathcomp.boot.finset]
    setIIr [prf, in mathcomp.classical.classical_sets]
    setIIr [prf, in mathcomp.boot.finset]
    setIK [prf, in mathcomp.classical.classical_sets]
    setIK [prf, in mathcomp.boot.finset]
    setIKC [prf, in mathcomp.classical.classical_sets]
    setIP [prf, in mathcomp.boot.finset]
    setIS [prf, in mathcomp.classical.classical_sets]
    setIS [prf, in mathcomp.boot.finset]
    setISS [prf, in mathcomp.classical.classical_sets]
    setISS [prf, in mathcomp.boot.finset]
    setIT [prf, in mathcomp.classical.classical_sets]
    setIT [prf, in mathcomp.boot.finset]
    setitv0 [prf, in mathcomp.classical.set_interval]
    setIUl [prf, in mathcomp.classical.classical_sets]
    setIUl [prf, in mathcomp.boot.finset]
    setIUr [prf, in mathcomp.classical.classical_sets]
    setIUr [prf, in mathcomp.boot.finset]
    setIYl [prf, in mathcomp.classical.classical_sets]
    setIYr [prf, in mathcomp.classical.classical_sets]
    setKI [prf, in mathcomp.classical.classical_sets]
    setKI [prf, in mathcomp.boot.finset]
    setKU [prf, in mathcomp.classical.classical_sets]
    setKU [prf, in mathcomp.boot.finset]
    setNK [prf, in mathcomp.classical.set_interval]
    SetOrder [mod, in mathcomp.classical.classical_sets]
    SetOrder.Exports [mod, in mathcomp.classical.classical_sets]
    SetOrder.Exports.botEset [prf, in mathcomp.classical.classical_sets]
    SetOrder.Exports.complEset [prf, in mathcomp.classical.classical_sets]
    SetOrder.Exports.joinEset [prf, in mathcomp.classical.classical_sets]
    SetOrder.Exports.meetEset [prf, in mathcomp.classical.classical_sets]
    SetOrder.Exports.properEset [prf, in mathcomp.classical.classical_sets]
    SetOrder.Exports.properPset [prf, in mathcomp.classical.classical_sets]
    SetOrder.Exports.subEset [prf, in mathcomp.classical.classical_sets]
    SetOrder.Exports.subsetEset [prf, in mathcomp.classical.classical_sets]
    SetOrder.Exports.subsetPset [prf, in mathcomp.classical.classical_sets]
    SetOrder.Exports.topEset [prf, in mathcomp.classical.classical_sets]
    SetOrder.Internal [mod, in mathcomp.classical.classical_sets]
    SetOrder.Internal.Exports [mod, in mathcomp.classical.classical_sets]
    SetOrder.Internal.joinIB [prf, in mathcomp.classical.classical_sets]
    SetOrder.Internal.joinKI [prf, in mathcomp.classical.classical_sets]
    SetOrder.Internal.le_def [prf, in mathcomp.classical.classical_sets]
    SetOrder.Internal.lt_def [prf, in mathcomp.classical.classical_sets]
    SetOrder.Internal.meetKU [prf, in mathcomp.classical.classical_sets]
    SetOrder.Internal.SetOrder_setTsub [prf, in mathcomp.classical.classical_sets]
    SetOrder.Internal.SetOrder_sub0set [prf, in mathcomp.classical.classical_sets]
    SetOrder.Internal.subKI [prf, in mathcomp.classical.classical_sets]
    setP [prf, in mathcomp.boot.finset]
    SetRing [mod, in mathcomp.analysis.measure_theory.measure_function]
    setring [def, in mathcomp.analysis.measure_theory.measurable_structure]
    SetRing.all_decomp_neq0 [prf, in mathcomp.analysis.measure_theory.measure_function]
    SetRing.cover_decomp [prf, in mathcomp.analysis.measure_theory.measure_function]
    SetRing.decomp [def, in mathcomp.analysis.measure_theory.measure_function]
    SetRing.decomp_finite_set [prf, in mathcomp.analysis.measure_theory.measure_function]
    SetRing.decomp_measurable [prf, in mathcomp.analysis.measure_theory.measure_function]
    SetRing.decomp_neq0 [prf, in mathcomp.analysis.measure_theory.measure_function]
    SetRing.decomp_set0 [prf, in mathcomp.analysis.measure_theory.measure_function]
    SetRing.decomp_sub [prf, in mathcomp.analysis.measure_theory.measure_function]
    SetRing.decomp_triv [prf, in mathcomp.analysis.measure_theory.measure_function]
    SetRing.decompN0 [prf, in mathcomp.analysis.measure_theory.measure_function]
    SetRing.display [def, in mathcomp.analysis.measure_theory.measure_function]
    SetRing.Exports [mod, in mathcomp.analysis.measure_theory.measure_function]
    SetRing.measurable_fin_trivIset [def, in mathcomp.analysis.measure_theory.measure_function]
    SetRing.measurable_subring [prf, in mathcomp.analysis.measure_theory.measure_function]
    SetRing.measure [def, in mathcomp.analysis.measure_theory.measure_function]
    SetRing.ring_finite_set [prf, in mathcomp.analysis.measure_theory.measure_function]
    SetRing.ring_measurableE [prf, in mathcomp.analysis.measure_theory.measure_function]
    SetRing.Rmu [abbrev, in mathcomp.analysis.measure_theory.measure_function]
    SetRing.Rmu_additive [prf, in mathcomp.analysis.measure_theory.measure_function]
    SetRing.Rmu_fin_bigcup [prf, in mathcomp.analysis.measure_theory.measure_function]
    SetRing.Rmu_ge0 [prf, in mathcomp.analysis.measure_theory.measure_function]
    SetRing.RmuE [prf, in mathcomp.analysis.measure_theory.measure_function]
    SetRing.rT [abbrev, in mathcomp.analysis.measure_theory.measure_function]
    SetRing.type [def, in mathcomp.analysis.measure_theory.measure_function]
    setring0 [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    setring_fin_bigcup [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    setring_id [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    setring_monotone_sigma_ring [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    setringD [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    setringDI [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
    setringU [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    setSD [prf, in mathcomp.classical.classical_sets]
    setSD [prf, in mathcomp.boot.finset]
    setSD_closed [def, in mathcomp.analysis.measure_theory.measurable_structure]
    setSI [prf, in mathcomp.classical.classical_sets]
    setSI [prf, in mathcomp.boot.finset]
    setSU [prf, in mathcomp.classical.classical_sets]
    setSU [prf, in mathcomp.boot.finset]
    setSX [prf, in mathcomp.classical.classical_sets]
    setT [def, in mathcomp.classical.classical_sets]
    setT [abbrev, in mathcomp.boot.finset]
    setT0 [prf, in mathcomp.classical.classical_sets]
    setT_bool [prf, in mathcomp.classical.classical_sets]
    setT_group [def, in mathcomp.finite_group.fingroup]
    setT_unit [prf, in mathcomp.classical.classical_sets]
    setTbij [def, in mathcomp.classical.functions]
    setTD [prf, in mathcomp.classical.classical_sets]
    setTD [prf, in mathcomp.boot.finset]
    setTfor [def, in mathcomp.boot.finset]
    setTI [prf, in mathcomp.classical.classical_sets]
    setTI [prf, in mathcomp.boot.finset]
    setTP [abbrev, in mathcomp.classical.classical_sets]
    setTPn [prf, in mathcomp.classical.classical_sets]
    setTT_bijective [prf, in mathcomp.classical.functions]
    setTU [prf, in mathcomp.classical.classical_sets]
    setTU [prf, in mathcomp.boot.finset]
    setTX [prf, in mathcomp.classical.classical_sets]
    setTYC [prf, in mathcomp.classical.classical_sets]
    setU [def, in mathcomp.classical.classical_sets]
    setU [def, in mathcomp.boot.finset]
    setU0 [prf, in mathcomp.classical.classical_sets]
    setU0 [prf, in mathcomp.boot.finset]
    setU11 [prf, in mathcomp.boot.finset]
    setU1itv [prf, in mathcomp.classical.set_interval]
    setU1K [prf, in mathcomp.boot.finset]
    setU1P [prf, in mathcomp.boot.finset]
    setU1r [prf, in mathcomp.boot.finset]
    setU_bigcapl [prf, in mathcomp.classical.classical_sets]
    setU_bigcapr [prf, in mathcomp.classical.classical_sets]
    setU_closed [def, in mathcomp.classical.classical_sets]
    setU_eq0 [prf, in mathcomp.classical.classical_sets]
    setU_eq0 [prf, in mathcomp.boot.finset]
    setU_id2r [prf, in mathcomp.classical.classical_sets]
    setU_II [prf, in mathcomp.classical.classical_sets]
    setU_seqD [prf, in mathcomp.analysis.sequences]
    setUA [prf, in mathcomp.classical.classical_sets]
    setUA [prf, in mathcomp.boot.finset]
    setUAC [prf, in mathcomp.classical.classical_sets]
    setUAC [prf, in mathcomp.boot.finset]
    setUACA [prf, in mathcomp.classical.classical_sets]
    setUACA [prf, in mathcomp.boot.finset]
    setUC [prf, in mathcomp.classical.classical_sets]
    setUC [prf, in mathcomp.boot.finset]
    setUCA [prf, in mathcomp.classical.classical_sets]
    setUCA [prf, in mathcomp.boot.finset]
    setUCK [prf, in mathcomp.classical.classical_sets]
    setUCl [prf, in mathcomp.classical.classical_sets]
    setUCr [prf, in mathcomp.classical.classical_sets]
    setUCr [prf, in mathcomp.boot.finset]
    setUD [prf, in mathcomp.boot.finset]
    setUDK [prf, in mathcomp.classical.classical_sets]
    setUDl [prf, in mathcomp.classical.classical_sets]
    setUDl [prf, in mathcomp.boot.finset]
    setUDr [prf, in mathcomp.classical.classical_sets]
    setUid [prf, in mathcomp.classical.classical_sets]
    setUid [prf, in mathcomp.boot.finset]
    setUIDK [prf, in mathcomp.classical.classical_sets]
    setUidl [prf, in mathcomp.classical.classical_sets]
    setUidPl [prf, in mathcomp.classical.classical_sets]
    setUidPl [prf, in mathcomp.boot.finset]
    setUidPr [prf, in mathcomp.classical.classical_sets]
    setUidPr [prf, in mathcomp.boot.finset]
    setUidr [prf, in mathcomp.classical.classical_sets]
    setUIl [prf, in mathcomp.classical.classical_sets]
    setUIl [prf, in mathcomp.boot.finset]
    setUIr [prf, in mathcomp.classical.classical_sets]
    setUIr [prf, in mathcomp.boot.finset]
    setUitv1 [prf, in mathcomp.classical.set_interval]
    setUitv_set2 [prf, in mathcomp.classical.set_interval]
    setUK [prf, in mathcomp.classical.classical_sets]
    setUK [prf, in mathcomp.boot.finset]
    setUKC [prf, in mathcomp.classical.classical_sets]
    setUKD [prf, in mathcomp.classical.classical_sets]
    setUP [prf, in mathcomp.boot.finset]
    setUS [prf, in mathcomp.classical.classical_sets]
    setUS [prf, in mathcomp.boot.finset]
    setUSS [prf, in mathcomp.classical.classical_sets]
    setUSS [prf, in mathcomp.boot.finset]
    setUT [prf, in mathcomp.classical.classical_sets]
    setUT [prf, in mathcomp.boot.finset]
    setUUl [prf, in mathcomp.classical.classical_sets]
    setUUl [prf, in mathcomp.boot.finset]
    setUUr [prf, in mathcomp.classical.classical_sets]
    setUUr [prf, in mathcomp.boot.finset]
    setUv [prf, in mathcomp.classical.classical_sets]
    setvU [prf, in mathcomp.classical.classical_sets]
    setX [def, in mathcomp.classical.classical_sets]
    setX [def, in mathcomp.boot.finset]
    setX0 [prf, in mathcomp.classical.classical_sets]
    setX_bigcupl [prf, in mathcomp.classical.classical_sets]
    setX_bigcupr [prf, in mathcomp.classical.classical_sets]
    setX_dprod [prf, in mathcomp.finite_group.gproduct]
    setX_gen [prf, in mathcomp.finite_group.gproduct]
    setX_group [def, in mathcomp.finite_group.gproduct]
    setX_of_sigT [def, in mathcomp.analysis.topology_theory.subtype_topology]
    setX_of_sigT_continuous [prf, in mathcomp.analysis.topology_theory.subtype_topology]
    setX_of_sigTK [prf, in mathcomp.analysis.topology_theory.subtype_topology]
    setX_prod [prf, in mathcomp.finite_group.gproduct]
    setXI [prf, in mathcomp.classical.classical_sets]
    setXL [def, in mathcomp.classical.classical_sets]
    setXn [def, in mathcomp.boot.finset]
    setXn_dprod [prf, in mathcomp.finite_group.gproduct]
    setXn_gen [prf, in mathcomp.finite_group.gproduct]
    setXn_group [def, in mathcomp.finite_group.gproduct]
    setXn_prod [prf, in mathcomp.finite_group.gproduct]
    setXn_sol [prf, in mathcomp.solvable.nilpotent]
    setXnP [prf, in mathcomp.boot.finset]
    setXnS [prf, in mathcomp.boot.finset]
    setXP [prf, in mathcomp.boot.finset]
    setXR [def, in mathcomp.classical.classical_sets]
    setXS [prf, in mathcomp.boot.finset]
    setXT [prf, in mathcomp.classical.classical_sets]
    setXTT [prf, in mathcomp.classical.classical_sets]
    setY [def, in mathcomp.classical.classical_sets]
    setY0 [prf, in mathcomp.classical.classical_sets]
    setY_closed [def, in mathcomp.analysis.measure_theory.measurable_structure]
    setY_def [prf, in mathcomp.classical.classical_sets]
    setYA [prf, in mathcomp.classical.classical_sets]
    setYC [prf, in mathcomp.classical.classical_sets]
    setYCT [prf, in mathcomp.classical.classical_sets]
    setYD [prf, in mathcomp.classical.classical_sets]
    setYE [prf, in mathcomp.classical.classical_sets]
    setYI [prf, in mathcomp.classical.classical_sets]
    setYK [prf, in mathcomp.classical.classical_sets]
    setYTC [prf, in mathcomp.classical.classical_sets]
    setYU [prf, in mathcomp.classical.classical_sets]
    sfinite_Fubini [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_fubini]
    sfinite_kernel [prf, in mathcomp.analysis.kernel]
    sfinite_kernel_measure [prf, in mathcomp.analysis.kernel]
    sfinite_kernel_subdef [def, in mathcomp.analysis.kernel]
    sfinite_measure [def, in mathcomp.analysis.measure_theory.measure_function]
    sfinite_measure_seq [def, in mathcomp.analysis.measure_theory.measure_function]
    sfinite_measure_seqP [prf, in mathcomp.analysis.measure_theory.measure_function]
    sfinite_measure_sigma_finite [prf, in mathcomp.analysis.measure_theory.measure_function]
    sfinite_mzero [prf, in mathcomp.analysis.measure_theory.measure_function]
    SFiniteKernel [abbrev, in mathcomp.analysis.kernel]
    SFiniteKernel [mod, in mathcomp.analysis.kernel]
    SFiniteKernel.axioms_ [rec, in mathcomp.analysis.kernel]
    SFiniteKernel.class [proj, in mathcomp.analysis.kernel]
    SFiniteKernel.clone [abbrev, in mathcomp.analysis.kernel]
    SFiniteKernel.copy [abbrev, in mathcomp.analysis.kernel]
    SFiniteKernel.Exports [mod, in mathcomp.analysis.kernel]
    SFiniteKernel.kernel_isKernel_mixin [proj, in mathcomp.analysis.kernel]
    SFiniteKernel.kernel_isSFiniteKernel_subdef_mixin [proj, in mathcomp.analysis.kernel]
    SFiniteKernel.on [abbrev, in mathcomp.analysis.kernel]
    SFiniteKernel.on_ [abbrev, in mathcomp.analysis.kernel]
    SFiniteKernel.pack_ [def, in mathcomp.analysis.kernel]
    SFiniteKernel.phant_clone [def, in mathcomp.analysis.kernel]
    SFiniteKernel.phant_on_ [def, in mathcomp.analysis.kernel]
    SFiniteKernel.sort [proj, in mathcomp.analysis.kernel]
    SFiniteKernel.type [rec, in mathcomp.analysis.kernel]
    SFiniteKernel_isFinite [mod, in mathcomp.analysis.kernel]
    SFiniteKernel_isFinite [abbrev, in mathcomp.analysis.kernel]
    SFiniteKernel_isFinite.Build [abbrev, in mathcomp.analysis.kernel]
    SFiniteKernelElpiOperations [mod, in mathcomp.analysis.kernel]
    SFiniteMeasure [abbrev, in mathcomp.analysis.measure_theory.measure_function]
    SFiniteMeasure [mod, in mathcomp.analysis.measure_theory.measure_function]
    SFiniteMeasure.axioms_ [rec, in mathcomp.analysis.measure_theory.measure_function]
    SFiniteMeasure.class [proj, in mathcomp.analysis.measure_theory.measure_function]
    SFiniteMeasure.clone [abbrev, in mathcomp.analysis.measure_theory.measure_function]
    SFiniteMeasure.copy [abbrev, in mathcomp.analysis.measure_theory.measure_function]
    SFiniteMeasure.Exports [mod, in mathcomp.analysis.measure_theory.measure_function]
    SFiniteMeasure.measure_function_Content_isMeasure_mixin [proj, in mathcomp.analysis.measure_theory.measure_function]
    SFiniteMeasure.measure_function_isContent_mixin [proj, in mathcomp.analysis.measure_theory.measure_function]
    SFiniteMeasure.measure_function_isSFinite_mixin [proj, in mathcomp.analysis.measure_theory.measure_function]
    SFiniteMeasure.on [abbrev, in mathcomp.analysis.measure_theory.measure_function]
    SFiniteMeasure.on_ [abbrev, in mathcomp.analysis.measure_theory.measure_function]
    SFiniteMeasure.pack_ [def, in mathcomp.analysis.measure_theory.measure_function]
    SFiniteMeasure.phant_clone [def, in mathcomp.analysis.measure_theory.measure_function]
    SFiniteMeasure.phant_on_ [def, in mathcomp.analysis.measure_theory.measure_function]
    SFiniteMeasure.sort [proj, in mathcomp.analysis.measure_theory.measure_function]
    SFiniteMeasure.type [rec, in mathcomp.analysis.measure_theory.measure_function]
    SFiniteMeasureElpiOperations [mod, in mathcomp.analysis.measure_theory.measure_function]
    sfun [abbrev, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
    sfun [def, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
    sfun0 [prf, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
    sfun1 [prf, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
    sfun_fubini_tonelli [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_fubini]
    sfun_fubini_tonelli1 [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_fubini]
    sfun_fubini_tonelli2 [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_fubini]
    sfun_fubini_tonelli_FE [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_fubini]
    sfun_fubini_tonelli_GE [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_fubini]
    sfun_key [def, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
    sfun_keyed [def, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
    sfun_measurable_fun_fubini_tonelli_F [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_fubini]
    sfun_measurable_fun_fubini_tonelli_G [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_fubini]
    sfun_prod [prf, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
    sfun_rect [prf, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
    sfun_Sub [def, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
    sfun_subring_closed [prf, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
    sfun_sum [prf, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
    sfun_valP [prf, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
    sfunB [prf, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
    sfunD [prf, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
    sfuneqP [prf, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
    sfunM [prf, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
    sfunN [prf, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
    sfunX [prf, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
    sgr [abbrev, in mathcomp.algebra.ssrint]
    sgr [abbrev, in mathcomp.algebra.rat]
    sgr_denq [prf, in mathcomp.algebra.rat]
    sgr_numq [prf, in mathcomp.algebra.rat]
    sgr_numq_div [prf, in mathcomp.algebra.rat]
    sgr_scalq [prf, in mathcomp.algebra.rat]
    sgrEz [prf, in mathcomp.algebra.ssrint]
    sgrMz [prf, in mathcomp.algebra.ssrint]
    sgrz [prf, in mathcomp.algebra.ssrint]
    sgval [def, in mathcomp.finite_group.fingroup]
    sgval_morphism [def, in mathcomp.finite_group.morphism]
    sgval_sub [prf, in mathcomp.finite_group.morphism]
    sgvalK [prf, in mathcomp.finite_group.fingroup]
    sgvalM [prf, in mathcomp.finite_group.fingroup]
    sgvalmK [prf, in mathcomp.finite_group.morphism]
    sgz [def, in mathcomp.algebra.ssrint]
    sgz0 [prf, in mathcomp.algebra.ssrint]
    sgz1 [prf, in mathcomp.algebra.ssrint]
    sgz_contents [prf, in mathcomp.algebra.intdiv]
    sgz_cp0 [prf, in mathcomp.algebra.ssrint]
    sgz_def [prf, in mathcomp.algebra.ssrint]
    sgz_eq [prf, in mathcomp.algebra.ssrint]
    sgz_eq0 [prf, in mathcomp.algebra.ssrint]
    sgz_ge0 [prf, in mathcomp.algebra.ssrint]
    sgz_gt0 [prf, in mathcomp.algebra.ssrint]
    sgz_id [prf, in mathcomp.algebra.ssrint]
    sgz_int [prf, in mathcomp.algebra.ssrint]
    sgz_le0 [prf, in mathcomp.algebra.ssrint]
    sgz_lead_primitive [prf, in mathcomp.algebra.intdiv]
    sgz_lt0 [prf, in mathcomp.algebra.ssrint]
    sgz_odd [prf, in mathcomp.algebra.ssrint]
    sgz_sgr [prf, in mathcomp.algebra.ssrint]
    sgz_smul [prf, in mathcomp.algebra.ssrint]
    sgz_val [ind, in mathcomp.algebra.ssrint]
    sgzE [def, in mathcomp.algebra.ssrint]
    sgzM [prf, in mathcomp.algebra.ssrint]
    sgzN [prf, in mathcomp.algebra.ssrint]
    sgzN1 [prf, in mathcomp.algebra.ssrint]
    SgzNeg [constr, in mathcomp.algebra.ssrint]
    SgzNull [constr, in mathcomp.algebra.ssrint]
    sgzP [prf, in mathcomp.algebra.ssrint]
    SgzPos [constr, in mathcomp.algebra.ssrint]
    sgzX [prf, in mathcomp.algebra.ssrint]
    sh [def, in mathcomp.solvable.burnside_app]
    Sh [def, in mathcomp.solvable.burnside_app]
    Sh_inj [prf, in mathcomp.solvable.burnside_app]
    sh_inv [prf, in mathcomp.solvable.burnside_app]
    shape [def, in mathcomp.boot.seq]
    shape_rev [prf, in mathcomp.boot.seq]
    shift [def, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
    shift0 [prf, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
    shorten [def, in mathcomp.boot.path]
    shorten_spec [ind, in mathcomp.boot.path]
    shortenP [prf, in mathcomp.boot.path]
    ShortenSpec [constr, in mathcomp.boot.path]
    ShortFunSyntax [mod, in mathcomp.classical.functions]
    showo [prf, in mathcomp.analysis.landau]
    sig2_eqW [prf, in mathcomp.boot.choice]
    sig2W [prf, in mathcomp.boot.choice]
    sig_big_dep [prf, in mathcomp.boot.bigop]
    sig_big_dep_idem [prf, in mathcomp.boot.bigop]
    sig_eq2W [prf, in mathcomp.boot.choice]
    sig_eqW [prf, in mathcomp.boot.choice]
    sigL [def, in mathcomp.classical.functions]
    sigL2K [prf, in mathcomp.classical.functions]
    sigL_arrow [def, in mathcomp.analysis.topology_theory.function_spaces]
    sigL_bijP [prf, in mathcomp.classical.functions]
    sigL_funP [prf, in mathcomp.classical.functions]
    sigL_injP [prf, in mathcomp.classical.functions]
    sigL_isfun [prf, in mathcomp.classical.functions]
    sigL_restrict [prf, in mathcomp.classical.functions]
    sigL_some_inv [prf, in mathcomp.classical.functions]
    sigL_surjP [prf, in mathcomp.classical.functions]
    sigL_valL [prf, in mathcomp.classical.functions]
    sigL_valLfun [prf, in mathcomp.classical.functions]
    sigLE [prf, in mathcomp.classical.functions]
    sigLfun [def, in mathcomp.classical.functions]
    sigLK [prf, in mathcomp.classical.functions]
    sigLR [def, in mathcomp.classical.functions]
    sigLR_bijP [prf, in mathcomp.classical.functions]
    sigLR_injP [prf, in mathcomp.classical.functions]
    sigLR_surjP [prf, in mathcomp.classical.functions]
    sigLRfun_bijP [prf, in mathcomp.classical.functions]
    sigma_additive [def, in mathcomp.analysis.measure_theory.measure_function]
    sigma_additive_is_additive [prf, in mathcomp.analysis.measure_theory.measure_function]
    sigma_algebra [def, in mathcomp.analysis.measure_theory.measurable_structure]
    sigma_algebra0 [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    sigma_algebra_bigcap [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    sigma_algebra_bigcup [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    sigma_algebra_dynkin [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    sigma_algebra_id [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    sigma_algebra_image [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    sigma_algebra_image_class [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
    sigma_algebra_measurable [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    sigma_algebra_preimage [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    sigma_algebra_preimage_class [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
    sigma_algebra_preimage_classE [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
    sigma_algebra_strace [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    sigma_algebraC [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    sigma_algebraCD [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    sigma_algebraP [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    sigma_display [def, in mathcomp.analysis.measure_theory.measurable_structure]
    sigma_finite [def, in mathcomp.analysis.measure_theory.measure_function]
    sigma_finite_counting [prf, in mathcomp.analysis.measure_theory.counting_measure]
    sigma_finite_mkproduct [prf, in mathcomp.analysis.kernel]
    sigma_finite_mzero [prf, in mathcomp.analysis.measure_theory.measure_function]
    sigma_finiteP [prf, in mathcomp.analysis.measure_theory.measure_function]
    sigma_finiteT [def, in mathcomp.analysis.measure_theory.measure_function]
    sigma_ring [def, in mathcomp.analysis.measure_theory.measurable_structure]
    sigma_ring_monotone [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    sigma_subadditive [def, in mathcomp.analysis.measure_theory.measure_extension]
    SigmaFiniteContent [abbrev, in mathcomp.analysis.measure_theory.measure_function]
    SigmaFiniteContent [mod, in mathcomp.analysis.measure_theory.measure_function]
    SigmaFiniteContent.axioms_ [rec, in mathcomp.analysis.measure_theory.measure_function]
    SigmaFiniteContent.class [proj, in mathcomp.analysis.measure_theory.measure_function]
    SigmaFiniteContent.clone [abbrev, in mathcomp.analysis.measure_theory.measure_function]
    SigmaFiniteContent.copy [abbrev, in mathcomp.analysis.measure_theory.measure_function]
    SigmaFiniteContent.Exports [mod, in mathcomp.analysis.measure_theory.measure_function]
    SigmaFiniteContent.Exports.sigma_finite_content [abbrev, in mathcomp.analysis.measure_theory.measure_function]
    SigmaFiniteContent.measure_function_isContent_mixin [proj, in mathcomp.analysis.measure_theory.measure_function]
    SigmaFiniteContent.measure_function_isSigmaFinite_mixin [proj, in mathcomp.analysis.measure_theory.measure_function]
    SigmaFiniteContent.on [abbrev, in mathcomp.analysis.measure_theory.measure_function]
    SigmaFiniteContent.on_ [abbrev, in mathcomp.analysis.measure_theory.measure_function]
    SigmaFiniteContent.pack_ [def, in mathcomp.analysis.measure_theory.measure_function]
    SigmaFiniteContent.phant_clone [def, in mathcomp.analysis.measure_theory.measure_function]
    SigmaFiniteContent.phant_on_ [def, in mathcomp.analysis.measure_theory.measure_function]
    SigmaFiniteContent.sort [proj, in mathcomp.analysis.measure_theory.measure_function]
    SigmaFiniteContent.type [rec, in mathcomp.analysis.measure_theory.measure_function]
    SigmaFiniteContentElpiOperations [mod, in mathcomp.analysis.measure_theory.measure_function]
    SigmaFiniteMeasure [abbrev, in mathcomp.analysis.measure_theory.measure_function]
    SigmaFiniteMeasure [mod, in mathcomp.analysis.measure_theory.measure_function]
    SigmaFiniteMeasure.axioms_ [rec, in mathcomp.analysis.measure_theory.measure_function]
    SigmaFiniteMeasure.class [proj, in mathcomp.analysis.measure_theory.measure_function]
    SigmaFiniteMeasure.clone [abbrev, in mathcomp.analysis.measure_theory.measure_function]
    SigmaFiniteMeasure.copy [abbrev, in mathcomp.analysis.measure_theory.measure_function]
    SigmaFiniteMeasure.Exports [mod, in mathcomp.analysis.measure_theory.measure_function]
    SigmaFiniteMeasure.Exports.join_measure_function_SigmaFiniteMeasure_between_measure_function_Measure_and_measure_function_SigmaFiniteContent [def, in mathcomp.analysis.measure_theory.measure_function]
    SigmaFiniteMeasure.Exports.join_measure_function_SigmaFiniteMeasure_between_measure_function_SFiniteMeasure_and_measure_function_SigmaFiniteContent [def, in mathcomp.analysis.measure_theory.measure_function]
    SigmaFiniteMeasure.Exports.sigma_finite_measure [abbrev, in mathcomp.analysis.measure_theory.measure_function]
    SigmaFiniteMeasure.measure_function_Content_isMeasure_mixin [proj, in mathcomp.analysis.measure_theory.measure_function]
    SigmaFiniteMeasure.measure_function_isContent_mixin [proj, in mathcomp.analysis.measure_theory.measure_function]
    SigmaFiniteMeasure.measure_function_isSFinite_mixin [proj, in mathcomp.analysis.measure_theory.measure_function]
    SigmaFiniteMeasure.measure_function_isSigmaFinite_mixin [proj, in mathcomp.analysis.measure_theory.measure_function]
    SigmaFiniteMeasure.on [abbrev, in mathcomp.analysis.measure_theory.measure_function]
    SigmaFiniteMeasure.on_ [abbrev, in mathcomp.analysis.measure_theory.measure_function]
    SigmaFiniteMeasure.pack_ [def, in mathcomp.analysis.measure_theory.measure_function]
    SigmaFiniteMeasure.phant_clone [def, in mathcomp.analysis.measure_theory.measure_function]
    SigmaFiniteMeasure.phant_on_ [def, in mathcomp.analysis.measure_theory.measure_function]
    SigmaFiniteMeasure.sort [proj, in mathcomp.analysis.measure_theory.measure_function]
    SigmaFiniteMeasure.type [rec, in mathcomp.analysis.measure_theory.measure_function]
    SigmaFiniteMeasureElpiOperations [mod, in mathcomp.analysis.measure_theory.measure_function]
    SigmaFiniteTransitionKernel [abbrev, in mathcomp.analysis.kernel]
    SigmaFiniteTransitionKernel [mod, in mathcomp.analysis.kernel]
    SigmaFiniteTransitionKernel.axioms_ [rec, in mathcomp.analysis.kernel]
    SigmaFiniteTransitionKernel.class [proj, in mathcomp.analysis.kernel]
    SigmaFiniteTransitionKernel.clone [abbrev, in mathcomp.analysis.kernel]
    SigmaFiniteTransitionKernel.copy [abbrev, in mathcomp.analysis.kernel]
    SigmaFiniteTransitionKernel.Exports [mod, in mathcomp.analysis.kernel]
    SigmaFiniteTransitionKernel.Exports.sigma_finite_kernel [abbrev, in mathcomp.analysis.kernel]
    SigmaFiniteTransitionKernel.kernel_isKernel_mixin [proj, in mathcomp.analysis.kernel]
    SigmaFiniteTransitionKernel.kernel_isSigmaFiniteTransitionKernel_mixin [proj, in mathcomp.analysis.kernel]
    SigmaFiniteTransitionKernel.on [abbrev, in mathcomp.analysis.kernel]
    SigmaFiniteTransitionKernel.on_ [abbrev, in mathcomp.analysis.kernel]
    SigmaFiniteTransitionKernel.pack_ [def, in mathcomp.analysis.kernel]
    SigmaFiniteTransitionKernel.phant_clone [def, in mathcomp.analysis.kernel]
    SigmaFiniteTransitionKernel.phant_on_ [def, in mathcomp.analysis.kernel]
    SigmaFiniteTransitionKernel.sort [proj, in mathcomp.analysis.kernel]
    SigmaFiniteTransitionKernel.type [rec, in mathcomp.analysis.kernel]
    SigmaFiniteTransitionKernelElpiOperations [mod, in mathcomp.analysis.kernel]
    SigmaRing [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
    SigmaRing [mod, in mathcomp.analysis.measure_theory.measurable_structure]
    SigmaRing.axioms_ [rec, in mathcomp.analysis.measure_theory.measurable_structure]
    SigmaRing.choice_hasChoice_mixin [proj, in mathcomp.analysis.measure_theory.measurable_structure]
    SigmaRing.class [proj, in mathcomp.analysis.measure_theory.measurable_structure]
    SigmaRing.classical_sets_isPointed_mixin [proj, in mathcomp.analysis.measure_theory.measurable_structure]
    SigmaRing.clone [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
    SigmaRing.copy [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
    SigmaRing.eqtype_hasDecEq_mixin [proj, in mathcomp.analysis.measure_theory.measurable_structure]
    SigmaRing.Exports [mod, in mathcomp.analysis.measure_theory.measurable_structure]
    SigmaRing.Exports.sigmaRingType [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
    SigmaRing.measurable_structure_hasMeasurableCountableUnion_mixin [proj, in mathcomp.analysis.measure_theory.measurable_structure]
    SigmaRing.measurable_structure_isSemiRingOfSets_mixin [proj, in mathcomp.analysis.measure_theory.measurable_structure]
    SigmaRing.measurable_structure_SemiRingOfSets_isRingOfSets_mixin [proj, in mathcomp.analysis.measure_theory.measurable_structure]
    SigmaRing.on [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
    SigmaRing.on_ [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
    SigmaRing.pack_ [def, in mathcomp.analysis.measure_theory.measurable_structure]
    SigmaRing.phant_clone [def, in mathcomp.analysis.measure_theory.measurable_structure]
    SigmaRing.phant_on_ [def, in mathcomp.analysis.measure_theory.measurable_structure]
    SigmaRing.sort [proj, in mathcomp.analysis.measure_theory.measurable_structure]
    SigmaRing.type [rec, in mathcomp.analysis.measure_theory.measurable_structure]
    SigmaRingElpiOperations [mod, in mathcomp.analysis.measure_theory.measurable_structure]
    sigmaRingType_lambda_system [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    sign_morph [def, in mathcomp.solvable.alt]
    signed [file, in mathcomp.reals.signed]
    Signed [mod, in mathcomp.reals.signed]
    Signed.allP [proj, in mathcomp.reals.signed]
    Signed.def [rec, in mathcomp.reals.signed]
    Signed.Exports [mod, in mathcomp.reals.signed]
    Signed.Exports.nonneg [def, in mathcomp.reals.signed]
    Signed.Exports.num [abbrev, in mathcomp.reals.signed]
    Signed.Exports.posnum [def, in mathcomp.reals.signed]
    Signed.from [def, in mathcomp.reals.signed]
    Signed.fromP [def, in mathcomp.reals.signed]
    Signed.is_real [def, in mathcomp.reals.signed]
    Signed.mk [def, in mathcomp.reals.signed]
    Signed.P [proj, in mathcomp.reals.signed]
    Signed.r [proj, in mathcomp.reals.signed]
    Signed.reality_cond [def, in mathcomp.reals.signed]
    Signed.sort [proj, in mathcomp.reals.signed]
    Signed.sort_x0 [proj, in mathcomp.reals.signed]
    Signed.spec [abbrev, in mathcomp.reals.signed]
    Signed.typ [rec, in mathcomp.reals.signed]
    signed_intro [prf, in mathcomp.reals.signed]
    signed_le_total [prf, in mathcomp.reals.signed]
    signr_scalq [prf, in mathcomp.algebra.rat]
    sigR [def, in mathcomp.classical.functions]
    sigR_funK [prf, in mathcomp.classical.functions]
    sigR_some_inv [prf, in mathcomp.classical.functions]
    sigRK [prf, in mathcomp.classical.functions]
    SigSub [def, in mathcomp.classical.classical_sets]
    sigT_compact [prf, in mathcomp.analysis.topology_theory.sigT_topology]
    sigT_continuous [prf, in mathcomp.analysis.topology_theory.sigT_topology]
    sigT_fun [def, in mathcomp.classical.unstable]
    sigT_hausdorff [prf, in mathcomp.analysis.topology_theory.separation_axioms]
    sigT_nbhs [def, in mathcomp.analysis.topology_theory.sigT_topology]
    sigT_nbhs_nbhs [prf, in mathcomp.analysis.topology_theory.sigT_topology]
    sigT_nbhs_proper [prf, in mathcomp.analysis.topology_theory.sigT_topology]
    sigT_nbhs_singleton [prf, in mathcomp.analysis.topology_theory.sigT_topology]
    sigT_nbhsE [prf, in mathcomp.analysis.topology_theory.sigT_topology]
    sigT_of_setX [def, in mathcomp.analysis.topology_theory.subtype_topology]
    sigT_of_setX_continuous [prf, in mathcomp.analysis.topology_theory.subtype_topology]
    sigT_of_setXK [prf, in mathcomp.analysis.topology_theory.subtype_topology]
    sigT_openP [prf, in mathcomp.analysis.topology_theory.sigT_topology]
    sigT_setUE [prf, in mathcomp.analysis.topology_theory.sigT_topology]
    sigT_topology [file, in mathcomp.analysis.topology_theory.sigT_topology]
    sigW [prf, in mathcomp.boot.choice]
    similar [abbrev, in mathcomp.algebra.mxred]
    similar_diag [abbrev, in mathcomp.algebra.mxred]
    similar_diag_mxminpoly [prf, in mathcomp.algebra.mxred]
    similar_diag_row_base [prf, in mathcomp.algebra.mxred]
    similar_diag_sum [prf, in mathcomp.algebra.mxred]
    similar_diagLR [prf, in mathcomp.algebra.mxred]
    similar_diagP [prf, in mathcomp.algebra.mxred]
    similar_diagPex [prf, in mathcomp.algebra.mxred]
    similar_diagPp [prf, in mathcomp.algebra.mxred]
    similar_in [abbrev, in mathcomp.algebra.mxred]
    similar_in_to [abbrev, in mathcomp.algebra.mxred]
    similar_mxminpoly [prf, in mathcomp.algebra.mxred]
    similar_to [def, in mathcomp.algebra.mxred]
    similar_trig [abbrev, in mathcomp.algebra.mxred]
    similarLR [prf, in mathcomp.algebra.mxred]
    similarP [prf, in mathcomp.algebra.mxred]
    similarPp [prf, in mathcomp.algebra.mxred]
    similarRL [prf, in mathcomp.algebra.mxred]
    similarW [prf, in mathcomp.algebra.mxred]
    simmx_for [abbrev, in mathcomp.algebra.mxpoly]
    simmx_in [abbrev, in mathcomp.algebra.mxpoly]
    simmx_in_to [abbrev, in mathcomp.algebra.mxpoly]
    simmx_minpoly [prf, in mathcomp.algebra.mxpoly]
    simmx_to_for [def, in mathcomp.algebra.mxpoly]
    simmxLR [prf, in mathcomp.algebra.mxpoly]
    simmxP [prf, in mathcomp.algebra.mxpoly]
    simmxPp [prf, in mathcomp.algebra.mxpoly]
    simmxRL [prf, in mathcomp.algebra.mxpoly]
    simmxW [prf, in mathcomp.algebra.mxpoly]
    simp [abbrev, in mathcomp.algebra.polydiv]
    simp [abbrev, in mathcomp.algebra.poly]
    simp [abbrev, in mathcomp.algebra.mxalgebra]
    simp [abbrev, in mathcomp.algebra.matrix]
    simpl_pred_finpredType [def, in mathcomp.finmap.finmap]
    simple [def, in mathcomp.solvable.gseries]
    simple_Alt5 [prf, in mathcomp.solvable.alt]
    simple_Alt5_base [prf, in mathcomp.solvable.alt]
    simple_Alt_3 [prf, in mathcomp.solvable.alt]
    simple_bounded [prf, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
    simple_compsP [prf, in mathcomp.solvable.jordanholder]
    simple_functions [file, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
    simple_maxnormal [prf, in mathcomp.solvable.gseries]
    simple_sol_prime [prf, in mathcomp.solvable.maximal]
    simpleP [prf, in mathcomp.solvable.gseries]
    simplrefl [abbrev, in mathcomp.boot.ssrAC]
    sin [abbrev, in mathcomp.analysis.trigo]
    sin [mod, in mathcomp.analysis.trigo]
    sin.body [def, in mathcomp.analysis.trigo]
    sin.unlock [def, in mathcomp.analysis.trigo]
    sin0 [prf, in mathcomp.analysis.trigo]
    sin0cos1 [prf, in mathcomp.analysis.trigo]
    sin1cos0 [prf, in mathcomp.analysis.trigo]
    sin2_gt0 [prf, in mathcomp.analysis.trigo]
    sin2cos2 [prf, in mathcomp.analysis.trigo]
    sin2pi [prf, in mathcomp.analysis.trigo]
    sin_acos [prf, in mathcomp.analysis.trigo]
    sin_coeff [def, in mathcomp.analysis.trigo]
    sin_coeff' [def, in mathcomp.analysis.trigo]
    sin_coeff'E [prf, in mathcomp.analysis.trigo]
    sin_coeff_even [prf, in mathcomp.analysis.trigo]
    sin_coeffE [prf, in mathcomp.analysis.trigo]
    sin_ge0_pi [prf, in mathcomp.analysis.trigo]
    sin_geN1 [prf, in mathcomp.analysis.trigo]
    sin_gt0_pi [prf, in mathcomp.analysis.trigo]
    sin_gt0_pihalf [prf, in mathcomp.analysis.trigo]
    sin_inj [prf, in mathcomp.analysis.trigo]
    sin_inum [def, in mathcomp.analysis.trigo]
    sin_le1 [prf, in mathcomp.analysis.trigo]
    sin_Locked [modtype, in mathcomp.analysis.trigo]
    sin_Locked.body [ax, in mathcomp.analysis.trigo]
    sin_Locked.unlock [ax, in mathcomp.analysis.trigo]
    sin_max [prf, in mathcomp.analysis.trigo]
    sin_mulr2n [prf, in mathcomp.analysis.trigo]
    sin_pihalf [prf, in mathcomp.analysis.trigo]
    sin_sg [prf, in mathcomp.analysis.trigo]
    sin_unlock_subterm [def, in mathcomp.analysis.trigo]
    sinB [prf, in mathcomp.analysis.trigo]
    sinBpihalf [prf, in mathcomp.analysis.trigo]
    sinD [prf, in mathcomp.analysis.trigo]
    sinD2pi [prf, in mathcomp.analysis.trigo]
    sinD_cosD [prf, in mathcomp.analysis.trigo]
    sinDpi [prf, in mathcomp.analysis.trigo]
    sinDpihalf [prf, in mathcomp.analysis.trigo]
    sinE [prf, in mathcomp.analysis.trigo]
    singletons [def, in mathcomp.analysis.topology_theory.function_spaces]
    sinK [prf, in mathcomp.analysis.trigo]
    sinN [prf, in mathcomp.analysis.trigo]
    sinN_cosN [prf, in mathcomp.analysis.trigo]
    sinpi [prf, in mathcomp.analysis.trigo]
    sintegral [def, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_definition]
    sintegral0 [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_definition]
    sintegral_EFin_cst [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_nonneg]
    sintegral_ge0 [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_definition]
    sintegral_giry_join [prf, in mathcomp.analysis.lebesgue_integral_theory.giry]
    sintegral_indic [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_definition]
    sintegralD [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_definition]
    sintegralE [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_definition]
    sintegralEnnsfun [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_definition]
    sintegralET [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_definition]
    sintegralrM [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_definition]
    size [def, in mathcomp.boot.seq]
    size0nil [prf, in mathcomp.boot.seq]
    size1_polyC [prf, in mathcomp.algebra.poly]
    size1_zip [prf, in mathcomp.boot.seq]
    size2_zip [prf, in mathcomp.boot.seq]
    size_abelian_type [prf, in mathcomp.solvable.abelian]
    size_add [abbrev, in mathcomp.algebra.poly]
    size_addl [abbrev, in mathcomp.algebra.poly]
    size_algC_pfactor [prf, in mathcomp.field.algC]
    size_algR_pfactor [prf, in mathcomp.field.algC]
    size_allpairs [prf, in mathcomp.boot.seq]
    size_allpairs_dep [prf, in mathcomp.boot.seq]
    size_basis [prf, in mathcomp.algebra.vector]
    size_behead [prf, in mathcomp.boot.seq]
    size_belast [prf, in mathcomp.boot.seq]
    size_bseq [prf, in mathcomp.boot.tuple]
    size_cast_bseq [prf, in mathcomp.boot.tuple]
    size_cat [prf, in mathcomp.boot.seq]
    size_char_poly [prf, in mathcomp.algebra.mxpoly]
    size_Cmul [prf, in mathcomp.algebra.poly]
    size_codom [prf, in mathcomp.boot.fintype]
    size_comp_poly [prf, in mathcomp.algebra.poly]
    size_comp_poly2 [prf, in mathcomp.algebra.poly]
    size_comp_poly_leq [prf, in mathcomp.algebra.poly]
    size_cons_poly [prf, in mathcomp.algebra.poly]
    size_Cyclotomic [prf, in mathcomp.field.cyclotomic]
    size_cyclotomic [prf, in mathcomp.field.cyclotomic]
    size_drop [prf, in mathcomp.boot.seq]
    size_drop_poly [prf, in mathcomp.algebra.poly]
    size_enum_ord [prf, in mathcomp.boot.fintype]
    size_eq0 [prf, in mathcomp.boot.seq]
    size_even_poly [prf, in mathcomp.algebra.poly]
    size_even_poly_eq [prf, in mathcomp.algebra.poly]
    size_exp [prf, in mathcomp.algebra.poly]
    size_exp_leq [abbrev, in mathcomp.algebra.poly]
    size_exp_XsubC [prf, in mathcomp.algebra.poly]
    size_Fadjoin_poly [prf, in mathcomp.field.fieldext]
    size_filter [prf, in mathcomp.boot.seq]
    size_filter_gt0 [prf, in mathcomp.classical.unstable]
    size_filter_gt0 [prf, in mathcomp.boot.seq]
    size_flatten [prf, in mathcomp.boot.seq]
    size_image [prf, in mathcomp.boot.fintype]
    size_incr_nth [prf, in mathcomp.boot.seq]
    size_infix [prf, in mathcomp.boot.seq]
    size_insub_bseq [prf, in mathcomp.boot.tuple]
    size_iota [prf, in mathcomp.boot.seq]
    size_lagrange [prf, in mathcomp.algebra.qpoly]
    size_lagrange_ [prf, in mathcomp.algebra.qpoly]
    size_map [prf, in mathcomp.boot.seq]
    size_map_inj_poly [prf, in mathcomp.algebra.poly]
    size_map_poly [prf, in mathcomp.algebra.poly]
    size_map_poly_id0 [prf, in mathcomp.algebra.poly]
    size_map_polyC [prf, in mathcomp.algebra.poly]
    size_mask [prf, in mathcomp.boot.seq]
    size_merge [prf, in mathcomp.boot.path]
    size_merge_sort_push [prf, in mathcomp.boot.path]
    size_minCpoly [prf, in mathcomp.field.algC]
    size_minPoly [prf, in mathcomp.field.fieldext]
    size_mk_monic [prf, in mathcomp.algebra.qpoly]
    size_mk_monic_gt0 [prf, in mathcomp.algebra.qpoly]
    size_mk_monic_gt1 [prf, in mathcomp.algebra.qpoly]
    size_mkseq [prf, in mathcomp.boot.seq]
    size_Mmonic [prf, in mathcomp.algebra.poly]
    size_mod_mxminpoly [prf, in mathcomp.algebra.mxpoly]
    size_monicM [prf, in mathcomp.algebra.poly]
    size_mset [def, in mathcomp.finmap.multiset]
    size_mset0 [prf, in mathcomp.finmap.multiset]
    size_mset_eq0 [prf, in mathcomp.finmap.multiset]
    size_Msign [prf, in mathcomp.algebra.poly]
    size_mul [prf, in mathcomp.algebra.poly]
    size_mul_eq1 [prf, in mathcomp.algebra.poly]
    size_mul_leq [abbrev, in mathcomp.algebra.poly]
    size_mulX [prf, in mathcomp.algebra.poly]
    size_mulXn [prf, in mathcomp.algebra.poly]
    size_MXaddC [prf, in mathcomp.algebra.poly]
    size_mxminpoly [prf, in mathcomp.algebra.mxpoly]
    size_ncons [prf, in mathcomp.boot.seq]
    size_npoly [prf, in mathcomp.algebra.qpoly]
    size_npoly0 [prf, in mathcomp.algebra.qpoly]
    size_nseq [prf, in mathcomp.boot.seq]
    size_odd_poly [prf, in mathcomp.algebra.poly]
    size_odd_poly_eq [prf, in mathcomp.algebra.poly]
    size_opp [abbrev, in mathcomp.algebra.poly]
    size_orbit [prf, in mathcomp.boot.fingraph]
    size_pairmap [prf, in mathcomp.boot.seq]
    size_permutations [prf, in mathcomp.boot.seq]
    size_pmap [prf, in mathcomp.boot.seq]
    size_pmap_sub [prf, in mathcomp.boot.seq]
    size_poly [prf, in mathcomp.algebra.poly]
    size_Poly [prf, in mathcomp.algebra.poly]
    size_poly0 [prf, in mathcomp.algebra.poly]
    size_poly1 [prf, in mathcomp.algebra.poly]
    size_poly1P [prf, in mathcomp.algebra.poly]
    size_poly_eq [prf, in mathcomp.algebra.poly]
    size_poly_eq0 [prf, in mathcomp.algebra.poly]
    size_poly_exp_leq [prf, in mathcomp.algebra.poly]
    size_poly_gt0 [prf, in mathcomp.algebra.poly]
    size_poly_leq0 [prf, in mathcomp.algebra.poly]
    size_poly_leq0P [prf, in mathcomp.algebra.poly]
    size_poly_prod_leq [prf, in mathcomp.algebra.poly]
    size_poly_XaY [prf, in mathcomp.algebra.polyXY]
    size_poly_XmY [prf, in mathcomp.algebra.polyXY]
    size_polyC [prf, in mathcomp.algebra.poly]
    size_polyC_leq1 [prf, in mathcomp.algebra.poly]
    size_polyD [prf, in mathcomp.algebra.poly]
    size_polyDl [prf, in mathcomp.algebra.poly]
    size_polyMleq [prf, in mathcomp.algebra.poly]
    size_polyN [prf, in mathcomp.algebra.poly]
    size_polyX [prf, in mathcomp.algebra.poly]
    size_polyXn [prf, in mathcomp.algebra.poly]
    size_prefix [prf, in mathcomp.boot.seq]
    size_prod [prf, in mathcomp.algebra.poly]
    size_prod_eq1 [prf, in mathcomp.algebra.poly]
    size_prod_leq [abbrev, in mathcomp.algebra.poly]
    size_prod_seq [prf, in mathcomp.algebra.poly]
    size_prod_seq_eq1 [prf, in mathcomp.algebra.poly]
    size_prod_XsubC [prf, in mathcomp.algebra.poly]
    size_proper_mul [prf, in mathcomp.algebra.poly]
    size_rat_int_poly [prf, in mathcomp.algebra.rat]
    size_rcons [prf, in mathcomp.boot.seq]
    size_rem [prf, in mathcomp.boot.seq]
    size_reshape [prf, in mathcomp.boot.seq]
    size_rev [prf, in mathcomp.boot.seq]
    size_rot [prf, in mathcomp.boot.seq]
    size_rotr [prf, in mathcomp.boot.seq]
    size_scale [prf, in mathcomp.algebra.poly]
    size_scale_leq [prf, in mathcomp.algebra.poly]
    size_scanl [prf, in mathcomp.boot.seq]
    size_seq_fset [prf, in mathcomp.finmap.finmap]
    size_set_nth [prf, in mathcomp.boot.seq]
    size_sort [prf, in mathcomp.boot.path]
    size_sort_keys [prf, in mathcomp.finmap.finmap]
    size_subseq [prf, in mathcomp.boot.seq]
    size_subseq_leqif [prf, in mathcomp.boot.seq]
    size_suffix [prf, in mathcomp.boot.seq]
    size_sum [prf, in mathcomp.algebra.poly]
    size_take [prf, in mathcomp.boot.seq]
    size_take_min [prf, in mathcomp.boot.seq]
    size_take_poly [prf, in mathcomp.algebra.poly]
    size_takel [prf, in mathcomp.boot.seq]
    size_tally_seq [prf, in mathcomp.boot.seq]
    size_traject [prf, in mathcomp.boot.path]
    size_tuple [prf, in mathcomp.boot.tuple]
    size_undup [prf, in mathcomp.boot.seq]
    size_widen_bseq [prf, in mathcomp.boot.tuple]
    size_XaddC [prf, in mathcomp.algebra.poly]
    size_XmulC [prf, in mathcomp.algebra.poly]
    size_Xn_sub_1 [prf, in mathcomp.algebra.poly]
    size_XnaddC [prf, in mathcomp.algebra.poly]
    size_XnsubC [prf, in mathcomp.algebra.poly]
    size_XsubC [prf, in mathcomp.algebra.poly]
    size_zip [prf, in mathcomp.boot.seq]
    size_zprimitive [prf, in mathcomp.algebra.intdiv]
    sizeY [def, in mathcomp.algebra.polyXY]
    sizeY_eq0 [prf, in mathcomp.algebra.polyXY]
    sizeY_mulX [prf, in mathcomp.algebra.polyXY]
    sizeYE [prf, in mathcomp.algebra.polyXY]
    skew [abbrev, in mathcomp.algebra.sesquilinear]
    skew_field_algid1 [prf, in mathcomp.field.falgebra]
    skew_field_dimS [prf, in mathcomp.field.falgebra]
    skew_field_module_dimS [prf, in mathcomp.field.falgebra]
    skew_field_module_semisimple [prf, in mathcomp.field.falgebra]
    skewmx [abbrev, in mathcomp.algebra.sesquilinear]
    small_ent_sub [def, in mathcomp.analysis.topology_theory.function_spaces]
    small_nil_class [prf, in mathcomp.solvable.sylow]
    small_set_sub [prf, in mathcomp.classical.filter]
    smallest [def, in mathcomp.classical.classical_sets]
    smallest_filter_filter [inst, in mathcomp.classical.filter]
    smallest_filter_finI [prf, in mathcomp.classical.filter]
    smallest_id [prf, in mathcomp.classical.classical_sets]
    smallest_lambda_system [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    smallest_setring [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    smallest_sigma_algebra [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    smallest_sigma_ring [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    smallest_sub [prf, in mathcomp.classical.classical_sets]
    snd_fset [def, in mathcomp.classical.cardinality]
    snd_is_monoid_morphism [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
    snd_is_multiplicative [prf, in mathcomp.boot.monoid]
    snd_is_scalable [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
    snd_is_umagma_morphism [prf, in mathcomp.boot.monoid]
    snd_is_zmod_morphism [prf, in mathcomp.boot.nmodule]
    snd_morphism [def, in mathcomp.finite_group.gproduct]
    snd_morphM [prf, in mathcomp.finite_group.gproduct]
    snd_open [prf, in mathcomp.analysis.topology_theory.product_topology]
    snd_set [def, in mathcomp.classical.classical_sets]
    snd_set_snd [prf, in mathcomp.classical.classical_sets]
    snd_setX [prf, in mathcomp.classical.classical_sets]
    sol_coprime_Sylow_exists [prf, in mathcomp.solvable.hall]
    sol_coprime_Sylow_subset [prf, in mathcomp.solvable.hall]
    sol_coprime_Sylow_trans [prf, in mathcomp.solvable.hall]
    sol_der1_proper [prf, in mathcomp.solvable.nilpotent]
    sol_prime_factor_exists [prf, in mathcomp.solvable.maximal]
    solvable [file, in mathcomp.solvable.solvable]
    solvable [def, in mathcomp.solvable.nilpotent]
    solvable1 [prf, in mathcomp.solvable.nilpotent]
    solvable_AltF [prf, in mathcomp.solvable.alt]
    solvable_norm_abelem [prf, in mathcomp.solvable.maximal]
    solvable_SymF [prf, in mathcomp.solvable.alt]
    solvableS [prf, in mathcomp.solvable.nilpotent]
    solve_Qint_span [prf, in mathcomp.algebra.rat]
    some_big_AC_mk_monoid [prf, in mathcomp.boot.bigop]
    some_big_mk_monoid [prf, in mathcomp.boot.bigop]
    some_bigcap [prf, in mathcomp.classical.classical_sets]
    some_comp_inv [prf, in mathcomp.classical.functions]
    Some_fnd [prf, in mathcomp.finmap.finmap]
    some_image [prf, in mathcomp.classical.classical_sets]
    some_inv [prf, in mathcomp.classical.functions]
    some_iter_inv [prf, in mathcomp.classical.functions]
    Some_oextract [prf, in mathcomp.finmap.finmap]
    Some_ojoin [prf, in mathcomp.finmap.finmap]
    some_preimage [prf, in mathcomp.classical.classical_sets]
    some_set0 [prf, in mathcomp.classical.classical_sets]
    some_set1 [prf, in mathcomp.classical.classical_sets]
    some_set_eq0 [prf, in mathcomp.classical.classical_sets]
    some_setC [prf, in mathcomp.classical.classical_sets]
    some_setD [prf, in mathcomp.classical.classical_sets]
    some_setI [prf, in mathcomp.classical.classical_sets]
    some_setT [prf, in mathcomp.classical.classical_sets]
    some_setU [prf, in mathcomp.classical.classical_sets]
    sop [def, in mathcomp.solvable.burnside_app]
    sop_inj [prf, in mathcomp.solvable.burnside_app]
    sop_morph [prf, in mathcomp.solvable.burnside_app]
    sop_spec [prf, in mathcomp.solvable.burnside_app]
    sort [def, in mathcomp.boot.path]
    sort_bseq [def, in mathcomp.boot.tuple]
    sort_bseqP [prf, in mathcomp.boot.tuple]
    sort_iota_stable [prf, in mathcomp.boot.path]
    sort_keys [abbrev, in mathcomp.finmap.finmap]
    sort_keys_id [prf, in mathcomp.finmap.finmap]
    sort_keys_nil [prf, in mathcomp.finmap.finmap]
    sort_keys_perm [abbrev, in mathcomp.finmap.finmap]
    sort_keys_uniq [abbrev, in mathcomp.finmap.finmap]
    sort_keysE [abbrev, in mathcomp.finmap.finmap]
    sort_map [prf, in mathcomp.boot.path]
    sort_pairwise_stable [prf, in mathcomp.boot.path]
    sort_rec1 [def, in mathcomp.boot.path]
    sort_sorted [prf, in mathcomp.boot.path]
    sort_sorted_in [prf, in mathcomp.boot.path]
    sort_stable [prf, in mathcomp.boot.path]
    sort_stable_in [prf, in mathcomp.boot.path]
    sort_tuple [def, in mathcomp.boot.tuple]
    sort_tupleP [prf, in mathcomp.boot.tuple]
    sort_uniq [prf, in mathcomp.boot.path]
    sortE [prf, in mathcomp.boot.path]
    sorted [abbrev, in mathcomp.boot.path]
    sorted [abbrev, in mathcomp.boot.path]
    sorted [def, in mathcomp.boot.path]
    sorted_cat_cons [prf, in mathcomp.boot.path]
    sorted_divisors [prf, in mathcomp.boot.prime]
    sorted_divisors_ltn [prf, in mathcomp.boot.prime]
    sorted_eq [prf, in mathcomp.boot.path]
    sorted_eq_in [prf, in mathcomp.boot.path]
    sorted_filter [prf, in mathcomp.boot.path]
    sorted_filter_in [prf, in mathcomp.boot.path]
    sorted_leq_index [prf, in mathcomp.boot.path]
    sorted_leq_index_in [prf, in mathcomp.boot.path]
    sorted_leq_nth [prf, in mathcomp.boot.path]
    sorted_leq_nth_in [prf, in mathcomp.boot.path]
    sorted_ltn_index [prf, in mathcomp.boot.path]
    sorted_ltn_index_in [prf, in mathcomp.boot.path]
    sorted_ltn_nth [prf, in mathcomp.boot.path]
    sorted_ltn_nth_in [prf, in mathcomp.boot.path]
    sorted_map [prf, in mathcomp.boot.path]
    sorted_mask [prf, in mathcomp.boot.path]
    sorted_mask_in [prf, in mathcomp.boot.path]
    sorted_mask_sort [prf, in mathcomp.boot.path]
    sorted_mask_sort_in [prf, in mathcomp.boot.path]
    sorted_merge [prf, in mathcomp.boot.path]
    sorted_pairwise [prf, in mathcomp.boot.path]
    sorted_pairwise_in [prf, in mathcomp.boot.path]
    sorted_primes [prf, in mathcomp.boot.prime]
    sorted_relI [prf, in mathcomp.boot.path]
    sorted_sort [prf, in mathcomp.boot.path]
    sorted_sort_in [prf, in mathcomp.boot.path]
    sorted_subseq_sort [prf, in mathcomp.boot.path]
    sorted_subseq_sort_in [prf, in mathcomp.boot.path]
    sorted_uniq [prf, in mathcomp.boot.path]
    sorted_uniq_in [prf, in mathcomp.boot.path]
    sortedP [prf, in mathcomp.boot.path]
    SortKeys [mod, in mathcomp.finmap.finmap]
    SortKeys.E [prf, in mathcomp.finmap.finmap]
    SortKeys.eq [prf, in mathcomp.finmap.finmap]
    SortKeys.f [def, in mathcomp.finmap.finmap]
    SortKeys.perm [prf, in mathcomp.finmap.finmap]
    SortKeys.uniq [prf, in mathcomp.finmap.finmap]
    SortKeysSig [modtype, in mathcomp.finmap.finmap]
    sp [abbrev, in mathcomp.algebra.matrix]
    sp [abbrev, in mathcomp.algebra.matrix]
    sp [abbrev, in mathcomp.algebra.matrix]
    sp [abbrev, in mathcomp.algebra.matrix]
    sp [abbrev, in mathcomp.algebra.matrix]
    sp [abbrev, in mathcomp.algebra.matrix]
    sp [abbrev, in mathcomp.algebra.matrix]
    sp [abbrev, in mathcomp.algebra.matrix]
    sp [abbrev, in mathcomp.algebra.matrix]
    sp [abbrev, in mathcomp.algebra.matrix]
    sp [abbrev, in mathcomp.algebra.matrix]
    sp [abbrev, in mathcomp.algebra.matrix]
    Space [constr, in mathcomp.algebra.vector]
    space [ind, in mathcomp.algebra.vector]
    space_ind [scheme, in mathcomp.algebra.vector]
    space_rec [scheme, in mathcomp.algebra.vector]
    space_rect [scheme, in mathcomp.algebra.vector]
    space_sind [scheme, in mathcomp.algebra.vector]
    span [def, in mathcomp.algebra.vector]
    span_basis [prf, in mathcomp.algebra.vector]
    span_bigcat [prf, in mathcomp.algebra.vector]
    span_cat [prf, in mathcomp.algebra.vector]
    span_cons [prf, in mathcomp.algebra.vector]
    span_def [prf, in mathcomp.algebra.vector]
    span_expanded_def [def, in mathcomp.algebra.vector]
    span_key [prf, in mathcomp.algebra.vector]
    span_lfunP [prf, in mathcomp.algebra.vector]
    span_nil [prf, in mathcomp.algebra.vector]
    span_orthogonal [prf, in mathcomp.algebra.sesquilinear]
    span_seq1 [prf, in mathcomp.algebra.vector]
    span_subvP [prf, in mathcomp.algebra.vector]
    span_unlockable [def, in mathcomp.algebra.vector]
    special [def, in mathcomp.solvable.maximal]
    spectral [file, in mathcomp.algebra.spectral]
    spectral_diag [def, in mathcomp.algebra.spectral]
    spectral_unit [prf, in mathcomp.algebra.spectral]
    spectral_unitarymx [prf, in mathcomp.algebra.spectral]
    spectralmx [def, in mathcomp.algebra.spectral]
    split [abbrev, in mathcomp.classical.functions]
    split [abbrev, in mathcomp.classical.functions]
    Split [constr, in mathcomp.boot.path]
    split [ind, in mathcomp.boot.path]
    split [def, in mathcomp.boot.fintype]
    split1 [prf, in mathcomp.boot.nmodule]
    split1_extraspecial [prf, in mathcomp.solvable.maximal]
    Split2r [constr, in mathcomp.boot.path]
    split2r [ind, in mathcomp.boot.path]
    split_ [def, in mathcomp.classical.functions]
    split_ent [def, in mathcomp.analysis.topology_theory.uniform_structure]
    split_ent_subset [prf, in mathcomp.analysis.topology_theory.uniform_structure]
    split_entP [prf, in mathcomp.analysis.topology_theory.uniform_structure]
    split_find [prf, in mathcomp.boot.seq]
    split_find_nth [prf, in mathcomp.boot.seq]
    split_find_nth_spec [ind, in mathcomp.boot.seq]
    split_find_spec [ind, in mathcomp.boot.seq]
    split_ord_spec [ind, in mathcomp.boot.fintype]
    split_ordP [prf, in mathcomp.boot.fintype]
    split_spec [ind, in mathcomp.boot.fintype]
    SplitBij [abbrev, in mathcomp.classical.functions]
    SplitBij [mod, in mathcomp.classical.functions]
    SplitBij.axioms_ [rec, in mathcomp.classical.functions]
    SplitBij.class [proj, in mathcomp.classical.functions]
    SplitBij.clone [abbrev, in mathcomp.classical.functions]
    SplitBij.copy [abbrev, in mathcomp.classical.functions]
    SplitBij.Exports [mod, in mathcomp.classical.functions]
    SplitBij.Exports.join_functions_SplitBij_between_functions_Bij_and_functions_Inversible [def, in mathcomp.classical.functions]
    SplitBij.Exports.join_functions_SplitBij_between_functions_Bij_and_functions_InvFun [def, in mathcomp.classical.functions]
    SplitBij.Exports.join_functions_SplitBij_between_functions_Bij_and_functions_SplitInj [def, in mathcomp.classical.functions]
    SplitBij.Exports.join_functions_SplitBij_between_functions_Bij_and_functions_SplitInjFun [def, in mathcomp.classical.functions]
    SplitBij.Exports.join_functions_SplitBij_between_functions_Bij_and_functions_SplitSurj [def, in mathcomp.classical.functions]
    SplitBij.Exports.join_functions_SplitBij_between_functions_Bij_and_functions_SplitSurjFun [def, in mathcomp.classical.functions]
    SplitBij.Exports.join_functions_SplitBij_between_functions_Inject_and_functions_SplitSurj [def, in mathcomp.classical.functions]
    SplitBij.Exports.join_functions_SplitBij_between_functions_Inject_and_functions_SplitSurjFun [def, in mathcomp.classical.functions]
    SplitBij.Exports.join_functions_SplitBij_between_functions_InjFun_and_functions_SplitSurj [def, in mathcomp.classical.functions]
    SplitBij.Exports.join_functions_SplitBij_between_functions_InjFun_and_functions_SplitSurjFun [def, in mathcomp.classical.functions]
    SplitBij.Exports.join_functions_SplitBij_between_functions_SplitInj_and_functions_SplitSurj [def, in mathcomp.classical.functions]
    SplitBij.Exports.join_functions_SplitBij_between_functions_SplitInj_and_functions_SplitSurjFun [def, in mathcomp.classical.functions]
    SplitBij.Exports.join_functions_SplitBij_between_functions_SplitInj_and_functions_Surject [def, in mathcomp.classical.functions]
    SplitBij.Exports.join_functions_SplitBij_between_functions_SplitInj_and_functions_SurjFun [def, in mathcomp.classical.functions]
    SplitBij.Exports.join_functions_SplitBij_between_functions_SplitInjFun_and_functions_SplitSurj [def, in mathcomp.classical.functions]
    SplitBij.Exports.join_functions_SplitBij_between_functions_SplitInjFun_and_functions_SplitSurjFun [def, in mathcomp.classical.functions]
    SplitBij.Exports.join_functions_SplitBij_between_functions_SplitInjFun_and_functions_Surject [def, in mathcomp.classical.functions]
    SplitBij.Exports.join_functions_SplitBij_between_functions_SplitInjFun_and_functions_SurjFun [def, in mathcomp.classical.functions]
    SplitBij.functions_isFun_mixin [proj, in mathcomp.classical.functions]
    SplitBij.functions_OInv_Can_mixin [proj, in mathcomp.classical.functions]
    SplitBij.functions_OInv_CanV_mixin [proj, in mathcomp.classical.functions]
    SplitBij.functions_OInv_Inv_mixin [proj, in mathcomp.classical.functions]
    SplitBij.functions_OInv_mixin [proj, in mathcomp.classical.functions]
    SplitBij.on [abbrev, in mathcomp.classical.functions]
    SplitBij.on_ [abbrev, in mathcomp.classical.functions]
    SplitBij.pack_ [def, in mathcomp.classical.functions]
    SplitBij.phant_clone [def, in mathcomp.classical.functions]
    SplitBij.phant_on_ [def, in mathcomp.classical.functions]
    SplitBij.sort [proj, in mathcomp.classical.functions]
    SplitBij.type [rec, in mathcomp.classical.functions]
    splitbij_sub [prf, in mathcomp.classical.functions]
    splitbij_sub_sym [prf, in mathcomp.classical.functions]
    SplitBijElpiOperations [mod, in mathcomp.classical.functions]
    SplitHi [constr, in mathcomp.boot.fintype]
    splitid [prf, in mathcomp.classical.functions]
    SplitInj [abbrev, in mathcomp.classical.functions]
    SplitInj [mod, in mathcomp.classical.functions]
    SplitInj.axioms_ [rec, in mathcomp.classical.functions]
    SplitInj.class [proj, in mathcomp.classical.functions]
    SplitInj.clone [abbrev, in mathcomp.classical.functions]
    SplitInj.copy [abbrev, in mathcomp.classical.functions]
    SplitInj.Exports [mod, in mathcomp.classical.functions]
    SplitInj.Exports.join_functions_SplitInj_between_functions_Inject_and_functions_Inversible [def, in mathcomp.classical.functions]
    SplitInj.functions_OInv_Can_mixin [proj, in mathcomp.classical.functions]
    SplitInj.functions_OInv_Inv_mixin [proj, in mathcomp.classical.functions]
    SplitInj.functions_OInv_mixin [proj, in mathcomp.classical.functions]
    SplitInj.on [abbrev, in mathcomp.classical.functions]
    SplitInj.on_ [abbrev, in mathcomp.classical.functions]
    SplitInj.pack_ [def, in mathcomp.classical.functions]
    SplitInj.phant_clone [def, in mathcomp.classical.functions]
    SplitInj.phant_on_ [def, in mathcomp.classical.functions]
    SplitInj.sort [proj, in mathcomp.classical.functions]
    SplitInj.type [rec, in mathcomp.classical.functions]
    SplitInjElpiOperations [mod, in mathcomp.classical.functions]
    SplitInjFun [abbrev, in mathcomp.classical.functions]
    SplitInjFun [mod, in mathcomp.classical.functions]
    SplitInjFun.axioms_ [rec, in mathcomp.classical.functions]
    SplitInjFun.class [proj, in mathcomp.classical.functions]
    SplitInjFun.clone [abbrev, in mathcomp.classical.functions]
    SplitInjFun.copy [abbrev, in mathcomp.classical.functions]
    SplitInjFun.Exports [mod, in mathcomp.classical.functions]
    SplitInjFun.Exports.join_functions_SplitInjFun_between_functions_Fun_and_functions_SplitInj [def, in mathcomp.classical.functions]
    SplitInjFun.Exports.join_functions_SplitInjFun_between_functions_Inject_and_functions_InvFun [def, in mathcomp.classical.functions]
    SplitInjFun.Exports.join_functions_SplitInjFun_between_functions_InjFun_and_functions_Inversible [def, in mathcomp.classical.functions]
    SplitInjFun.Exports.join_functions_SplitInjFun_between_functions_InjFun_and_functions_InvFun [def, in mathcomp.classical.functions]
    SplitInjFun.Exports.join_functions_SplitInjFun_between_functions_InjFun_and_functions_SplitInj [def, in mathcomp.classical.functions]
    SplitInjFun.Exports.join_functions_SplitInjFun_between_functions_InvFun_and_functions_SplitInj [def, in mathcomp.classical.functions]
    SplitInjFun.Exports.join_functions_SplitInjFun_between_functions_OInvFun_and_functions_SplitInj [def, in mathcomp.classical.functions]
    SplitInjFun.functions_isFun_mixin [proj, in mathcomp.classical.functions]
    SplitInjFun.functions_OInv_Can_mixin [proj, in mathcomp.classical.functions]
    SplitInjFun.functions_OInv_Inv_mixin [proj, in mathcomp.classical.functions]
    SplitInjFun.functions_OInv_mixin [proj, in mathcomp.classical.functions]
    SplitInjFun.on [abbrev, in mathcomp.classical.functions]
    SplitInjFun.on_ [abbrev, in mathcomp.classical.functions]
    SplitInjFun.pack_ [def, in mathcomp.classical.functions]
    SplitInjFun.phant_clone [def, in mathcomp.classical.functions]
    SplitInjFun.phant_on_ [def, in mathcomp.classical.functions]
    SplitInjFun.sort [proj, in mathcomp.classical.functions]
    SplitInjFun.type [rec, in mathcomp.classical.functions]
    SplitInjFun_CanV [abbrev, in mathcomp.classical.functions]
    SplitInjFun_CanV [mod, in mathcomp.classical.functions]
    SplitInjFun_CanV.axioms [abbrev, in mathcomp.classical.functions]
    SplitInjFun_CanV.axioms_ [rec, in mathcomp.classical.functions]
    SplitInjFun_CanV.Build [abbrev, in mathcomp.classical.functions]
    SplitInjFun_CanV.Exports [mod, in mathcomp.classical.functions]
    SplitInjFun_CanV.injV [proj, in mathcomp.classical.functions]
    SplitInjFun_CanV.invS [proj, in mathcomp.classical.functions]
    SplitInjFun_CanV.phant_axioms [def, in mathcomp.classical.functions]
    SplitInjFun_CanV.phant_Build [def, in mathcomp.classical.functions]
    SplitInjFunElpiOperations [mod, in mathcomp.classical.functions]
    splitK [prf, in mathcomp.boot.fintype]
    Splitl [constr, in mathcomp.boot.path]
    splitl [ind, in mathcomp.boot.path]
    SplitLo [constr, in mathcomp.boot.fintype]
    SplitOrdHi [constr, in mathcomp.boot.fintype]
    SplitOrdLo [constr, in mathcomp.boot.fintype]
    splitP [prf, in mathcomp.boot.path]
    splitP [prf, in mathcomp.boot.fintype]
    splitP2r [prf, in mathcomp.boot.path]
    splitPl [prf, in mathcomp.boot.path]
    splitPr [prf, in mathcomp.boot.path]
    Splitr [constr, in mathcomp.boot.path]
    splitr [ind, in mathcomp.boot.path]
    splits_over [def, in mathcomp.finite_group.gproduct]
    splitsP [prf, in mathcomp.finite_group.gproduct]
    SplitSurj [abbrev, in mathcomp.classical.functions]
    SplitSurj [mod, in mathcomp.classical.functions]
    SplitSurj.axioms_ [rec, in mathcomp.classical.functions]
    SplitSurj.class [proj, in mathcomp.classical.functions]
    SplitSurj.clone [abbrev, in mathcomp.classical.functions]
    SplitSurj.copy [abbrev, in mathcomp.classical.functions]
    SplitSurj.Exports [mod, in mathcomp.classical.functions]
    SplitSurj.Exports.join_functions_SplitSurj_between_functions_Inversible_and_functions_Surject [def, in mathcomp.classical.functions]
    SplitSurj.functions_OInv_CanV_mixin [proj, in mathcomp.classical.functions]
    SplitSurj.functions_OInv_Inv_mixin [proj, in mathcomp.classical.functions]
    SplitSurj.functions_OInv_mixin [proj, in mathcomp.classical.functions]
    SplitSurj.on [abbrev, in mathcomp.classical.functions]
    SplitSurj.on_ [abbrev, in mathcomp.classical.functions]
    SplitSurj.pack_ [def, in mathcomp.classical.functions]
    SplitSurj.phant_clone [def, in mathcomp.classical.functions]
    SplitSurj.phant_on_ [def, in mathcomp.classical.functions]
    SplitSurj.sort [proj, in mathcomp.classical.functions]
    SplitSurj.type [rec, in mathcomp.classical.functions]
    SplitSurjElpiOperations [mod, in mathcomp.classical.functions]
    SplitSurjFun [abbrev, in mathcomp.classical.functions]
    SplitSurjFun [mod, in mathcomp.classical.functions]
    SplitSurjFun.axioms_ [rec, in mathcomp.classical.functions]
    SplitSurjFun.class [proj, in mathcomp.classical.functions]
    SplitSurjFun.clone [abbrev, in mathcomp.classical.functions]
    SplitSurjFun.copy [abbrev, in mathcomp.classical.functions]
    SplitSurjFun.Exports [mod, in mathcomp.classical.functions]
    SplitSurjFun.Exports.join_functions_SplitSurjFun_between_functions_Fun_and_functions_SplitSurj [def, in mathcomp.classical.functions]
    SplitSurjFun.Exports.join_functions_SplitSurjFun_between_functions_Inversible_and_functions_SurjFun [def, in mathcomp.classical.functions]
    SplitSurjFun.Exports.join_functions_SplitSurjFun_between_functions_InvFun_and_functions_SplitSurj [def, in mathcomp.classical.functions]
    SplitSurjFun.Exports.join_functions_SplitSurjFun_between_functions_InvFun_and_functions_Surject [def, in mathcomp.classical.functions]
    SplitSurjFun.Exports.join_functions_SplitSurjFun_between_functions_InvFun_and_functions_SurjFun [def, in mathcomp.classical.functions]
    SplitSurjFun.Exports.join_functions_SplitSurjFun_between_functions_OInvFun_and_functions_SplitSurj [def, in mathcomp.classical.functions]
    SplitSurjFun.Exports.join_functions_SplitSurjFun_between_functions_SplitSurj_and_functions_SurjFun [def, in mathcomp.classical.functions]
    SplitSurjFun.functions_isFun_mixin [proj, in mathcomp.classical.functions]
    SplitSurjFun.functions_OInv_CanV_mixin [proj, in mathcomp.classical.functions]
    SplitSurjFun.functions_OInv_Inv_mixin [proj, in mathcomp.classical.functions]
    SplitSurjFun.functions_OInv_mixin [proj, in mathcomp.classical.functions]
    SplitSurjFun.on [abbrev, in mathcomp.classical.functions]
    SplitSurjFun.on_ [abbrev, in mathcomp.classical.functions]
    SplitSurjFun.pack_ [def, in mathcomp.classical.functions]
    SplitSurjFun.phant_clone [def, in mathcomp.classical.functions]
    SplitSurjFun.phant_on_ [def, in mathcomp.classical.functions]
    SplitSurjFun.sort [proj, in mathcomp.classical.functions]
    SplitSurjFun.type [rec, in mathcomp.classical.functions]
    SplitSurjFun_Inj [abbrev, in mathcomp.classical.functions]
    SplitSurjFun_Inj [mod, in mathcomp.classical.functions]
    SplitSurjFun_Inj.axioms [abbrev, in mathcomp.classical.functions]
    SplitSurjFun_Inj.axioms_ [rec, in mathcomp.classical.functions]
    SplitSurjFun_Inj.Build [abbrev, in mathcomp.classical.functions]
    SplitSurjFun_Inj.Exports [mod, in mathcomp.classical.functions]
    SplitSurjFun_Inj.inj [proj, in mathcomp.classical.functions]
    SplitSurjFun_Inj.phant_axioms [def, in mathcomp.classical.functions]
    SplitSurjFun_Inj.phant_Build [def, in mathcomp.classical.functions]
    SplitSurjFunElpiOperations [mod, in mathcomp.classical.functions]
    splitting_field_axiom [def, in mathcomp.field.galois]
    splitting_field_normal [prf, in mathcomp.field.galois]
    splitting_galoisField [prf, in mathcomp.field.galois]
    splitting_normalField [prf, in mathcomp.field.galois]
    SplittingField [abbrev, in mathcomp.field.galois]
    SplittingField [mod, in mathcomp.field.galois]
    SplittingField.Algebra_AddMagma_isAddSemigroup_mixin [proj, in mathcomp.field.galois]
    SplittingField.Algebra_BaseAddMagma_isAddMagma_mixin [proj, in mathcomp.field.galois]
    SplittingField.Algebra_BaseAddUMagma_isAddUMagma_mixin [proj, in mathcomp.field.galois]
    SplittingField.Algebra_BaseZmoduleNmodule_isZmodule_mixin [proj, in mathcomp.field.galois]
    SplittingField.Algebra_hasAdd_mixin [proj, in mathcomp.field.galois]
    SplittingField.Algebra_hasOpp_mixin [proj, in mathcomp.field.galois]
    SplittingField.Algebra_hasZero_mixin [proj, in mathcomp.field.galois]
    SplittingField.axioms_ [rec, in mathcomp.field.galois]
    SplittingField.choice_hasChoice_mixin [proj, in mathcomp.field.galois]
    SplittingField.class [proj, in mathcomp.field.galois]
    SplittingField.clone [abbrev, in mathcomp.field.galois]
    SplittingField.copy [abbrev, in mathcomp.field.galois]
    SplittingField.eqtype_hasDecEq_mixin [proj, in mathcomp.field.galois]
    SplittingField.Exports [mod, in mathcomp.field.galois]
    SplittingField.Exports.splittingFieldType [abbrev, in mathcomp.field.galois]
    SplittingField.galois_FieldExt_isSplittingField_mixin [proj, in mathcomp.field.galois]
    SplittingField.GRing_ComUnitRing_isIntegral_mixin [proj, in mathcomp.field.galois]
    SplittingField.GRing_LSemiAlgebra_isSemiAlgebra_mixin [proj, in mathcomp.field.galois]
    SplittingField.GRing_LSemiModule_isLSemiAlgebra_mixin [proj, in mathcomp.field.galois]
    SplittingField.GRing_Nmodule_isLSemiModule_mixin [proj, in mathcomp.field.galois]
    SplittingField.GRing_Nmodule_isPzSemiRing_mixin [proj, in mathcomp.field.galois]
    SplittingField.GRing_NzRing_hasMulInverse_mixin [proj, in mathcomp.field.galois]
    SplittingField.GRing_PzSemiRing_isNonZero_mixin [proj, in mathcomp.field.galois]
    SplittingField.GRing_SemiRing_hasCommutativeMul_mixin [proj, in mathcomp.field.galois]
    SplittingField.GRing_UnitRing_isField_mixin [proj, in mathcomp.field.galois]
    SplittingField.on [abbrev, in mathcomp.field.galois]
    SplittingField.on_ [abbrev, in mathcomp.field.galois]
    SplittingField.pack_ [def, in mathcomp.field.galois]
    SplittingField.phant_clone [def, in mathcomp.field.galois]
    SplittingField.phant_on_ [def, in mathcomp.field.galois]
    SplittingField.sort [proj, in mathcomp.field.galois]
    SplittingField.type [rec, in mathcomp.field.galois]
    SplittingField.vector_LSemiModule_hasFinDim_mixin [proj, in mathcomp.field.galois]
    SplittingField.vector_SemiVector_isProper_mixin [proj, in mathcomp.field.galois]
    SplittingFieldElpiOperations [mod, in mathcomp.field.galois]
    SplittingFieldExports [mod, in mathcomp.field.galois]
    splittingFieldFor [def, in mathcomp.field.galois]
    splittingFieldForS [prf, in mathcomp.field.galois]
    splittingFieldP [prf, in mathcomp.field.galois]
    splittingPoly [prf, in mathcomp.field.galois]
    splitV [prf, in mathcomp.classical.functions]
    sprob_kernel [def, in mathcomp.analysis.kernel]
    sprob_kernel_le1 [prf, in mathcomp.analysis.kernel]
    sprob_kernelP [prf, in mathcomp.analysis.kernel]
    sprob_mkcomp_noparam [prf, in mathcomp.analysis.kernel]
    sprobability_setT [def, in mathcomp.analysis.measure_theory.probability_measure]
    sq [abbrev, in mathcomp.algebra.matrix]
    sq [abbrev, in mathcomp.algebra.matrix]
    sq [abbrev, in mathcomp.algebra.matrix]
    sq [abbrev, in mathcomp.algebra.matrix]
    sq [abbrev, in mathcomp.algebra.matrix]
    sq [abbrev, in mathcomp.algebra.matrix]
    sq [abbrev, in mathcomp.algebra.matrix]
    sqmx_ind [prf, in mathcomp.algebra.matrix]
    sqr_continuous [prf, in mathcomp.analysis.realfun]
    sqr_sqrte [prf, in mathcomp.reals.constructive_ereal]
    sqre_ge0 [prf, in mathcomp.reals.constructive_ereal]
    sqreD [prf, in mathcomp.reals.constructive_ereal]
    sqrn_gt0 [prf, in mathcomp.boot.ssrnat]
    sqrn_inj [prf, in mathcomp.boot.ssrnat]
    sqrnB [prf, in mathcomp.boot.ssrnat]
    sqrnD [prf, in mathcomp.boot.ssrnat]
    sqrnD_sub [prf, in mathcomp.boot.ssrnat]
    sqrt_continuous [prf, in mathcomp.analysis.realfun]
    sqrt_dnorm_eq0 [prf, in mathcomp.algebra.sesquilinear]
    sqrt_dnorm_ge0 [prf, in mathcomp.algebra.sesquilinear]
    sqrt_dnorm_gt0 [prf, in mathcomp.algebra.sesquilinear]
    sqrt_nonzero_subdef [def, in mathcomp.reals.signed]
    sqrt_snum [def, in mathcomp.reals.signed]
    sqrtC_reality_subdef [def, in mathcomp.reals.signed]
    sqrtC_snum [def, in mathcomp.reals.signed]
    sqrte [def, in mathcomp.reals.constructive_ereal]
    sqrte0 [prf, in mathcomp.reals.constructive_ereal]
    sqrte_fin_num [prf, in mathcomp.reals.constructive_ereal]
    sqrte_ge0 [prf, in mathcomp.reals.constructive_ereal]
    sqrte_sqr [prf, in mathcomp.reals.constructive_ereal]
    sqrteM [prf, in mathcomp.reals.constructive_ereal]
    sqrtK [prf, in mathcomp.classical.unstable]
    square [def, in mathcomp.solvable.burnside_app]
    square_coloring_number2 [def, in mathcomp.solvable.burnside_app]
    square_coloring_number4 [def, in mathcomp.solvable.burnside_app]
    square_coloring_number8 [def, in mathcomp.solvable.burnside_app]
    squash [constr, in mathcomp.classical.classical_sets]
    squashed [ind, in mathcomp.classical.classical_sets]
    squeeze_cvge [prf, in mathcomp.analysis.normedtype_theory.normed_module]
    squeeze_cvgr [prf, in mathcomp.analysis.normedtype_theory.normed_module]
    squeeze_fin [prf, in mathcomp.analysis.normedtype_theory.normed_module]
    ssetI [def, in mathcomp.boot.finset]
    ssquash [def, in mathcomp.classical.functions]
    ssrAC [file, in mathcomp.boot.ssrAC]
    ssralg [file, in mathcomp.algebra.algebraic_hierarchy.ssralg]
    ssrbool [file, in mathcomp.boot.ssrbool]
    ssreflect [file, in mathcomp.boot.ssreflect]
    ssrfun [file, in mathcomp.boot.ssrfun]
    ssrint [file, in mathcomp.algebra.ssrint]
    ssrmatching [file, in mathcomp.boot.ssrmatching]
    ssrnat [file, in mathcomp.boot.ssrnat]
    ssrnotations [file, in mathcomp.boot.ssrnotations]
    ssrnum [file, in mathcomp.algebra.numeric_hierarchy.ssrnum]
    ssval [proj, in mathcomp.boot.fintype]
    ssvalP [proj, in mathcomp.boot.fintype]
    sT [abbrev, in mathcomp.reals.signed]
    sT [abbrev, in mathcomp.reals.signed]
    sT [abbrev, in mathcomp.reals.signed]
    sT [abbrev, in mathcomp.finite_group.fingroup]
    sT [abbrev, in mathcomp.boot.fintype]
    sT [abbrev, in mathcomp.boot.finset]
    stab_ntransitive [prf, in mathcomp.solvable.primitive_action]
    stab_ntransitiveI [prf, in mathcomp.solvable.primitive_action]
    stab_semiprime [prf, in mathcomp.solvable.frobenius]
    stable [prf, in mathcomp.solvable.burnside_app]
    stable0mx [prf, in mathcomp.algebra.mxalgebra]
    stable_factor [def, in mathcomp.solvable.gseries]
    stableCmx [prf, in mathcomp.algebra.mxalgebra]
    stableDmx [prf, in mathcomp.algebra.mxalgebra]
    stablemx [abbrev, in mathcomp.algebra.mxalgebra]
    stablemx [abbrev, in mathcomp.algebra.mxalgebra]
    stablemx0 [prf, in mathcomp.algebra.mxalgebra]
    stablemx_comp [prf, in mathcomp.algebra.mxred]
    stablemx_comp [prf, in mathcomp.algebra.mxpoly]
    stablemx_full [prf, in mathcomp.algebra.mxalgebra]
    stablemx_restrict [prf, in mathcomp.algebra.mxred]
    stablemx_restrict [prf, in mathcomp.algebra.mxpoly]
    stablemx_row_base [prf, in mathcomp.algebra.mxalgebra]
    stablemx_sums [prf, in mathcomp.algebra.mxalgebra]
    stablemx_unit [prf, in mathcomp.algebra.mxalgebra]
    stablemxC [prf, in mathcomp.algebra.mxalgebra]
    stablemxD [prf, in mathcomp.algebra.mxalgebra]
    stablemxM [prf, in mathcomp.algebra.mxalgebra]
    stablemxN [prf, in mathcomp.algebra.mxalgebra]
    stableNmx [prf, in mathcomp.algebra.mxalgebra]
    StarMonoid [abbrev, in mathcomp.boot.monoid]
    StarMonoid [mod, in mathcomp.boot.monoid]
    StarMonoid.axioms_ [rec, in mathcomp.boot.monoid]
    StarMonoid.choice_hasChoice_mixin [proj, in mathcomp.boot.monoid]
    StarMonoid.class [proj, in mathcomp.boot.monoid]
    StarMonoid.clone [abbrev, in mathcomp.boot.monoid]
    StarMonoid.copy [abbrev, in mathcomp.boot.monoid]
    StarMonoid.eqtype_hasDecEq_mixin [proj, in mathcomp.boot.monoid]
    StarMonoid.Exports [mod, in mathcomp.boot.monoid]
    StarMonoid.Exports.join_monoid_StarMonoid_between_monoid_BaseGroup_and_choice_Choice [def, in mathcomp.boot.monoid]
    StarMonoid.Exports.join_monoid_StarMonoid_between_monoid_BaseGroup_and_eqtype_Equality [def, in mathcomp.boot.monoid]
    StarMonoid.Exports.join_monoid_StarMonoid_between_monoid_BaseGroup_and_monoid_ChoiceBaseUMagma [def, in mathcomp.boot.monoid]
    StarMonoid.Exports.join_monoid_StarMonoid_between_monoid_BaseGroup_and_monoid_ChoiceMagma [def, in mathcomp.boot.monoid]
    StarMonoid.Exports.join_monoid_StarMonoid_between_monoid_BaseGroup_and_monoid_Monoid [def, in mathcomp.boot.monoid]
    StarMonoid.Exports.join_monoid_StarMonoid_between_monoid_BaseGroup_and_monoid_Semigroup [def, in mathcomp.boot.monoid]
    StarMonoid.Exports.join_monoid_StarMonoid_between_monoid_BaseGroup_and_monoid_UMagma [def, in mathcomp.boot.monoid]
    StarMonoid.Exports.starMonoidType [abbrev, in mathcomp.boot.monoid]
    StarMonoid.monoid_BaseUMagma_isUMagma_mixin [proj, in mathcomp.boot.monoid]
    StarMonoid.monoid_hasInv_mixin [proj, in mathcomp.boot.monoid]
    StarMonoid.monoid_hasMul_mixin [proj, in mathcomp.boot.monoid]
    StarMonoid.monoid_hasOne_mixin [proj, in mathcomp.boot.monoid]
    StarMonoid.monoid_Magma_isSemigroup_mixin [proj, in mathcomp.boot.monoid]
    StarMonoid.monoid_Monoid_isStarMonoid_mixin [proj, in mathcomp.boot.monoid]
    StarMonoid.on [abbrev, in mathcomp.boot.monoid]
    StarMonoid.on_ [abbrev, in mathcomp.boot.monoid]
    StarMonoid.pack_ [def, in mathcomp.boot.monoid]
    StarMonoid.phant_clone [def, in mathcomp.boot.monoid]
    StarMonoid.phant_on_ [def, in mathcomp.boot.monoid]
    StarMonoid.sort [proj, in mathcomp.boot.monoid]
    StarMonoid.type [rec, in mathcomp.boot.monoid]
    StarMonoid_isGroup [abbrev, in mathcomp.boot.monoid]
    StarMonoid_isGroup [mod, in mathcomp.boot.monoid]
    StarMonoid_isGroup.axioms [abbrev, in mathcomp.boot.monoid]
    StarMonoid_isGroup.axioms_ [rec, in mathcomp.boot.monoid]
    StarMonoid_isGroup.Build [abbrev, in mathcomp.boot.monoid]
    StarMonoid_isGroup.Exports [mod, in mathcomp.boot.monoid]
    StarMonoid_isGroup.identity_builder [def, in mathcomp.boot.monoid]
    StarMonoid_isGroup.mulVg [proj, in mathcomp.boot.monoid]
    StarMonoid_isGroup.phant_axioms [def, in mathcomp.boot.monoid]
    StarMonoid_isGroup.phant_Build [def, in mathcomp.boot.monoid]
    StarMonoidElpiOperations [mod, in mathcomp.boot.monoid]
    start_with [def, in mathcomp.classical.classical_orders]
    start_with_prefix [prf, in mathcomp.classical.classical_orders]
    strace [def, in mathcomp.analysis.measure_theory.measurable_structure]
    strace_sigma_ring [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    Streicher_K_ [def, in mathcomp.classical.internal_Eqdep_dec]
    Streicher_K__eq_rect_eq [prf, in mathcomp.classical.internal_Eqdep_dec]
    Streicher_K_on_ [def, in mathcomp.classical.internal_Eqdep_dec]
    Streicher_K_on__eq_rect_eq_on [prf, in mathcomp.classical.internal_Eqdep_dec]
    strict_adjunction [prf, in mathcomp.boot.fingraph]
    strict_monotonic [def, in mathcomp.classical.unstable]
    strict_monotonicW [prf, in mathcomp.classical.unstable]
    strictly_dominated_by [def, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
    strictly_dominated_by1 [prf, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
    strong_Primitive_Element_Theorem [prf, in mathcomp.field.separable]
    strongest_coprime_quotient_cent [prf, in mathcomp.solvable.hall]
    StrongJordanHolderUniqueness [prf, in mathcomp.solvable.jordanholder]
    Sub [abbrev, in mathcomp.boot.eqtype]
    Sub [def, in mathcomp.boot.eqtype]
    sub0e [prf, in mathcomp.reals.constructive_ereal]
    sub0mx [prf, in mathcomp.algebra.mxalgebra]
    sub0n [prf, in mathcomp.boot.ssrnat]
    sub0seq [prf, in mathcomp.boot.seq]
    sub0set [prf, in mathcomp.classical.classical_sets]
    sub0set [prf, in mathcomp.boot.finset]
    sub0v [prf, in mathcomp.algebra.vector]
    sub1_agenv [prf, in mathcomp.field.falgebra]
    sub1_scale_ball [prf, in mathcomp.analysis.normedtype_theory.vitali_lemma]
    sub1b [prf, in mathcomp.boot.ssrnat]
    sub1G [prf, in mathcomp.finite_group.fingroup]
    sub1mx [prf, in mathcomp.algebra.mxalgebra]
    sub1seq [prf, in mathcomp.boot.seq]
    sub1set [prf, in mathcomp.classical.classical_sets]
    sub1set [prf, in mathcomp.boot.finset]
    sub1v [prf, in mathcomp.field.fieldext]
    sub_abelian_cent [prf, in mathcomp.finite_group.fingroup]
    sub_abelian_cent2 [prf, in mathcomp.finite_group.fingroup]
    sub_abelian_norm [prf, in mathcomp.finite_group.fingroup]
    sub_abelian_normal [prf, in mathcomp.finite_group.fingroup]
    sub_act_proof [prf, in mathcomp.finite_group.action]
    sub_adds_genmx_ortho [prf, in mathcomp.algebra.spectral]
    sub_addsmxP [prf, in mathcomp.algebra.mxalgebra]
    sub_adjoin1v [prf, in mathcomp.field.fieldext]
    sub_adjoin_separable_generator [prf, in mathcomp.field.separable]
    sub_ae_eq2 [inst, in mathcomp.analysis.measure_theory.measure_negligible]
    sub_afixRs_norm [prf, in mathcomp.finite_group.action]
    sub_afixRs_norms [prf, in mathcomp.finite_group.action]
    sub_agenv [prf, in mathcomp.field.falgebra]
    sub_all [prf, in mathcomp.boot.seq]
    sub_allrel [prf, in mathcomp.boot.seq]
    sub_annihilant [def, in mathcomp.algebra.polyXY]
    sub_annihilant_in_ideal [prf, in mathcomp.algebra.polyXY]
    sub_annihilant_neq0 [prf, in mathcomp.algebra.polyXY]
    sub_annihilantP [prf, in mathcomp.algebra.polyXY]
    sub_astab1 [prf, in mathcomp.finite_group.action]
    sub_astab1_in [prf, in mathcomp.finite_group.action]
    sub_astabQ [prf, in mathcomp.finite_group.action]
    sub_astabQR [prf, in mathcomp.finite_group.action]
    sub_baseField [prf, in mathcomp.field.fieldext]
    sub_bigcap [prf, in mathcomp.classical.classical_sets]
    sub_bigcapmxP [prf, in mathcomp.algebra.mxalgebra]
    sub_boundedl [prf, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
    sub_boundedr [prf, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
    sub_capmx [prf, in mathcomp.algebra.mxalgebra]
    sub_capmx_gen [prf, in mathcomp.algebra.mxalgebra]
    sub_caratheodory [prf, in mathcomp.analysis.measure_theory.measure_extension]
    sub_cent1 [prf, in mathcomp.finite_group.fingroup]
    sub_center_normal [prf, in mathcomp.solvable.center]
    sub_class_support [prf, in mathcomp.finite_group.fingroup]
    sub_cofinite_set [prf, in mathcomp.classical.cardinality]
    sub_conjg [prf, in mathcomp.finite_group.fingroup]
    sub_conjgV [prf, in mathcomp.finite_group.fingroup]
    sub_continuous [prf, in mathcomp.analysis.normedtype_theory.tvs]
    sub_cosetpre [prf, in mathcomp.finite_group.quotient]
    sub_cosetpre_quo [prf, in mathcomp.finite_group.quotient]
    sub_count [prf, in mathcomp.boot.seq]
    sub_countable [prf, in mathcomp.classical.cardinality]
    sub_cycle [prf, in mathcomp.boot.path]
    sub_cyclic_char [prf, in mathcomp.solvable.cyclic]
    sub_daddsmx [prf, in mathcomp.algebra.mxalgebra]
    sub_daddsmx_spec [ind, in mathcomp.algebra.mxalgebra]
    sub_der1_abelian [prf, in mathcomp.solvable.commutator]
    sub_der1_norm [prf, in mathcomp.solvable.commutator]
    sub_der1_normal [prf, in mathcomp.solvable.commutator]
    sub_dominatedl [prf, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
    sub_dominatedr [prf, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
    sub_double_eseries [prf, in mathcomp.analysis.sequences]
    sub_double_series [prf, in mathcomp.analysis.sequences]
    sub_dsumsmx [prf, in mathcomp.algebra.mxalgebra]
    sub_dsumsmx_spec [ind, in mathcomp.algebra.mxalgebra]
    sub_eigenspace_conjmx [prf, in mathcomp.algebra.mxred]
    sub_eigenspace_conjmx [prf, in mathcomp.algebra.mxpoly]
    sub_eseries [prf, in mathcomp.analysis.sequences]
    sub_eseries_geq [prf, in mathcomp.analysis.sequences]
    sub_find [prf, in mathcomp.boot.seq]
    sub_finite_set [prf, in mathcomp.classical.cardinality]
    sub_fun [def, in mathcomp.finmap.finmap]
    sub_g_sigma_ring [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    sub_gcore [prf, in mathcomp.finite_group.fingroup]
    sub_gen [prf, in mathcomp.finite_group.fingroup]
    sub_gen_smallest [prf, in mathcomp.classical.classical_sets]
    sub_Hall_pcore [prf, in mathcomp.solvable.pgroup]
    sub_has [prf, in mathcomp.boot.seq]
    sub_im_coset [prf, in mathcomp.finite_group.quotient]
    sub_image_setI [prf, in mathcomp.classical.classical_sets]
    sub_image_some [prf, in mathcomp.classical.classical_sets]
    sub_image_someP [prf, in mathcomp.classical.classical_sets]
    sub_imset_pre [prf, in mathcomp.boot.finset]
    sub_in_allrel [prf, in mathcomp.boot.seq]
    sub_in_constt [prf, in mathcomp.solvable.pgroup]
    sub_in_cycle [prf, in mathcomp.boot.path]
    sub_in_le_big [prf, in mathcomp.boot.bigop]
    sub_in_pairwise [prf, in mathcomp.boot.seq]
    sub_in_partn [prf, in mathcomp.boot.prime]
    sub_in_path [prf, in mathcomp.boot.path]
    sub_in_pcore [prf, in mathcomp.solvable.pgroup]
    sub_in_pnat [prf, in mathcomp.boot.prime]
    sub_in_sorted [prf, in mathcomp.boot.path]
    sub_infinite_set [prf, in mathcomp.classical.cardinality]
    sub_inseparable [prf, in mathcomp.field.separable]
    sub_isog [prf, in mathcomp.finite_group.morphism]
    sub_isom [prf, in mathcomp.finite_group.morphism]
    sub_kermx [prf, in mathcomp.algebra.mxalgebra]
    sub_kermxP [prf, in mathcomp.algebra.mxalgebra]
    sub_kermxpoly_conjmx [prf, in mathcomp.algebra.mxred]
    sub_kermxpoly_conjmx [prf, in mathcomp.algebra.mxpoly]
    sub_klipschitz [prf, in mathcomp.analysis.normedtype_theory.normed_module]
    sub_lcoset [prf, in mathcomp.finite_group.fingroup]
    sub_lcosetV [prf, in mathcomp.finite_group.fingroup]
    sub_Ldiv [prf, in mathcomp.solvable.abelian]
    sub_LdivT [prf, in mathcomp.solvable.abelian]
    sub_le_big [prf, in mathcomp.boot.bigop]
    sub_le_big_seq [prf, in mathcomp.boot.bigop]
    sub_le_big_seq_cond [prf, in mathcomp.boot.bigop]
    sub_Lfun_finLfun [prf, in mathcomp.analysis.hoelder]
    sub_Lfun_mfun [prf, in mathcomp.analysis.hoelder]
    sub_lipschitz [prf, in mathcomp.analysis.normedtype_theory.normed_module]
    sub_ltmx_trans [prf, in mathcomp.algebra.mxalgebra]
    sub_map [prf, in mathcomp.boot.seq]
    sub_meets [prf, in mathcomp.classical.classical_sets]
    sub_morphim_pre [prf, in mathcomp.finite_group.morphism]
    sub_morphpre_im [prf, in mathcomp.finite_group.morphism]
    sub_morphpre_injm [prf, in mathcomp.finite_group.morphism]
    sub_nilpotent_cent2 [prf, in mathcomp.solvable.sylow]
    sub_normal_Hall [prf, in mathcomp.solvable.pgroup]
    sub_ord [def, in mathcomp.boot.fintype]
    sub_ord_proof [prf, in mathcomp.boot.fintype]
    sub_ordK [prf, in mathcomp.boot.fintype]
    sub_orthonormal [prf, in mathcomp.algebra.sesquilinear]
    sub_p_elt [prf, in mathcomp.solvable.pgroup]
    sub_pairwise [prf, in mathcomp.boot.seq]
    sub_pairwise_orthogonal [prf, in mathcomp.algebra.sesquilinear]
    sub_path [prf, in mathcomp.boot.path]
    sub_pcore [prf, in mathcomp.solvable.pgroup]
    sub_pgroup [prf, in mathcomp.solvable.pgroup]
    sub_pHall [prf, in mathcomp.solvable.pgroup]
    sub_pnat_coprime [prf, in mathcomp.boot.prime]
    sub_proper_trans [prf, in mathcomp.boot.fintype]
    sub_quotient_pre [prf, in mathcomp.finite_group.quotient]
    sub_rcoset [prf, in mathcomp.finite_group.fingroup]
    sub_rcosetV [prf, in mathcomp.finite_group.fingroup]
    Sub_rect [def, in mathcomp.boot.eqtype]
    sub_Rhull [prf, in mathcomp.analysis.normedtype_theory.normed_module]
    sub_rVP [prf, in mathcomp.algebra.mxalgebra]
    sub_scale_ball [prf, in mathcomp.analysis.normedtype_theory.vitali_lemma]
    sub_series [prf, in mathcomp.analysis.sequences]
    sub_series_geq [prf, in mathcomp.analysis.sequences]
    sub_setP [prf, in mathcomp.classical.cardinality]
    sub_setring [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    sub_setring2 [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    sub_sfun_fimfun [prf, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
    sub_sfun_mfun [prf, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
    sub_sigma_algebra [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    sub_sigma_algebra2 [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    sub_smallest [prf, in mathcomp.classical.classical_sets]
    sub_smallest2l [prf, in mathcomp.classical.classical_sets]
    sub_smallest2r [prf, in mathcomp.classical.classical_sets]
    sub_sorted [prf, in mathcomp.boot.path]
    sub_span [prf, in mathcomp.algebra.vector]
    Sub_spec [ind, in mathcomp.boot.eqtype]
    sub_sums_genmxP [prf, in mathcomp.algebra.mxalgebra]
    sub_sumsmxP [prf, in mathcomp.algebra.mxalgebra]
    sub_trivIset [prf, in mathcomp.classical.classical_sets]
    sub_type [def, in mathcomp.boot.eqtype]
    sub_unif_continuous [prf, in mathcomp.analysis.normedtype_theory.tvs]
    sub_within [prf, in mathcomp.classical.wochoice]
    sub_Zp_1 [prf, in mathcomp.algebra.zmodp]
    subact [def, in mathcomp.finite_group.action]
    subact_dom [def, in mathcomp.finite_group.action]
    subact_dom_group [def, in mathcomp.finite_group.action]
    subact_is_action [prf, in mathcomp.finite_group.action]
    subaction [def, in mathcomp.finite_group.action]
    subadditive [def, in mathcomp.analysis.measure_theory.measure_function]
    subAlgType [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
    SubBaseUMagma [abbrev, in mathcomp.boot.monoid]
    SubBaseUMagma [mod, in mathcomp.boot.monoid]
    SubBaseUMagma.axioms_ [rec, in mathcomp.boot.monoid]
    SubBaseUMagma.choice_hasChoice_mixin [proj, in mathcomp.boot.monoid]
    SubBaseUMagma.class [proj, in mathcomp.boot.monoid]
    SubBaseUMagma.clone [abbrev, in mathcomp.boot.monoid]
    SubBaseUMagma.copy [abbrev, in mathcomp.boot.monoid]
    SubBaseUMagma.eqtype_hasDecEq_mixin [proj, in mathcomp.boot.monoid]
    SubBaseUMagma.eqtype_isSub_mixin [proj, in mathcomp.boot.monoid]
    SubBaseUMagma.Exports [mod, in mathcomp.boot.monoid]
    SubBaseUMagma.Exports.join_monoid_SubBaseUMagma_between_monoid_BaseUMagma_and_choice_SubChoice [def, in mathcomp.boot.monoid]
    SubBaseUMagma.Exports.join_monoid_SubBaseUMagma_between_monoid_BaseUMagma_and_eqtype_SubEquality [def, in mathcomp.boot.monoid]
    SubBaseUMagma.Exports.join_monoid_SubBaseUMagma_between_monoid_BaseUMagma_and_eqtype_SubType [def, in mathcomp.boot.monoid]
    SubBaseUMagma.Exports.join_monoid_SubBaseUMagma_between_monoid_BaseUMagma_and_monoid_SubMagma [def, in mathcomp.boot.monoid]
    SubBaseUMagma.Exports.join_monoid_SubBaseUMagma_between_monoid_ChoiceBaseUMagma_and_choice_SubChoice [def, in mathcomp.boot.monoid]
    SubBaseUMagma.Exports.join_monoid_SubBaseUMagma_between_monoid_ChoiceBaseUMagma_and_eqtype_SubEquality [def, in mathcomp.boot.monoid]
    SubBaseUMagma.Exports.join_monoid_SubBaseUMagma_between_monoid_ChoiceBaseUMagma_and_eqtype_SubType [def, in mathcomp.boot.monoid]
    SubBaseUMagma.Exports.join_monoid_SubBaseUMagma_between_monoid_ChoiceBaseUMagma_and_monoid_SubMagma [def, in mathcomp.boot.monoid]
    SubBaseUMagma.Exports.subBaseUMagmaType [abbrev, in mathcomp.boot.monoid]
    SubBaseUMagma.monoid_hasMul_mixin [proj, in mathcomp.boot.monoid]
    SubBaseUMagma.monoid_hasOne_mixin [proj, in mathcomp.boot.monoid]
    SubBaseUMagma.monoid_isSubBaseUMagma_mixin [proj, in mathcomp.boot.monoid]
    SubBaseUMagma.monoid_isSubMagma_mixin [proj, in mathcomp.boot.monoid]
    SubBaseUMagma.on [abbrev, in mathcomp.boot.monoid]
    SubBaseUMagma.on_ [abbrev, in mathcomp.boot.monoid]
    SubBaseUMagma.pack_ [def, in mathcomp.boot.monoid]
    SubBaseUMagma.phant_clone [def, in mathcomp.boot.monoid]
    SubBaseUMagma.phant_on_ [def, in mathcomp.boot.monoid]
    SubBaseUMagma.sort [proj, in mathcomp.boot.monoid]
    SubBaseUMagma.type [rec, in mathcomp.boot.monoid]
    SubBaseUMagmaElpiOperations [mod, in mathcomp.boot.monoid]
    subBnAC [prf, in mathcomp.boot.ssrnat]
    subcent1_cycle_norm [prf, in mathcomp.solvable.center]
    subcent1_cycle_normal [prf, in mathcomp.solvable.center]
    subcent1_cycle_sub [prf, in mathcomp.solvable.center]
    subcent1_extraspecial_maximal [prf, in mathcomp.solvable.maximal]
    subcent1_id [prf, in mathcomp.solvable.center]
    subcent1_sub [prf, in mathcomp.solvable.center]
    subcent1C [prf, in mathcomp.solvable.center]
    subcent1P [prf, in mathcomp.solvable.center]
    subcent_char [prf, in mathcomp.solvable.center]
    subcent_dprod [prf, in mathcomp.finite_group.gproduct]
    subcent_norm [prf, in mathcomp.solvable.center]
    subcent_normal [prf, in mathcomp.solvable.center]
    subcent_sdprod [prf, in mathcomp.finite_group.gproduct]
    subcent_sub [prf, in mathcomp.solvable.center]
    subcent_TImulg [prf, in mathcomp.finite_group.gproduct]
    subcentP [prf, in mathcomp.solvable.center]
    SubChoice [abbrev, in mathcomp.boot.choice]
    SubChoice [mod, in mathcomp.boot.choice]
    SubChoice.axioms_ [rec, in mathcomp.boot.choice]
    SubChoice.choice_hasChoice_mixin [proj, in mathcomp.boot.choice]
    SubChoice.class [proj, in mathcomp.boot.choice]
    SubChoice.clone [abbrev, in mathcomp.boot.choice]
    SubChoice.copy [abbrev, in mathcomp.boot.choice]
    SubChoice.eqtype_hasDecEq_mixin [proj, in mathcomp.boot.choice]
    SubChoice.eqtype_isSub_mixin [proj, in mathcomp.boot.choice]
    SubChoice.Exports [mod, in mathcomp.boot.choice]
    SubChoice.Exports.join_choice_SubChoice_between_choice_Choice_and_eqtype_SubEquality [def, in mathcomp.boot.choice]
    SubChoice.Exports.join_choice_SubChoice_between_choice_Choice_and_eqtype_SubType [def, in mathcomp.boot.choice]
    SubChoice.Exports.subChoiceType [abbrev, in mathcomp.boot.choice]
    SubChoice.on [abbrev, in mathcomp.boot.choice]
    SubChoice.on_ [abbrev, in mathcomp.boot.choice]
    SubChoice.pack_ [def, in mathcomp.boot.choice]
    SubChoice.phant_clone [def, in mathcomp.boot.choice]
    SubChoice.phant_on_ [def, in mathcomp.boot.choice]
    SubChoice.sort [proj, in mathcomp.boot.choice]
    SubChoice.type [rec, in mathcomp.boot.choice]
    SubChoice_isSubGroup [abbrev, in mathcomp.boot.monoid]
    SubChoice_isSubGroup [mod, in mathcomp.boot.monoid]
    SubChoice_isSubGroup.axioms [abbrev, in mathcomp.boot.monoid]
    SubChoice_isSubGroup.axioms_ [rec, in mathcomp.boot.monoid]
    SubChoice_isSubGroup.Build [abbrev, in mathcomp.boot.monoid]
    SubChoice_isSubGroup.Exports [mod, in mathcomp.boot.monoid]
    SubChoice_isSubGroup.phant_axioms [def, in mathcomp.boot.monoid]
    SubChoice_isSubGroup.phant_Build [def, in mathcomp.boot.monoid]
    SubChoice_isSubMagma [abbrev, in mathcomp.boot.monoid]
    SubChoice_isSubMagma [mod, in mathcomp.boot.monoid]
    SubChoice_isSubMagma.axioms [abbrev, in mathcomp.boot.monoid]
    SubChoice_isSubMagma.axioms_ [rec, in mathcomp.boot.monoid]
    SubChoice_isSubMagma.Build [abbrev, in mathcomp.boot.monoid]
    SubChoice_isSubMagma.Exports [mod, in mathcomp.boot.monoid]
    SubChoice_isSubMagma.phant_axioms [def, in mathcomp.boot.monoid]
    SubChoice_isSubMagma.phant_Build [def, in mathcomp.boot.monoid]
    SubChoice_isSubMonoid [abbrev, in mathcomp.boot.monoid]
    SubChoice_isSubMonoid [mod, in mathcomp.boot.monoid]
    SubChoice_isSubMonoid.axioms [abbrev, in mathcomp.boot.monoid]
    SubChoice_isSubMonoid.axioms_ [rec, in mathcomp.boot.monoid]
    SubChoice_isSubMonoid.Build [abbrev, in mathcomp.boot.monoid]
    SubChoice_isSubMonoid.Exports [mod, in mathcomp.boot.monoid]
    SubChoice_isSubMonoid.phant_axioms [def, in mathcomp.boot.monoid]
    SubChoice_isSubMonoid.phant_Build [def, in mathcomp.boot.monoid]
    SubChoice_isSubSemigroup [abbrev, in mathcomp.boot.monoid]
    SubChoice_isSubSemigroup [mod, in mathcomp.boot.monoid]
    SubChoice_isSubSemigroup.axioms [abbrev, in mathcomp.boot.monoid]
    SubChoice_isSubSemigroup.axioms_ [rec, in mathcomp.boot.monoid]
    SubChoice_isSubSemigroup.Build [abbrev, in mathcomp.boot.monoid]
    SubChoice_isSubSemigroup.Exports [mod, in mathcomp.boot.monoid]
    SubChoice_isSubSemigroup.phant_axioms [def, in mathcomp.boot.monoid]
    SubChoice_isSubSemigroup.phant_Build [def, in mathcomp.boot.monoid]
    SubChoice_isSubUMagma [abbrev, in mathcomp.boot.monoid]
    SubChoice_isSubUMagma [mod, in mathcomp.boot.monoid]
    SubChoice_isSubUMagma.axioms [abbrev, in mathcomp.boot.monoid]
    SubChoice_isSubUMagma.axioms_ [rec, in mathcomp.boot.monoid]
    SubChoice_isSubUMagma.Build [abbrev, in mathcomp.boot.monoid]
    SubChoice_isSubUMagma.Exports [mod, in mathcomp.boot.monoid]
    SubChoice_isSubUMagma.phant_axioms [def, in mathcomp.boot.monoid]
    SubChoice_isSubUMagma.phant_Build [def, in mathcomp.boot.monoid]
    SubChoiceElpiOperations [mod, in mathcomp.boot.choice]
    subclosed_compact [prf, in mathcomp.analysis.topology_theory.compact]
    subComRingType [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
    subComSemiRingType [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
    SubCountable [abbrev, in mathcomp.boot.choice]
    SubCountable [mod, in mathcomp.boot.choice]
    SubCountable.axioms_ [rec, in mathcomp.boot.choice]
    SubCountable.choice_Choice_isCountable_mixin [proj, in mathcomp.boot.choice]
    SubCountable.choice_hasChoice_mixin [proj, in mathcomp.boot.choice]
    SubCountable.class [proj, in mathcomp.boot.choice]
    SubCountable.clone [abbrev, in mathcomp.boot.choice]
    SubCountable.copy [abbrev, in mathcomp.boot.choice]
    SubCountable.eqtype_hasDecEq_mixin [proj, in mathcomp.boot.choice]
    SubCountable.eqtype_isSub_mixin [proj, in mathcomp.boot.choice]
    SubCountable.Exports [mod, in mathcomp.boot.choice]
    SubCountable.Exports.join_choice_SubCountable_between_choice_Countable_and_choice_SubChoice [def, in mathcomp.boot.choice]
    SubCountable.Exports.join_choice_SubCountable_between_choice_Countable_and_eqtype_SubEquality [def, in mathcomp.boot.choice]
    SubCountable.Exports.join_choice_SubCountable_between_choice_Countable_and_eqtype_SubType [def, in mathcomp.boot.choice]
    SubCountable.Exports.subCountType [abbrev, in mathcomp.boot.choice]
    SubCountable.on [abbrev, in mathcomp.boot.choice]
    SubCountable.on_ [abbrev, in mathcomp.boot.choice]
    SubCountable.pack_ [def, in mathcomp.boot.choice]
    SubCountable.phant_clone [def, in mathcomp.boot.choice]
    SubCountable.phant_on_ [def, in mathcomp.boot.choice]
    SubCountable.sort [proj, in mathcomp.boot.choice]
    SubCountable.type [rec, in mathcomp.boot.choice]
    SubCountable_isFinite [abbrev, in mathcomp.boot.fintype]
    SubCountable_isFinite [mod, in mathcomp.boot.fintype]
    SubCountable_isFinite.axioms [abbrev, in mathcomp.boot.fintype]
    SubCountable_isFinite.axioms_ [rec, in mathcomp.boot.fintype]
    SubCountable_isFinite.Build [abbrev, in mathcomp.boot.fintype]
    SubCountable_isFinite.Exports [mod, in mathcomp.boot.fintype]
    SubCountable_isFinite.phant_axioms [def, in mathcomp.boot.fintype]
    SubCountable_isFinite.phant_Build [def, in mathcomp.boot.fintype]
    SubCountableElpiOperations [mod, in mathcomp.boot.choice]
    subCset [prf, in mathcomp.boot.finset]
    subD1set [prf, in mathcomp.boot.finset]
    SubDaddsmxSpec [constr, in mathcomp.algebra.mxalgebra]
    subDnAC [prf, in mathcomp.boot.ssrnat]
    subDnCA [prf, in mathcomp.boot.ssrnat]
    subDnCAC [prf, in mathcomp.boot.ssrnat]
    subdom [abbrev, in mathcomp.finite_group.action]
    subDset [prf, in mathcomp.boot.finset]
    subDsetl [prf, in mathcomp.classical.classical_sets]
    subDsetr [prf, in mathcomp.classical.classical_sets]
    SubDsumsmxSpec [constr, in mathcomp.algebra.mxalgebra]
    sube0 [prf, in mathcomp.reals.constructive_ereal]
    sube_cvg0 [prf, in mathcomp.analysis.normedtype_theory.normed_module]
    sube_eq [prf, in mathcomp.reals.constructive_ereal]
    sube_ge0 [prf, in mathcomp.reals.constructive_ereal]
    sube_gt0 [prf, in mathcomp.reals.constructive_ereal]
    sube_le0 [prf, in mathcomp.reals.constructive_ereal]
    sube_lt0 [prf, in mathcomp.reals.constructive_ereal]
    subee [prf, in mathcomp.reals.constructive_ereal]
    subEfproper [prf, in mathcomp.finmap.finmap]
    subeK [prf, in mathcomp.reals.constructive_ereal]
    subEproper [prf, in mathcomp.boot.finset]
    SubEquality [abbrev, in mathcomp.boot.eqtype]
    SubEquality [mod, in mathcomp.boot.eqtype]
    SubEquality.axioms_ [rec, in mathcomp.boot.eqtype]
    SubEquality.class [proj, in mathcomp.boot.eqtype]
    SubEquality.clone [abbrev, in mathcomp.boot.eqtype]
    SubEquality.copy [abbrev, in mathcomp.boot.eqtype]
    SubEquality.eqtype_hasDecEq_mixin [proj, in mathcomp.boot.eqtype]
    SubEquality.eqtype_isSub_mixin [proj, in mathcomp.boot.eqtype]
    SubEquality.Exports [mod, in mathcomp.boot.eqtype]
    SubEquality.Exports.join_eqtype_SubEquality_between_eqtype_Equality_and_eqtype_SubType [def, in mathcomp.boot.eqtype]
    SubEquality.Exports.subEqType [abbrev, in mathcomp.boot.eqtype]
    SubEquality.on [abbrev, in mathcomp.boot.eqtype]
    SubEquality.on_ [abbrev, in mathcomp.boot.eqtype]
    SubEquality.pack_ [def, in mathcomp.boot.eqtype]
    SubEquality.phant_clone [def, in mathcomp.boot.eqtype]
    SubEquality.phant_on_ [def, in mathcomp.boot.eqtype]
    SubEquality.sort [proj, in mathcomp.boot.eqtype]
    SubEquality.type [rec, in mathcomp.boot.eqtype]
    SubEqualityElpiOperations [mod, in mathcomp.boot.eqtype]
    suber_ge0 [prf, in mathcomp.reals.constructive_ereal]
    suber_lt0 [prf, in mathcomp.reals.constructive_ereal]
    subfext0 [def, in mathcomp.field.fieldext]
    subfext0_morph [def, in mathcomp.field.fieldext]
    subfext1 [def, in mathcomp.field.fieldext]
    subfext1_morph [def, in mathcomp.field.fieldext]
    subfext_add [def, in mathcomp.field.fieldext]
    subfext_inv [def, in mathcomp.field.fieldext]
    subfext_mul [def, in mathcomp.field.fieldext]
    subfext_opp [def, in mathcomp.field.fieldext]
    subFExtend [def, in mathcomp.field.fieldext]
    subfield_closed [prf, in mathcomp.field.fieldext]
    SubFieldExtType [def, in mathcomp.field.fieldext]
    SubFinite [abbrev, in mathcomp.boot.fintype]
    SubFinite [mod, in mathcomp.boot.fintype]
    SubFinite.axioms_ [rec, in mathcomp.boot.fintype]
    SubFinite.choice_Choice_isCountable_mixin [proj, in mathcomp.boot.fintype]
    SubFinite.choice_hasChoice_mixin [proj, in mathcomp.boot.fintype]
    SubFinite.class [proj, in mathcomp.boot.fintype]
    SubFinite.clone [abbrev, in mathcomp.boot.fintype]
    SubFinite.copy [abbrev, in mathcomp.boot.fintype]
    SubFinite.eqtype_hasDecEq_mixin [proj, in mathcomp.boot.fintype]
    SubFinite.eqtype_isSub_mixin [proj, in mathcomp.boot.fintype]
    SubFinite.Exports [mod, in mathcomp.boot.fintype]
    SubFinite.Exports.join_fintype_SubFinite_between_fintype_Finite_and_choice_SubChoice [def, in mathcomp.boot.fintype]
    SubFinite.Exports.join_fintype_SubFinite_between_fintype_Finite_and_choice_SubCountable [def, in mathcomp.boot.fintype]
    SubFinite.Exports.join_fintype_SubFinite_between_fintype_Finite_and_eqtype_SubEquality [def, in mathcomp.boot.fintype]
    SubFinite.Exports.join_fintype_SubFinite_between_fintype_Finite_and_eqtype_SubType [def, in mathcomp.boot.fintype]
    SubFinite.Exports.subFinType [abbrev, in mathcomp.boot.fintype]
    SubFinite.fintype_isFinite_mixin [proj, in mathcomp.boot.fintype]
    SubFinite.on [abbrev, in mathcomp.boot.fintype]
    SubFinite.on_ [abbrev, in mathcomp.boot.fintype]
    SubFinite.pack_ [def, in mathcomp.boot.fintype]
    SubFinite.phant_clone [def, in mathcomp.boot.fintype]
    SubFinite.phant_on_ [def, in mathcomp.boot.fintype]
    SubFinite.sort [proj, in mathcomp.boot.fintype]
    SubFinite.type [rec, in mathcomp.boot.fintype]
    SubFiniteElpiOperations [mod, in mathcomp.boot.fintype]
    subfinset_finpred [def, in mathcomp.finmap.finmap]
    subfun [def, in mathcomp.classical.functions]
    subfun_imageT [prf, in mathcomp.classical.functions]
    subfun_inj [prf, in mathcomp.classical.functions]
    subfx_eval [def, in mathcomp.field.fieldext]
    subfx_eval_is_additive [def, in mathcomp.field.fieldext]
    subfx_eval_is_monoid_morphism [prf, in mathcomp.field.fieldext]
    subfx_eval_is_multiplicative [def, in mathcomp.field.fieldext]
    subfx_eval_is_zmod_morphism [prf, in mathcomp.field.fieldext]
    subfx_eval_morph [def, in mathcomp.field.fieldext]
    subfx_evalZ [prf, in mathcomp.field.fieldext]
    subfx_fieldAxiom [prf, in mathcomp.field.fieldext]
    subfx_inj [def, in mathcomp.field.fieldext]
    subfx_inj_base [prf, in mathcomp.field.fieldext]
    subfx_inj_eval [prf, in mathcomp.field.fieldext]
    subfx_inj_is_additive [def, in mathcomp.field.fieldext]
    subfx_inj_is_monoid_morphism [prf, in mathcomp.field.fieldext]
    subfx_inj_is_multiplicative [def, in mathcomp.field.fieldext]
    subfx_inj_is_zmod_morphism [prf, in mathcomp.field.fieldext]
    subfx_inj_root [prf, in mathcomp.field.fieldext]
    subfx_injZ [prf, in mathcomp.field.fieldext]
    subfx_inv0 [prf, in mathcomp.field.fieldext]
    subfx_inv_rep [def, in mathcomp.field.fieldext]
    subfx_irreducibleP [prf, in mathcomp.field.fieldext]
    subfx_mul_rep [def, in mathcomp.field.fieldext]
    subfx_poly_inv [def, in mathcomp.field.fieldext]
    subfx_root [def, in mathcomp.field.fieldext]
    subfx_scale [def, in mathcomp.field.fieldext]
    subfx_scaleAl [prf, in mathcomp.field.fieldext]
    subfx_scaler1r [prf, in mathcomp.field.fieldext]
    subfx_scalerA [prf, in mathcomp.field.fieldext]
    subfx_scalerDl [prf, in mathcomp.field.fieldext]
    subfx_scalerDr [prf, in mathcomp.field.fieldext]
    subfxE [prf, in mathcomp.field.fieldext]
    subfxEroot [prf, in mathcomp.field.fieldext]
    SubfxVect [def, in mathcomp.field.fieldext]
    subg [def, in mathcomp.finite_group.fingroup]
    Subg [constr, in mathcomp.finite_group.fingroup]
    subG1 [prf, in mathcomp.finite_group.fingroup]
    subG1_contra [prf, in mathcomp.finite_group.fingroup]
    subg_default [prf, in mathcomp.finite_group.fingroup]
    subg_inj [prf, in mathcomp.finite_group.fingroup]
    subg_inv [def, in mathcomp.finite_group.fingroup]
    subg_invP [prf, in mathcomp.finite_group.fingroup]
    subg_morphism [def, in mathcomp.finite_group.morphism]
    subg_mul [def, in mathcomp.finite_group.fingroup]
    subg_mulP [prf, in mathcomp.finite_group.fingroup]
    subg_of [ind, in mathcomp.finite_group.fingroup]
    subg_of_ind [scheme, in mathcomp.finite_group.fingroup]
    subg_of_rec [scheme, in mathcomp.finite_group.fingroup]
    subg_of_rect [scheme, in mathcomp.finite_group.fingroup]
    subg_of_sind [scheme, in mathcomp.finite_group.fingroup]
    subg_of_Sub [def, in mathcomp.finite_group.fingroup]
    subg_one [def, in mathcomp.finite_group.fingroup]
    subg_oneP [prf, in mathcomp.finite_group.fingroup]
    subgacent1E [prf, in mathcomp.finite_group.action]
    subgacentE [prf, in mathcomp.finite_group.action]
    subgK [prf, in mathcomp.finite_group.fingroup]
    subgM [prf, in mathcomp.finite_group.fingroup]
    subgmK [prf, in mathcomp.finite_group.morphism]
    subgP [prf, in mathcomp.finite_group.fingroup]
    SubGroup [abbrev, in mathcomp.boot.monoid]
    SubGroup [mod, in mathcomp.boot.monoid]
    SubGroup.axioms_ [rec, in mathcomp.boot.monoid]
    SubGroup.choice_hasChoice_mixin [proj, in mathcomp.boot.monoid]
    SubGroup.class [proj, in mathcomp.boot.monoid]
    SubGroup.clone [abbrev, in mathcomp.boot.monoid]
    SubGroup.copy [abbrev, in mathcomp.boot.monoid]
    SubGroup.eqtype_hasDecEq_mixin [proj, in mathcomp.boot.monoid]
    SubGroup.eqtype_isSub_mixin [proj, in mathcomp.boot.monoid]
    SubGroup.Exports [mod, in mathcomp.boot.monoid]
    SubGroup.Exports.join_monoid_SubGroup_between_monoid_BaseGroup_and_choice_SubChoice [def, in mathcomp.boot.monoid]
    SubGroup.Exports.join_monoid_SubGroup_between_monoid_BaseGroup_and_eqtype_SubEquality [def, in mathcomp.boot.monoid]
    SubGroup.Exports.join_monoid_SubGroup_between_monoid_BaseGroup_and_eqtype_SubType [def, in mathcomp.boot.monoid]
    SubGroup.Exports.join_monoid_SubGroup_between_monoid_BaseGroup_and_monoid_SubBaseUMagma [def, in mathcomp.boot.monoid]
    SubGroup.Exports.join_monoid_SubGroup_between_monoid_BaseGroup_and_monoid_SubMagma [def, in mathcomp.boot.monoid]
    SubGroup.Exports.join_monoid_SubGroup_between_monoid_BaseGroup_and_monoid_SubMonoid [def, in mathcomp.boot.monoid]
    SubGroup.Exports.join_monoid_SubGroup_between_monoid_BaseGroup_and_monoid_SubSemigroup [def, in mathcomp.boot.monoid]
    SubGroup.Exports.join_monoid_SubGroup_between_monoid_BaseGroup_and_monoid_SubUMagma [def, in mathcomp.boot.monoid]
    SubGroup.Exports.join_monoid_SubGroup_between_monoid_Group_and_choice_SubChoice [def, in mathcomp.boot.monoid]
    SubGroup.Exports.join_monoid_SubGroup_between_monoid_Group_and_eqtype_SubEquality [def, in mathcomp.boot.monoid]
    SubGroup.Exports.join_monoid_SubGroup_between_monoid_Group_and_eqtype_SubType [def, in mathcomp.boot.monoid]
    SubGroup.Exports.join_monoid_SubGroup_between_monoid_Group_and_monoid_SubBaseUMagma [def, in mathcomp.boot.monoid]
    SubGroup.Exports.join_monoid_SubGroup_between_monoid_Group_and_monoid_SubMagma [def, in mathcomp.boot.monoid]
    SubGroup.Exports.join_monoid_SubGroup_between_monoid_Group_and_monoid_SubMonoid [def, in mathcomp.boot.monoid]
    SubGroup.Exports.join_monoid_SubGroup_between_monoid_Group_and_monoid_SubSemigroup [def, in mathcomp.boot.monoid]
    SubGroup.Exports.join_monoid_SubGroup_between_monoid_Group_and_monoid_SubUMagma [def, in mathcomp.boot.monoid]
    SubGroup.Exports.join_monoid_SubGroup_between_monoid_StarMonoid_and_choice_SubChoice [def, in mathcomp.boot.monoid]
    SubGroup.Exports.join_monoid_SubGroup_between_monoid_StarMonoid_and_eqtype_SubEquality [def, in mathcomp.boot.monoid]
    SubGroup.Exports.join_monoid_SubGroup_between_monoid_StarMonoid_and_eqtype_SubType [def, in mathcomp.boot.monoid]
    SubGroup.Exports.join_monoid_SubGroup_between_monoid_StarMonoid_and_monoid_SubBaseUMagma [def, in mathcomp.boot.monoid]
    SubGroup.Exports.join_monoid_SubGroup_between_monoid_StarMonoid_and_monoid_SubMagma [def, in mathcomp.boot.monoid]
    SubGroup.Exports.join_monoid_SubGroup_between_monoid_StarMonoid_and_monoid_SubMonoid [def, in mathcomp.boot.monoid]
    SubGroup.Exports.join_monoid_SubGroup_between_monoid_StarMonoid_and_monoid_SubSemigroup [def, in mathcomp.boot.monoid]
    SubGroup.Exports.join_monoid_SubGroup_between_monoid_StarMonoid_and_monoid_SubUMagma [def, in mathcomp.boot.monoid]
    SubGroup.Exports.subGroupType [abbrev, in mathcomp.boot.monoid]
    SubGroup.monoid_BaseUMagma_isUMagma_mixin [proj, in mathcomp.boot.monoid]
    SubGroup.monoid_hasInv_mixin [proj, in mathcomp.boot.monoid]
    SubGroup.monoid_hasMul_mixin [proj, in mathcomp.boot.monoid]
    SubGroup.monoid_hasOne_mixin [proj, in mathcomp.boot.monoid]
    SubGroup.monoid_isSubBaseUMagma_mixin [proj, in mathcomp.boot.monoid]
    SubGroup.monoid_isSubMagma_mixin [proj, in mathcomp.boot.monoid]
    SubGroup.monoid_Magma_isSemigroup_mixin [proj, in mathcomp.boot.monoid]
    SubGroup.monoid_Monoid_isStarMonoid_mixin [proj, in mathcomp.boot.monoid]
    SubGroup.monoid_StarMonoid_isGroup_mixin [proj, in mathcomp.boot.monoid]
    SubGroup.on [abbrev, in mathcomp.boot.monoid]
    SubGroup.on_ [abbrev, in mathcomp.boot.monoid]
    SubGroup.pack_ [def, in mathcomp.boot.monoid]
    SubGroup.phant_clone [def, in mathcomp.boot.monoid]
    SubGroup.phant_on_ [def, in mathcomp.boot.monoid]
    SubGroup.sort [proj, in mathcomp.boot.monoid]
    SubGroup.type [rec, in mathcomp.boot.monoid]
    subgroup_transitiveP [prf, in mathcomp.finite_group.action]
    subgroup_transitivePin [prf, in mathcomp.finite_group.action]
    SubGroupElpiOperations [mod, in mathcomp.boot.monoid]
    subgroups [def, in mathcomp.finite_group.fingroup]
    subHall_Hall [prf, in mathcomp.solvable.pgroup]
    subHall_Sylow [prf, in mathcomp.solvable.pgroup]
    subimageK [prf, in mathcomp.classical.classical_sets]
    subIset [prf, in mathcomp.classical.classical_sets]
    subIset [prf, in mathcomp.boot.finset]
    subIsetl [prf, in mathcomp.classical.classical_sets]
    subIsetr [prf, in mathcomp.classical.classical_sets]
    subitv [def, in mathcomp.algebra.interval]
    subitv_anti [prf, in mathcomp.algebra.interval]
    subitv_refl [prf, in mathcomp.algebra.interval]
    subitv_trans [prf, in mathcomp.algebra.interval]
    subitvE [prf, in mathcomp.algebra.interval]
    subitvP [prf, in mathcomp.algebra.interval]
    subitvPl [prf, in mathcomp.algebra.interval]
    subitvPr [prf, in mathcomp.algebra.interval]
    SubK [prf, in mathcomp.boot.eqtype]
    subKimage [prf, in mathcomp.classical.classical_sets]
    subKn [prf, in mathcomp.boot.ssrnat]
    subl_surj [prf, in mathcomp.classical.functions]
    subLalgType [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
    subLSemiAlgType [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
    SubMagma [abbrev, in mathcomp.boot.monoid]
    SubMagma [mod, in mathcomp.boot.monoid]
    SubMagma.axioms_ [rec, in mathcomp.boot.monoid]
    SubMagma.choice_hasChoice_mixin [proj, in mathcomp.boot.monoid]
    SubMagma.class [proj, in mathcomp.boot.monoid]
    SubMagma.clone [abbrev, in mathcomp.boot.monoid]
    SubMagma.copy [abbrev, in mathcomp.boot.monoid]
    SubMagma.eqtype_hasDecEq_mixin [proj, in mathcomp.boot.monoid]
    SubMagma.eqtype_isSub_mixin [proj, in mathcomp.boot.monoid]
    SubMagma.Exports [mod, in mathcomp.boot.monoid]
    SubMagma.Exports.join_monoid_SubMagma_between_monoid_ChoiceMagma_and_choice_SubChoice [def, in mathcomp.boot.monoid]
    SubMagma.Exports.join_monoid_SubMagma_between_monoid_ChoiceMagma_and_eqtype_SubEquality [def, in mathcomp.boot.monoid]
    SubMagma.Exports.join_monoid_SubMagma_between_monoid_ChoiceMagma_and_eqtype_SubType [def, in mathcomp.boot.monoid]
    SubMagma.Exports.join_monoid_SubMagma_between_monoid_Magma_and_choice_SubChoice [def, in mathcomp.boot.monoid]
    SubMagma.Exports.join_monoid_SubMagma_between_monoid_Magma_and_eqtype_SubEquality [def, in mathcomp.boot.monoid]
    SubMagma.Exports.join_monoid_SubMagma_between_monoid_Magma_and_eqtype_SubType [def, in mathcomp.boot.monoid]
    SubMagma.Exports.subMagmaType [abbrev, in mathcomp.boot.monoid]
    SubMagma.monoid_hasMul_mixin [proj, in mathcomp.boot.monoid]
    SubMagma.monoid_isSubMagma_mixin [proj, in mathcomp.boot.monoid]
    SubMagma.on [abbrev, in mathcomp.boot.monoid]
    SubMagma.on_ [abbrev, in mathcomp.boot.monoid]
    SubMagma.pack_ [def, in mathcomp.boot.monoid]
    SubMagma.phant_clone [def, in mathcomp.boot.monoid]
    SubMagma.phant_on_ [def, in mathcomp.boot.monoid]
    SubMagma.sort [proj, in mathcomp.boot.monoid]
    SubMagma.type [rec, in mathcomp.boot.monoid]
    SubMagmaElpiOperations [mod, in mathcomp.boot.monoid]
    SubMonoid [abbrev, in mathcomp.boot.monoid]
    SubMonoid [mod, in mathcomp.boot.monoid]
    SubMonoid.axioms_ [rec, in mathcomp.boot.monoid]
    SubMonoid.choice_hasChoice_mixin [proj, in mathcomp.boot.monoid]
    SubMonoid.class [proj, in mathcomp.boot.monoid]
    SubMonoid.clone [abbrev, in mathcomp.boot.monoid]
    SubMonoid.copy [abbrev, in mathcomp.boot.monoid]
    SubMonoid.eqtype_hasDecEq_mixin [proj, in mathcomp.boot.monoid]
    SubMonoid.eqtype_isSub_mixin [proj, in mathcomp.boot.monoid]
    SubMonoid.Exports [mod, in mathcomp.boot.monoid]
    SubMonoid.Exports.join_monoid_SubMonoid_between_monoid_BaseUMagma_and_monoid_SubSemigroup [def, in mathcomp.boot.monoid]
    SubMonoid.Exports.join_monoid_SubMonoid_between_monoid_ChoiceBaseUMagma_and_monoid_SubSemigroup [def, in mathcomp.boot.monoid]
    SubMonoid.Exports.join_monoid_SubMonoid_between_monoid_Monoid_and_choice_SubChoice [def, in mathcomp.boot.monoid]
    SubMonoid.Exports.join_monoid_SubMonoid_between_monoid_Monoid_and_eqtype_SubEquality [def, in mathcomp.boot.monoid]
    SubMonoid.Exports.join_monoid_SubMonoid_between_monoid_Monoid_and_eqtype_SubType [def, in mathcomp.boot.monoid]
    SubMonoid.Exports.join_monoid_SubMonoid_between_monoid_Monoid_and_monoid_SubBaseUMagma [def, in mathcomp.boot.monoid]
    SubMonoid.Exports.join_monoid_SubMonoid_between_monoid_Monoid_and_monoid_SubMagma [def, in mathcomp.boot.monoid]
    SubMonoid.Exports.join_monoid_SubMonoid_between_monoid_Monoid_and_monoid_SubSemigroup [def, in mathcomp.boot.monoid]
    SubMonoid.Exports.join_monoid_SubMonoid_between_monoid_Monoid_and_monoid_SubUMagma [def, in mathcomp.boot.monoid]
    SubMonoid.Exports.join_monoid_SubMonoid_between_monoid_Semigroup_and_monoid_SubBaseUMagma [def, in mathcomp.boot.monoid]
    SubMonoid.Exports.join_monoid_SubMonoid_between_monoid_Semigroup_and_monoid_SubUMagma [def, in mathcomp.boot.monoid]
    SubMonoid.Exports.join_monoid_SubMonoid_between_monoid_SubBaseUMagma_and_monoid_SubSemigroup [def, in mathcomp.boot.monoid]
    SubMonoid.Exports.join_monoid_SubMonoid_between_monoid_SubSemigroup_and_monoid_SubUMagma [def, in mathcomp.boot.monoid]
    SubMonoid.Exports.join_monoid_SubMonoid_between_monoid_SubSemigroup_and_monoid_UMagma [def, in mathcomp.boot.monoid]
    SubMonoid.Exports.subMonoidType [abbrev, in mathcomp.boot.monoid]
    SubMonoid.monoid_BaseUMagma_isUMagma_mixin [proj, in mathcomp.boot.monoid]
    SubMonoid.monoid_hasMul_mixin [proj, in mathcomp.boot.monoid]
    SubMonoid.monoid_hasOne_mixin [proj, in mathcomp.boot.monoid]
    SubMonoid.monoid_isSubBaseUMagma_mixin [proj, in mathcomp.boot.monoid]
    SubMonoid.monoid_isSubMagma_mixin [proj, in mathcomp.boot.monoid]
    SubMonoid.monoid_Magma_isSemigroup_mixin [proj, in mathcomp.boot.monoid]
    SubMonoid.on [abbrev, in mathcomp.boot.monoid]
    SubMonoid.on_ [abbrev, in mathcomp.boot.monoid]
    SubMonoid.pack_ [def, in mathcomp.boot.monoid]
    SubMonoid.phant_clone [def, in mathcomp.boot.monoid]
    SubMonoid.phant_on_ [def, in mathcomp.boot.monoid]
    SubMonoid.sort [proj, in mathcomp.boot.monoid]
    SubMonoid.type [rec, in mathcomp.boot.monoid]
    SubMonoidElpiOperations [mod, in mathcomp.boot.monoid]
    submx [abbrev, in mathcomp.algebra.mxalgebra]
    submx [mod, in mathcomp.algebra.mxalgebra]
    submx.body [def, in mathcomp.algebra.mxalgebra]
    submx.unlock [def, in mathcomp.algebra.mxalgebra]
    submx0 [prf, in mathcomp.algebra.mxalgebra]
    submx0null [prf, in mathcomp.algebra.mxalgebra]
    submx1 [prf, in mathcomp.algebra.mxalgebra]
    submx_full [prf, in mathcomp.algebra.mxalgebra]
    submx_Locked [modtype, in mathcomp.algebra.mxalgebra]
    submx_Locked.body [ax, in mathcomp.algebra.mxalgebra]
    submx_Locked.unlock [ax, in mathcomp.algebra.mxalgebra]
    submx_ortho [prf, in mathcomp.algebra.spectral]
    submx_refl [prf, in mathcomp.algebra.mxalgebra]
    submx_rowsub [prf, in mathcomp.algebra.mxalgebra]
    submx_trans [prf, in mathcomp.algebra.mxalgebra]
    submx_unlock_subterm [def, in mathcomp.algebra.mxalgebra]
    submx_unlockable [def, in mathcomp.algebra.mxalgebra]
    submxblock [def, in mathcomp.algebra.matrix]
    submxblock0 [prf, in mathcomp.algebra.matrix]
    submxblock_diag [prf, in mathcomp.algebra.matrix]
    submxblock_sum [prf, in mathcomp.algebra.matrix]
    submxblockB [prf, in mathcomp.algebra.matrix]
    submxblockD [prf, in mathcomp.algebra.matrix]
    submxblockEh [prf, in mathcomp.algebra.matrix]
    submxblockEv [prf, in mathcomp.algebra.matrix]
    submxblockK [prf, in mathcomp.algebra.matrix]
    submxblockN [prf, in mathcomp.algebra.matrix]
    submxcol [def, in mathcomp.algebra.matrix]
    submxcol0 [prf, in mathcomp.algebra.matrix]
    submxcol_matrix [prf, in mathcomp.algebra.matrix]
    submxcol_mul [prf, in mathcomp.algebra.matrix]
    submxcol_sum [prf, in mathcomp.algebra.matrix]
    submxcolB [prf, in mathcomp.algebra.matrix]
    submxcolD [prf, in mathcomp.algebra.matrix]
    submxcolK [prf, in mathcomp.algebra.matrix]
    submxcolN [prf, in mathcomp.algebra.matrix]
    submxE [prf, in mathcomp.algebra.mxalgebra]
    submxElt [prf, in mathcomp.algebra.mxalgebra]
    submxK [prf, in mathcomp.algebra.matrix]
    submxMfree [prf, in mathcomp.algebra.mxalgebra]
    submxMl [prf, in mathcomp.algebra.mxalgebra]
    submxMr [prf, in mathcomp.algebra.mxalgebra]
    submxP [prf, in mathcomp.algebra.mxalgebra]
    submxrow [def, in mathcomp.algebra.matrix]
    submxrow0 [prf, in mathcomp.algebra.matrix]
    submxrow_matrix [prf, in mathcomp.algebra.matrix]
    submxrow_sum [prf, in mathcomp.algebra.matrix]
    submxrowB [prf, in mathcomp.algebra.matrix]
    submxrowD [prf, in mathcomp.algebra.matrix]
    submxrowK [prf, in mathcomp.algebra.matrix]
    submxrowN [prf, in mathcomp.algebra.matrix]
    subn [def, in mathcomp.boot.ssrnat]
    subn0 [prf, in mathcomp.boot.ssrnat]
    subn1 [prf, in mathcomp.boot.ssrnat]
    subn2 [prf, in mathcomp.boot.ssrnat]
    subn_eq0 [prf, in mathcomp.boot.ssrnat]
    subn_exp [prf, in mathcomp.boot.binomial]
    subn_gt0 [prf, in mathcomp.boot.ssrnat]
    subn_if_gt [prf, in mathcomp.boot.ssrnat]
    subn_maxl [prf, in mathcomp.boot.ssrnat]
    subn_minl [prf, in mathcomp.boot.ssrnat]
    subn_rec [def, in mathcomp.boot.ssrnat]
    subn_sqr [prf, in mathcomp.boot.ssrnat]
    subnA [prf, in mathcomp.boot.ssrnat]
    subnAC [prf, in mathcomp.boot.ssrnat]
    subnBA [prf, in mathcomp.boot.ssrnat]
    subnBAC [prf, in mathcomp.boot.ssrnat]
    subnBl_leq [prf, in mathcomp.boot.ssrnat]
    subnBr_leq [prf, in mathcomp.boot.ssrnat]
    subnCBA [prf, in mathcomp.boot.ssrnat]
    subnDA [prf, in mathcomp.boot.ssrnat]
    subnDAC [prf, in mathcomp.boot.ssrnat]
    subnDl [prf, in mathcomp.boot.ssrnat]
    subnDr [prf, in mathcomp.boot.ssrnat]
    subnE [prf, in mathcomp.boot.ssrnat]
    subnK [prf, in mathcomp.boot.ssrnat]
    subnKC [prf, in mathcomp.boot.ssrnat]
    subnn [prf, in mathcomp.boot.ssrnat]
    subnormal [def, in mathcomp.solvable.gseries]
    subnormal_refl [prf, in mathcomp.solvable.gseries]
    subnormal_sub [prf, in mathcomp.solvable.gseries]
    subnormal_trans [prf, in mathcomp.solvable.gseries]
    subnormalEl [prf, in mathcomp.solvable.gseries]
    subnormalEr [prf, in mathcomp.solvable.gseries]
    subnormalEsupport [prf, in mathcomp.solvable.gseries]
    subnormalP [prf, in mathcomp.solvable.gseries]
    subnS [prf, in mathcomp.boot.ssrnat]
    subnSK [prf, in mathcomp.boot.ssrnat]
    SubP [prf, in mathcomp.boot.eqtype]
    SubProbability [abbrev, in mathcomp.analysis.measure_theory.probability_measure]
    SubProbability [mod, in mathcomp.analysis.measure_theory.probability_measure]
    SubProbability.axioms_ [rec, in mathcomp.analysis.measure_theory.probability_measure]
    SubProbability.class [proj, in mathcomp.analysis.measure_theory.probability_measure]
    SubProbability.clone [abbrev, in mathcomp.analysis.measure_theory.probability_measure]
    SubProbability.copy [abbrev, in mathcomp.analysis.measure_theory.probability_measure]
    SubProbability.Exports [mod, in mathcomp.analysis.measure_theory.probability_measure]
    SubProbability.Exports.subprobability [abbrev, in mathcomp.analysis.measure_theory.probability_measure]
    SubProbability.measure_function_Content_isMeasure_mixin [proj, in mathcomp.analysis.measure_theory.probability_measure]
    SubProbability.measure_function_isContent_mixin [proj, in mathcomp.analysis.measure_theory.probability_measure]
    SubProbability.measure_function_isFinite_mixin [proj, in mathcomp.analysis.measure_theory.probability_measure]
    SubProbability.measure_function_isSFinite_mixin [proj, in mathcomp.analysis.measure_theory.probability_measure]
    SubProbability.measure_function_isSigmaFinite_mixin [proj, in mathcomp.analysis.measure_theory.probability_measure]
    SubProbability.on [abbrev, in mathcomp.analysis.measure_theory.probability_measure]
    SubProbability.on_ [abbrev, in mathcomp.analysis.measure_theory.probability_measure]
    SubProbability.pack_ [def, in mathcomp.analysis.measure_theory.probability_measure]
    SubProbability.phant_clone [def, in mathcomp.analysis.measure_theory.probability_measure]
    SubProbability.phant_on_ [def, in mathcomp.analysis.measure_theory.probability_measure]
    SubProbability.probability_measure_isSubProbability_mixin [proj, in mathcomp.analysis.measure_theory.probability_measure]
    SubProbability.sort [proj, in mathcomp.analysis.measure_theory.probability_measure]
    SubProbability.type [rec, in mathcomp.analysis.measure_theory.probability_measure]
    SubProbability_isProbability [mod, in mathcomp.analysis.kernel]
    SubProbability_isProbability [abbrev, in mathcomp.analysis.kernel]
    SubProbability_isProbability.Build [abbrev, in mathcomp.analysis.kernel]
    SubProbabilityElpiOperations [mod, in mathcomp.analysis.measure_theory.probability_measure]
    SubProbabilityKernel [abbrev, in mathcomp.analysis.kernel]
    SubProbabilityKernel [mod, in mathcomp.analysis.kernel]
    SubProbabilityKernel.axioms_ [rec, in mathcomp.analysis.kernel]
    SubProbabilityKernel.class [proj, in mathcomp.analysis.kernel]
    SubProbabilityKernel.clone [abbrev, in mathcomp.analysis.kernel]
    SubProbabilityKernel.copy [abbrev, in mathcomp.analysis.kernel]
    SubProbabilityKernel.Exports [mod, in mathcomp.analysis.kernel]
    SubProbabilityKernel.Exports.sprobability_kernel [abbrev, in mathcomp.analysis.kernel]
    SubProbabilityKernel.kernel_isFiniteTransitionKernel_mixin [proj, in mathcomp.analysis.kernel]
    SubProbabilityKernel.kernel_isKernel_mixin [proj, in mathcomp.analysis.kernel]
    SubProbabilityKernel.kernel_isMeasureFamUub_mixin [proj, in mathcomp.analysis.kernel]
    SubProbabilityKernel.kernel_isSFiniteKernel_subdef_mixin [proj, in mathcomp.analysis.kernel]
    SubProbabilityKernel.kernel_isSubProbabilityKernel_mixin [proj, in mathcomp.analysis.kernel]
    SubProbabilityKernel.on [abbrev, in mathcomp.analysis.kernel]
    SubProbabilityKernel.on_ [abbrev, in mathcomp.analysis.kernel]
    SubProbabilityKernel.pack_ [def, in mathcomp.analysis.kernel]
    SubProbabilityKernel.phant_clone [def, in mathcomp.analysis.kernel]
    SubProbabilityKernel.phant_on_ [def, in mathcomp.analysis.kernel]
    SubProbabilityKernel.sort [proj, in mathcomp.analysis.kernel]
    SubProbabilityKernel.type [rec, in mathcomp.analysis.kernel]
    SubProbabilityKernelElpiOperations [mod, in mathcomp.analysis.kernel]
    subq [def, in mathcomp.algebra.rat]
    subq_ge0 [prf, in mathcomp.algebra.rat]
    subr_cvg0 [prf, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
    subr_surj [prf, in mathcomp.classical.functions]
    subre_ge0 [prf, in mathcomp.reals.constructive_ereal]
    subre_lt0 [prf, in mathcomp.reals.constructive_ereal]
    subRingType [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
    subrKC [prf, in mathcomp.classical.mathcomp_extra]
    subSemiAlgType [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
    SubSemigroup [abbrev, in mathcomp.boot.monoid]
    SubSemigroup [mod, in mathcomp.boot.monoid]
    SubSemigroup.axioms_ [rec, in mathcomp.boot.monoid]
    SubSemigroup.choice_hasChoice_mixin [proj, in mathcomp.boot.monoid]
    SubSemigroup.class [proj, in mathcomp.boot.monoid]
    SubSemigroup.clone [abbrev, in mathcomp.boot.monoid]
    SubSemigroup.copy [abbrev, in mathcomp.boot.monoid]
    SubSemigroup.eqtype_hasDecEq_mixin [proj, in mathcomp.boot.monoid]
    SubSemigroup.eqtype_isSub_mixin [proj, in mathcomp.boot.monoid]
    SubSemigroup.Exports [mod, in mathcomp.boot.monoid]
    SubSemigroup.Exports.join_monoid_SubSemigroup_between_monoid_Semigroup_and_choice_SubChoice [def, in mathcomp.boot.monoid]
    SubSemigroup.Exports.join_monoid_SubSemigroup_between_monoid_Semigroup_and_eqtype_SubEquality [def, in mathcomp.boot.monoid]
    SubSemigroup.Exports.join_monoid_SubSemigroup_between_monoid_Semigroup_and_eqtype_SubType [def, in mathcomp.boot.monoid]
    SubSemigroup.Exports.join_monoid_SubSemigroup_between_monoid_Semigroup_and_monoid_SubMagma [def, in mathcomp.boot.monoid]
    SubSemigroup.Exports.subSemigroupType [abbrev, in mathcomp.boot.monoid]
    SubSemigroup.monoid_hasMul_mixin [proj, in mathcomp.boot.monoid]
    SubSemigroup.monoid_isSubMagma_mixin [proj, in mathcomp.boot.monoid]
    SubSemigroup.monoid_Magma_isSemigroup_mixin [proj, in mathcomp.boot.monoid]
    SubSemigroup.on [abbrev, in mathcomp.boot.monoid]
    SubSemigroup.on_ [abbrev, in mathcomp.boot.monoid]
    SubSemigroup.pack_ [def, in mathcomp.boot.monoid]
    SubSemigroup.phant_clone [def, in mathcomp.boot.monoid]
    SubSemigroup.phant_on_ [def, in mathcomp.boot.monoid]
    SubSemigroup.sort [proj, in mathcomp.boot.monoid]
    SubSemigroup.type [rec, in mathcomp.boot.monoid]
    SubSemigroupElpiOperations [mod, in mathcomp.boot.monoid]
    subSemiRingType [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
    subseq [def, in mathcomp.boot.seq]
    subseq0 [prf, in mathcomp.boot.seq]
    subseq_anti [prf, in mathcomp.boot.seq]
    subseq_cat2l [prf, in mathcomp.boot.seq]
    subseq_cat2r [prf, in mathcomp.boot.seq]
    subseq_cons [prf, in mathcomp.boot.seq]
    subseq_filter [prf, in mathcomp.boot.seq]
    subseq_pairwise [prf, in mathcomp.boot.seq]
    subseq_path [prf, in mathcomp.boot.path]
    subseq_path_in [prf, in mathcomp.boot.path]
    subseq_rcons [prf, in mathcomp.boot.seq]
    subseq_refl [prf, in mathcomp.boot.seq]
    subseq_rem [prf, in mathcomp.boot.seq]
    subseq_rev [prf, in mathcomp.boot.seq]
    subseq_rot [prf, in mathcomp.boot.seq]
    subseq_sort [prf, in mathcomp.boot.path]
    subseq_sort_in [prf, in mathcomp.boot.path]
    subseq_sorted [prf, in mathcomp.boot.path]
    subseq_sorted_in [prf, in mathcomp.boot.path]
    subseq_trans [prf, in mathcomp.boot.seq]
    subseq_uniq [prf, in mathcomp.boot.seq]
    subseq_uniqP [prf, in mathcomp.boot.seq]
    subseqP [prf, in mathcomp.boot.seq]
    subset [def, in mathcomp.classical.classical_sets]
    subset [abbrev, in mathcomp.boot.fintype]
    subset [mod, in mathcomp.boot.fintype]
    subset.body [def, in mathcomp.boot.fintype]
    subset.unlock [def, in mathcomp.boot.fintype]
    subset0 [prf, in mathcomp.classical.classical_sets]
    subset0 [prf, in mathcomp.boot.finset]
    subset1 [prf, in mathcomp.boot.finset]
    subset_all [prf, in mathcomp.boot.fintype]
    subset_ball_prop_in_itv [prf, in mathcomp.analysis.topology_theory.pseudometric_structure]
    subset_ball_prop_in_itvcc [prf, in mathcomp.analysis.topology_theory.pseudometric_structure]
    subset_bigcap [prf, in mathcomp.classical.classical_sets]
    subset_bigcap_r [prf, in mathcomp.classical.classical_sets]
    subset_bigcup [prf, in mathcomp.classical.classical_sets]
    subset_bigcup_r [prf, in mathcomp.classical.classical_sets]
    subset_bigsetI [prf, in mathcomp.classical.classical_sets]
    subset_bigsetI_cond [prf, in mathcomp.classical.classical_sets]
    subset_bigsetU [prf, in mathcomp.classical.classical_sets]
    subset_bigsetU_cond [prf, in mathcomp.classical.classical_sets]
    subset_card_le [prf, in mathcomp.classical.cardinality]
    subset_cardP [prf, in mathcomp.boot.fintype]
    subset_cat2 [prf, in mathcomp.boot.fintype]
    subset_catl [prf, in mathcomp.boot.fintype]
    subset_catr [prf, in mathcomp.boot.fintype]
    subset_closed_ball [prf, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
    subset_closure [prf, in mathcomp.boot.fingraph]
    subset_closure [prf, in mathcomp.analysis.topology_theory.topology_structure]
    subset_closure_half [prf, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
    subset_cons [prf, in mathcomp.boot.seq]
    subset_cons [prf, in mathcomp.boot.fintype]
    subset_cons2 [prf, in mathcomp.boot.seq]
    subset_cons2 [prf, in mathcomp.boot.fintype]
    subset_cover [prf, in mathcomp.boot.finset]
    subset_dfs [prf, in mathcomp.boot.fingraph]
    subset_disjoint [prf, in mathcomp.boot.fintype]
    subset_eqP [prf, in mathcomp.boot.fintype]
    subset_faithful [prf, in mathcomp.finite_group.action]
    subset_filter [def, in mathcomp.classical.filter]
    subset_filter [prf, in mathcomp.boot.fintype]
    subset_filter_filter [inst, in mathcomp.classical.filter]
    subset_filter_proper [prf, in mathcomp.classical.filter]
    subset_fst_set [prf, in mathcomp.classical.classical_sets]
    subset_fsub [prf, in mathcomp.finmap.finmap]
    subset_fsubE [prf, in mathcomp.finmap.finmap]
    subset_gen [prf, in mathcomp.finite_group.fingroup]
    subset_has_lbound [prf, in mathcomp.classical.classical_sets]
    subset_has_ubound [prf, in mathcomp.classical.classical_sets]
    subset_imfset [prf, in mathcomp.finmap.finmap]
    subset_iter [prf, in mathcomp.boot.finset]
    subset_iterS [prf, in mathcomp.boot.finset]
    subset_itv [prf, in mathcomp.classical.set_interval]
    subset_itv [prf, in mathcomp.algebra.interval]
    subset_itv_bound [prf, in mathcomp.algebra.interval]
    subset_itv_co_cc [prf, in mathcomp.algebra.interval]
    subset_itv_oc_cc [prf, in mathcomp.algebra.interval]
    subset_itv_oo_cc [prf, in mathcomp.algebra.interval]
    subset_itv_oo_co [prf, in mathcomp.algebra.interval]
    subset_itv_oo_oc [prf, in mathcomp.algebra.interval]
    subset_itvl [prf, in mathcomp.classical.set_interval]
    subset_itvP [prf, in mathcomp.classical.set_interval]
    subset_itvr [prf, in mathcomp.classical.set_interval]
    subset_itvScc [prf, in mathcomp.classical.set_interval]
    subset_itvSoo [prf, in mathcomp.classical.set_interval]
    subset_itvW [prf, in mathcomp.classical.set_interval]
    subset_le_big [prf, in mathcomp.boot.bigop]
    subset_le_big_cond [prf, in mathcomp.boot.finset]
    subset_lee_nneseries [prf, in mathcomp.analysis.sequences]
    subset_leq_card [prf, in mathcomp.boot.fintype]
    subset_leqif_card [prf, in mathcomp.boot.fintype]
    subset_leqif_cards [prf, in mathcomp.boot.finset]
    subset_limgP [prf, in mathcomp.algebra.vector]
    subset_limit_point [prf, in mathcomp.analysis.topology_theory.topology_structure]
    subset_Locked [modtype, in mathcomp.boot.fintype]
    subset_Locked.body [ax, in mathcomp.boot.fintype]
    subset_Locked.unlock [ax, in mathcomp.boot.fintype]
    subset_mapP [prf, in mathcomp.boot.seq]
    subset_measure0 [prf, in mathcomp.analysis.measure_theory.measure_function]
    subset_memP [prf, in mathcomp.boot.seq]
    subset_msetBLR [prf, in mathcomp.finmap.multiset]
    subset_neq0 [prf, in mathcomp.boot.finset]
    subset_nonempty [prf, in mathcomp.classical.classical_sets]
    subset_null_set [prf, in mathcomp.analysis.measure_theory.measure_negligible]
    subset_pred1 [prf, in mathcomp.boot.fintype]
    subset_predT [prf, in mathcomp.boot.fintype]
    subset_refl [prf, in mathcomp.classical.classical_sets]
    subset_seqDU [prf, in mathcomp.analysis.sequences]
    subset_set1 [prf, in mathcomp.classical.classical_sets]
    subset_set2 [prf, in mathcomp.classical.classical_sets]
    subset_sigma_subadditive [def, in mathcomp.analysis.measure_theory.measurable_structure]
    subset_snd_set [prf, in mathcomp.classical.classical_sets]
    subset_split_ent [prf, in mathcomp.analysis.topology_theory.uniform_structure]
    subset_strace [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    subset_trans [prf, in mathcomp.classical.classical_sets]
    subset_trans [prf, in mathcomp.boot.fintype]
    subset_unlock [def, in mathcomp.boot.fintype]
    subset_unlock_subterm [def, in mathcomp.boot.fintype]
    subsetC [prf, in mathcomp.classical.classical_sets]
    subsetC [prf, in mathcomp.boot.finset]
    subsetC1 [prf, in mathcomp.classical.classical_sets]
    subsetC2 [prf, in mathcomp.classical.classical_sets]
    subsetC_disjoint [prf, in mathcomp.boot.finset]
    subsetC_trivIset [prf, in mathcomp.classical.classical_sets]
    subsetCl [prf, in mathcomp.classical.classical_sets]
    subsetCP [prf, in mathcomp.classical.classical_sets]
    subsetCPl [prf, in mathcomp.classical.classical_sets]
    subsetCPr [prf, in mathcomp.classical.classical_sets]
    subsetCr [prf, in mathcomp.classical.classical_sets]
    subsetCW [def, in mathcomp.classical.classical_sets]
    subsetD [prf, in mathcomp.boot.finset]
    subsetD1 [prf, in mathcomp.boot.finset]
    subsetD1P [prf, in mathcomp.boot.finset]
    subsetDl [prf, in mathcomp.boot.finset]
    subsetDP [prf, in mathcomp.boot.finset]
    subsetDr [prf, in mathcomp.boot.finset]
    subsetE [prf, in mathcomp.boot.fintype]
    subsetI [prf, in mathcomp.classical.classical_sets]
    subsetI [prf, in mathcomp.boot.finset]
    subsetI_eq0 [prf, in mathcomp.classical.classical_sets]
    subsetI_neq0 [prf, in mathcomp.classical.classical_sets]
    subsetIidl [prf, in mathcomp.boot.finset]
    subsetIidr [prf, in mathcomp.boot.finset]
    subsetIl [prf, in mathcomp.boot.finset]
    subsetIP [prf, in mathcomp.boot.finset]
    subsetIr [prf, in mathcomp.boot.finset]
    subsetP [prf, in mathcomp.classical.classical_sets]
    subsetP [prf, in mathcomp.boot.fintype]
    subsetPn [prf, in mathcomp.boot.fintype]
    subsets_disjoint [prf, in mathcomp.classical.classical_sets]
    subsets_disjoint [prf, in mathcomp.boot.finset]
    subsetT [prf, in mathcomp.classical.classical_sets]
    subsetT [prf, in mathcomp.boot.finset]
    subsetT_hint [prf, in mathcomp.boot.finset]
    subsetU [prf, in mathcomp.boot.finset]
    subsetU1 [prf, in mathcomp.boot.finset]
    subsetUl [prf, in mathcomp.classical.classical_sets]
    subsetUl [prf, in mathcomp.boot.finset]
    subsetUr [prf, in mathcomp.classical.classical_sets]
    subsetUr [prf, in mathcomp.boot.finset]
    subsetv [def, in mathcomp.algebra.vector]
    subsetW [prf, in mathcomp.classical.classical_sets]
    subSKn [prf, in mathcomp.boot.ssrnat]
    subSn [prf, in mathcomp.boot.ssrnat]
    subSnn [prf, in mathcomp.boot.ssrnat]
    subspace [def, in mathcomp.analysis.topology_theory.subspace_topology]
    subspace_ball [def, in mathcomp.analysis.topology_theory.subspace_topology]
    subspace_continuous_measurable_fun [prf, in mathcomp.analysis.measurable_realfun]
    subspace_continuousP [prf, in mathcomp.analysis.topology_theory.subspace_topology]
    subspace_cvgP [prf, in mathcomp.analysis.topology_theory.subspace_topology]
    subspace_ent [def, in mathcomp.analysis.topology_theory.subspace_topology]
    subspace_eq_continuous [prf, in mathcomp.analysis.topology_theory.subspace_topology]
    subspace_filter [inst, in mathcomp.analysis.topology_theory.subspace_topology]
    subspace_hausdorff [prf, in mathcomp.analysis.topology_theory.separation_axioms]
    subspace_proper_filter [inst, in mathcomp.analysis.topology_theory.subspace_topology]
    subspace_sigL_continuousP [prf, in mathcomp.analysis.topology_theory.subtype_topology]
    subspace_subtypeP [prf, in mathcomp.analysis.topology_theory.subtype_topology]
    subspace_topology [file, in mathcomp.analysis.topology_theory.subspace_topology]
    subspace_valL_continuousP [prf, in mathcomp.analysis.topology_theory.subtype_topology]
    subspace_valL_continuousP' [prf, in mathcomp.analysis.topology_theory.subtype_topology]
    subspaceT_continuous [prf, in mathcomp.analysis.topology_theory.subspace_topology]
    subSpec [constr, in mathcomp.boot.eqtype]
    subSS [prf, in mathcomp.boot.ssrnat]
    subTset [prf, in mathcomp.classical.classical_sets]
    subTset [prf, in mathcomp.boot.finset]
    SubType [abbrev, in mathcomp.boot.eqtype]
    SubType [mod, in mathcomp.boot.eqtype]
    SubType.axioms_ [rec, in mathcomp.boot.eqtype]
    SubType.class [proj, in mathcomp.boot.eqtype]
    SubType.clone [abbrev, in mathcomp.boot.eqtype]
    SubType.copy [abbrev, in mathcomp.boot.eqtype]
    SubType.eqtype_isSub_mixin [proj, in mathcomp.boot.eqtype]
    SubType.Exports [mod, in mathcomp.boot.eqtype]
    SubType.Exports.subType [abbrev, in mathcomp.boot.eqtype]
    SubType.on [abbrev, in mathcomp.boot.eqtype]
    SubType.on_ [abbrev, in mathcomp.boot.eqtype]
    SubType.pack_ [def, in mathcomp.boot.eqtype]
    SubType.phant_clone [def, in mathcomp.boot.eqtype]
    SubType.phant_on_ [def, in mathcomp.boot.eqtype]
    SubType.sort [proj, in mathcomp.boot.eqtype]
    SubType.type [rec, in mathcomp.boot.eqtype]
    subtype_topology [file, in mathcomp.analysis.topology_theory.subtype_topology]
    SubTypeElpiOperations [mod, in mathcomp.boot.eqtype]
    SubUMagma [abbrev, in mathcomp.boot.monoid]
    SubUMagma [mod, in mathcomp.boot.monoid]
    SubUMagma.axioms_ [rec, in mathcomp.boot.monoid]
    SubUMagma.choice_hasChoice_mixin [proj, in mathcomp.boot.monoid]
    SubUMagma.class [proj, in mathcomp.boot.monoid]
    SubUMagma.clone [abbrev, in mathcomp.boot.monoid]
    SubUMagma.copy [abbrev, in mathcomp.boot.monoid]
    SubUMagma.eqtype_hasDecEq_mixin [proj, in mathcomp.boot.monoid]
    SubUMagma.eqtype_isSub_mixin [proj, in mathcomp.boot.monoid]
    SubUMagma.Exports [mod, in mathcomp.boot.monoid]
    SubUMagma.Exports.join_monoid_SubUMagma_between_choice_SubChoice_and_monoid_UMagma [def, in mathcomp.boot.monoid]
    SubUMagma.Exports.join_monoid_SubUMagma_between_eqtype_SubEquality_and_monoid_UMagma [def, in mathcomp.boot.monoid]
    SubUMagma.Exports.join_monoid_SubUMagma_between_eqtype_SubType_and_monoid_UMagma [def, in mathcomp.boot.monoid]
    SubUMagma.Exports.join_monoid_SubUMagma_between_monoid_SubBaseUMagma_and_monoid_UMagma [def, in mathcomp.boot.monoid]
    SubUMagma.Exports.join_monoid_SubUMagma_between_monoid_SubMagma_and_monoid_UMagma [def, in mathcomp.boot.monoid]
    SubUMagma.Exports.subUMagmaType [abbrev, in mathcomp.boot.monoid]
    SubUMagma.monoid_BaseUMagma_isUMagma_mixin [proj, in mathcomp.boot.monoid]
    SubUMagma.monoid_hasMul_mixin [proj, in mathcomp.boot.monoid]
    SubUMagma.monoid_hasOne_mixin [proj, in mathcomp.boot.monoid]
    SubUMagma.monoid_isSubBaseUMagma_mixin [proj, in mathcomp.boot.monoid]
    SubUMagma.monoid_isSubMagma_mixin [proj, in mathcomp.boot.monoid]
    SubUMagma.on [abbrev, in mathcomp.boot.monoid]
    SubUMagma.on_ [abbrev, in mathcomp.boot.monoid]
    SubUMagma.pack_ [def, in mathcomp.boot.monoid]
    SubUMagma.phant_clone [def, in mathcomp.boot.monoid]
    SubUMagma.phant_on_ [def, in mathcomp.boot.monoid]
    SubUMagma.sort [proj, in mathcomp.boot.monoid]
    SubUMagma.type [rec, in mathcomp.boot.monoid]
    SubUMagmaElpiOperations [mod, in mathcomp.boot.monoid]
    subUset [prf, in mathcomp.classical.classical_sets]
    subUset [prf, in mathcomp.boot.finset]
    subUsetP [prf, in mathcomp.boot.finset]
    subV [abbrev, in mathcomp.algebra.vector]
    subv0 [prf, in mathcomp.algebra.vector]
    subv_add [prf, in mathcomp.algebra.vector]
    subv_adjoin [prf, in mathcomp.field.falgebra]
    subv_adjoin_seq [prf, in mathcomp.field.falgebra]
    subv_anti [prf, in mathcomp.algebra.vector]
    subv_bigcapP [prf, in mathcomp.algebra.vector]
    subv_cap [prf, in mathcomp.algebra.vector]
    subv_cent1 [prf, in mathcomp.field.falgebra]
    subv_sumP [prf, in mathcomp.algebra.vector]
    subv_trans [prf, in mathcomp.algebra.vector]
    SubVectType [def, in mathcomp.field.fieldext]
    subvf [prf, in mathcomp.algebra.vector]
    subvP [prf, in mathcomp.algebra.vector]
    subvP_adjoin [prf, in mathcomp.field.falgebra]
    subvPn [prf, in mathcomp.algebra.vector]
    Subvs [constr, in mathcomp.algebra.vector]
    subvs_fieldMixin [prf, in mathcomp.field.fieldext]
    subvs_inj [prf, in mathcomp.algebra.vector]
    subvs_mu1l [prf, in mathcomp.field.falgebra]
    subvs_mul [def, in mathcomp.field.falgebra]
    subvs_mul1 [prf, in mathcomp.field.falgebra]
    subvs_mulA [prf, in mathcomp.field.falgebra]
    subvs_mulDl [prf, in mathcomp.field.falgebra]
    subvs_mulDr [prf, in mathcomp.field.falgebra]
    subvs_of [ind, in mathcomp.algebra.vector]
    subvs_of_ind [scheme, in mathcomp.algebra.vector]
    subvs_of_rec [scheme, in mathcomp.algebra.vector]
    subvs_of_rect [scheme, in mathcomp.algebra.vector]
    subvs_of_sind [scheme, in mathcomp.algebra.vector]
    subvs_one [def, in mathcomp.field.falgebra]
    subvs_scaleAl [prf, in mathcomp.field.falgebra]
    subvs_scaleAr [prf, in mathcomp.field.falgebra]
    subvs_vect_iso [prf, in mathcomp.algebra.vector]
    SubvsE [prf, in mathcomp.algebra.vector]
    subvsP [prf, in mathcomp.algebra.vector]
    subvv [prf, in mathcomp.algebra.vector]
    subX_agenv [prf, in mathcomp.field.falgebra]
    subxx [prf, in mathcomp.boot.fintype]
    subxx_hint [prf, in mathcomp.boot.fintype]
    subzn [prf, in mathcomp.algebra.ssrint]
    subzSS [prf, in mathcomp.algebra.ssrint]
    succn [abbrev, in mathcomp.boot.ssrnat]
    succn_inj [prf, in mathcomp.boot.ssrnat]
    succn_snum [def, in mathcomp.reals.signed]
    succnK [prf, in mathcomp.boot.ssrnat]
    suffix [def, in mathcomp.boot.seq]
    suffix0s [prf, in mathcomp.boot.seq]
    suffix1s [prf, in mathcomp.boot.seq]
    suffix_catl [prf, in mathcomp.boot.seq]
    suffix_catr [prf, in mathcomp.boot.seq]
    suffix_cons [prf, in mathcomp.boot.seq]
    suffix_drop [prf, in mathcomp.boot.seq]
    suffix_infix [prf, in mathcomp.boot.seq]
    suffix_infix_trans [prf, in mathcomp.boot.seq]
    suffix_prefix_trans [prf, in mathcomp.boot.seq]
    suffix_rcons [prf, in mathcomp.boot.seq]
    suffix_refl [prf, in mathcomp.boot.seq]
    suffix_rev [prf, in mathcomp.boot.seq]
    suffix_revLR [prf, in mathcomp.boot.seq]
    suffix_sorted [prf, in mathcomp.boot.path]
    suffix_subseq [prf, in mathcomp.boot.seq]
    suffix_suffix [prf, in mathcomp.boot.seq]
    suffix_trans [prf, in mathcomp.boot.seq]
    suffix_uniq [prf, in mathcomp.boot.seq]
    suffixE [prf, in mathcomp.boot.seq]
    suffixP [prf, in mathcomp.boot.seq]
    suffixs0 [prf, in mathcomp.boot.seq]
    suffixW [prf, in mathcomp.boot.seq]
    sum [def, in mathcomp.analysis.showcase.summability]
    sum1_card [prf, in mathcomp.boot.bigop]
    sum1_count [prf, in mathcomp.boot.bigop]
    sum1_size [prf, in mathcomp.boot.bigop]
    sum1dep_card [prf, in mathcomp.boot.finset]
    sum_card_class [prf, in mathcomp.finite_group.action]
    sum_drop_poly [prf, in mathcomp.algebra.poly]
    sum_enum [def, in mathcomp.boot.fintype]
    sum_enum_prob [prf, in mathcomp.analysis.probability_theory.random_variable]
    sum_enum_uniq [prf, in mathcomp.boot.fintype]
    sum_eq [def, in mathcomp.boot.eqtype]
    sum_eqE [prf, in mathcomp.boot.eqtype]
    sum_eqP [prf, in mathcomp.boot.eqtype]
    sum_even_poly [prf, in mathcomp.algebra.poly]
    sum_ffun [prf, in mathcomp.boot.nmodule]
    sum_ffun [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
    sum_ffunE [prf, in mathcomp.boot.nmodule]
    sum_ffunE [prf, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
    sum_fin_num [prf, in mathcomp.reals.constructive_ereal]
    sum_fin_numP [prf, in mathcomp.reals.constructive_ereal]
    sum_fine [prf, in mathcomp.reals.constructive_ereal]
    sum_index_rcosets_cycle [prf, in mathcomp.solvable.finmodule]
    sum_isFinite [def, in mathcomp.boot.fintype]
    sum_lfunE [prf, in mathcomp.algebra.vector]
    sum_mset [prf, in mathcomp.finmap.multiset]
    sum_mxsum [def, in mathcomp.algebra.mxalgebra]
    sum_nat_cond_const [prf, in mathcomp.boot.finset]
    sum_nat_const [prf, in mathcomp.boot.bigop]
    sum_nat_const_nat [prf, in mathcomp.boot.bigop]
    sum_nat_eq0 [prf, in mathcomp.boot.bigop]
    sum_nat_eq1 [prf, in mathcomp.boot.bigop]
    sum_nat_seq_eq0 [prf, in mathcomp.finmap.multiset]
    sum_nat_seq_eq0 [prf, in mathcomp.boot.bigop]
    sum_nat_seq_eq1 [prf, in mathcomp.boot.bigop]
    sum_nat_seq_neq0 [prf, in mathcomp.boot.bigop]
    sum_ncycle_totient [prf, in mathcomp.solvable.cyclic]
    sum_nnsfun [def, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
    sum_nnsfunE [prf, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
    sum_odd_poly [prf, in mathcomp.algebra.poly]
    sum_of_opair [def, in mathcomp.boot.choice]
    sum_totient_dvd [prf, in mathcomp.solvable.cyclic]
    sume_ge0 [prf, in mathcomp.reals.constructive_ereal]
    sume_le0 [prf, in mathcomp.reals.constructive_ereal]
    sumEFin [prf, in mathcomp.reals.constructive_ereal]
    sumeN [prf, in mathcomp.reals.constructive_ereal]
    sumfv [prf, in mathcomp.algebra.vector]
    sumKx [abbrev, in mathcomp.field.fieldext]
    summability [file, in mathcomp.analysis.showcase.summability]
    summable [def, in mathcomp.analysis.showcase.summability]
    summable [def, in mathcomp.analysis.esum]
    summable_cvg [prf, in mathcomp.analysis.esum]
    summable_eseries [prf, in mathcomp.analysis.esum]
    summable_eseries_esum [prf, in mathcomp.analysis.esum]
    summable_fine_sum [prf, in mathcomp.analysis.esum]
    summable_funeneg [prf, in mathcomp.analysis.esum]
    summable_funepos [prf, in mathcomp.analysis.esum]
    summable_integral_dirac [prf, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_nonneg]
    summable_nneseries_lim [prf, in mathcomp.analysis.esum]
    summable_pinfty [prf, in mathcomp.analysis.esum]
    summableB [prf, in mathcomp.analysis.esum]
    summableD [prf, in mathcomp.analysis.esum]
    summableE [prf, in mathcomp.analysis.esum]
    summableN [prf, in mathcomp.analysis.esum]
    summx_sub [prf, in mathcomp.algebra.mxalgebra]
    summx_sub_sums [prf, in mathcomp.algebra.mxalgebra]
    summxE [prf, in mathcomp.algebra.matrix]
    sumMz [prf, in mathcomp.algebra.ssrint]
    sumn [def, in mathcomp.boot.seq]
    sumn_cat [prf, in mathcomp.boot.seq]
    sumn_count [prf, in mathcomp.boot.seq]
    sumn_filter [prf, in mathcomp.finmap.multiset]
    sumn_flatten [prf, in mathcomp.boot.seq]
    sumn_map [prf, in mathcomp.finmap.multiset]
    sumn_map_filter [prf, in mathcomp.finmap.multiset]
    sumn_ncons [prf, in mathcomp.boot.seq]
    sumn_nseq [prf, in mathcomp.boot.seq]
    sumn_rcons [prf, in mathcomp.boot.seq]
    sumn_rev [prf, in mathcomp.boot.seq]
    sumn_rot [prf, in mathcomp.boot.seq]
    sumn_set_nth [prf, in mathcomp.boot.seq]
    sumn_set_nth0 [prf, in mathcomp.boot.seq]
    sumn_set_nth_ltn [prf, in mathcomp.boot.seq]
    sumnB [prf, in mathcomp.boot.bigop]
    sumnE [prf, in mathcomp.boot.bigop]
    sumr_le0 [prf, in mathcomp.classical.mathcomp_extra]
    sumrfctE [prf, in mathcomp.classical.functions]
    sumsmx_subP [prf, in mathcomp.algebra.mxalgebra]
    sumsmx_sup [prf, in mathcomp.algebra.mxalgebra]
    sumsmxMr [prf, in mathcomp.algebra.mxalgebra]
    sumsmxMr_gen [prf, in mathcomp.algebra.mxalgebra]
    sumsmxS [prf, in mathcomp.algebra.mxalgebra]
    sumV [abbrev, in mathcomp.algebra.vector]
    sumv_pi [abbrev, in mathcomp.algebra.vector]
    sumv_pi_for [def, in mathcomp.algebra.vector]
    sumv_pi_nat_sum [prf, in mathcomp.algebra.vector]
    sumv_pi_sum [prf, in mathcomp.algebra.vector]
    sumv_pi_uniq_sum [prf, in mathcomp.algebra.vector]
    sumv_sup [prf, in mathcomp.algebra.vector]
    sup [def, in mathcomp.reals.reals]
    sup0 [prf, in mathcomp.reals.reals]
    sup1 [prf, in mathcomp.reals.reals]
    sup_adherent [prf, in mathcomp.reals.reals]
    sup_adherent_subdef [def, in mathcomp.reals.reals]
    sup_contract_le1 [prf, in mathcomp.analysis.ereal]
    sup_down [prf, in mathcomp.reals.reals]
    sup_ent [def, in mathcomp.analysis.topology_theory.supremum_topology]
    sup_ent_filter [prf, in mathcomp.analysis.topology_theory.supremum_topology]
    sup_ent_inv [prf, in mathcomp.analysis.topology_theory.supremum_topology]
    sup_ent_nbhs [prf, in mathcomp.analysis.topology_theory.supremum_topology]
    sup_ent_refl [prf, in mathcomp.analysis.topology_theory.supremum_topology]
    sup_ent_split [prf, in mathcomp.analysis.topology_theory.supremum_topology]
    sup_field_module [prf, in mathcomp.field.fieldext]
    sup_gt [prf, in mathcomp.reals.reals]
    sup_in_floor_set [prf, in mathcomp.reals.reals]
    sup_itv [prf, in mathcomp.reals.real_interval]
    sup_itvcc [prf, in mathcomp.reals.real_interval]
    sup_le [prf, in mathcomp.reals.reals]
    sup_le_ub [abbrev, in mathcomp.reals.reals]
    sup_open [abbrev, in mathcomp.analysis.topology_theory.function_spaces]
    sup_out [prf, in mathcomp.reals.reals]
    sup_pseudometric [def, in mathcomp.analysis.topology_theory.separation_axioms]
    sup_setU [prf, in mathcomp.reals.reals]
    sup_subbase [def, in mathcomp.analysis.topology_theory.supremum_topology]
    sup_sumE [prf, in mathcomp.reals.reals]
    sup_topology [def, in mathcomp.analysis.topology_theory.supremum_topology]
    sup_total [prf, in mathcomp.reals.reals]
    sup_ub_strict [prf, in mathcomp.reals.reals]
    sup_ubound [abbrev, in mathcomp.reals.reals]
    sup_upper_bound [prf, in mathcomp.reals.reals]
    sup_upper_bound_subdef [def, in mathcomp.reals.reals]
    super_bij [prf, in mathcomp.classical.cardinality]
    support [abbrev, in mathcomp.boot.nmodule]
    support [abbrev, in mathcomp.algebra.algebraic_hierarchy.rings_modules_and_algebras]
    support_for [def, in mathcomp.boot.finfun]
    supportE [prf, in mathcomp.boot.finfun]
    supportP [prf, in mathcomp.boot.finfun]
    supremum [def, in mathcomp.classical.classical_sets]
    supremum0 [prf, in mathcomp.classical.classical_sets]
    supremum1 [prf, in mathcomp.classical.classical_sets]
    supremum_out [prf, in mathcomp.classical.classical_sets]
    supremum_pinfty [prf, in mathcomp.analysis.ereal]
    supremum_topology [file, in mathcomp.analysis.topology_theory.supremum_topology]
    supremums [def, in mathcomp.classical.classical_sets]
    supremums1 [prf, in mathcomp.classical.classical_sets]
    supremumsT [prf, in mathcomp.analysis.ereal]
    supremumT [prf, in mathcomp.analysis.ereal]
    sups [def, in mathcomp.analysis.sequences]
    sups_preimage [prf, in mathcomp.analysis.sequences]
    supsN [prf, in mathcomp.analysis.sequences]
    surj [prf, in mathcomp.classical.functions]
    surj_card_ge [prf, in mathcomp.classical.cardinality]
    surj_comp [prf, in mathcomp.classical.functions]
    surj_epi [prf, in mathcomp.classical.functions]
    surj_id [prf, in mathcomp.classical.functions]
    surj_image_eq [prf, in mathcomp.classical.functions]
    surj_set0 [prf, in mathcomp.classical.functions]
    surjE [prf, in mathcomp.classical.functions]
    Surject [abbrev, in mathcomp.classical.functions]
    Surject [mod, in mathcomp.classical.functions]
    Surject.axioms_ [rec, in mathcomp.classical.functions]
    Surject.class [proj, in mathcomp.classical.functions]
    Surject.clone [abbrev, in mathcomp.classical.functions]
    Surject.copy [abbrev, in mathcomp.classical.functions]
    Surject.Exports [mod, in mathcomp.classical.functions]
    Surject.functions_OInv_CanV_mixin [proj, in mathcomp.classical.functions]
    Surject.functions_OInv_mixin [proj, in mathcomp.classical.functions]
    Surject.on [abbrev, in mathcomp.classical.functions]
    Surject.on_ [abbrev, in mathcomp.classical.functions]
    Surject.pack_ [def, in mathcomp.classical.functions]
    Surject.phant_clone [def, in mathcomp.classical.functions]
    Surject.phant_on_ [def, in mathcomp.classical.functions]
    Surject.sort [proj, in mathcomp.classical.functions]
    Surject.type [rec, in mathcomp.classical.functions]
    SurjectElpiOperations [mod, in mathcomp.classical.functions]
    surjection_of_surj [def, in mathcomp.classical.functions]
    surjective_existT [prf, in mathcomp.classical.boolp]
    surjective_ocanV [def, in mathcomp.classical.functions]
    surjective_oinvK [prf, in mathcomp.classical.functions]
    surjective_oinvS [prf, in mathcomp.classical.functions]
    SurjFun [abbrev, in mathcomp.classical.functions]
    SurjFun [mod, in mathcomp.classical.functions]
    SurjFun.axioms_ [rec, in mathcomp.classical.functions]
    SurjFun.class [proj, in mathcomp.classical.functions]
    SurjFun.clone [abbrev, in mathcomp.classical.functions]
    SurjFun.copy [abbrev, in mathcomp.classical.functions]
    SurjFun.Exports [mod, in mathcomp.classical.functions]
    SurjFun.Exports.join_functions_SurjFun_between_functions_Fun_and_functions_Surject [def, in mathcomp.classical.functions]
    SurjFun.Exports.join_functions_SurjFun_between_functions_OInvFun_and_functions_Surject [def, in mathcomp.classical.functions]
    SurjFun.functions_isFun_mixin [proj, in mathcomp.classical.functions]
    SurjFun.functions_OInv_CanV_mixin [proj, in mathcomp.classical.functions]
    SurjFun.functions_OInv_mixin [proj, in mathcomp.classical.functions]
    SurjFun.on [abbrev, in mathcomp.classical.functions]
    SurjFun.on_ [abbrev, in mathcomp.classical.functions]
    SurjFun.pack_ [def, in mathcomp.classical.functions]
    SurjFun.phant_clone [def, in mathcomp.classical.functions]
    SurjFun.phant_on_ [def, in mathcomp.classical.functions]
    SurjFun.sort [proj, in mathcomp.classical.functions]
    SurjFun.type [rec, in mathcomp.classical.functions]
    SurjFun_Inj [abbrev, in mathcomp.classical.functions]
    SurjFun_Inj [mod, in mathcomp.classical.functions]
    SurjFun_Inj.axioms [abbrev, in mathcomp.classical.functions]
    SurjFun_Inj.axioms_ [rec, in mathcomp.classical.functions]
    SurjFun_Inj.Build [abbrev, in mathcomp.classical.functions]
    SurjFun_Inj.Exports [mod, in mathcomp.classical.functions]
    SurjFun_Inj.inj [proj, in mathcomp.classical.functions]
    SurjFun_Inj.phant_axioms [def, in mathcomp.classical.functions]
    SurjFun_Inj.phant_Build [def, in mathcomp.classical.functions]
    SurjFunElpiOperations [mod, in mathcomp.classical.functions]
    surjfunPex [prf, in mathcomp.classical.cardinality]
    surjPex [prf, in mathcomp.classical.cardinality]
    surjPfun [prf, in mathcomp.classical.functions]
    surjpinv_bij [prf, in mathcomp.classical.functions]
    surjpinv_image_sub [prf, in mathcomp.classical.functions]
    surjpinv_inj [prf, in mathcomp.classical.functions]
    surjpK [prf, in mathcomp.classical.functions]
    sv [def, in mathcomp.solvable.burnside_app]
    Sv [def, in mathcomp.solvable.burnside_app]
    Sv_inj [prf, in mathcomp.solvable.burnside_app]
    sv_inv [prf, in mathcomp.solvable.burnside_app]
    swap [def, in mathcomp.classical.unstable]
    swap_continuous [prf, in mathcomp.analysis.topology_theory.product_topology]
    swap_pair [def, in mathcomp.boot.ssrfun]
    swap_pairK [prf, in mathcomp.boot.ssrfun]
    swapK [prf, in mathcomp.classical.unstable]
    swapXY [def, in mathcomp.algebra.polyXY]
    swapXY_comp_poly [prf, in mathcomp.algebra.polyXY]
    swapXY_def [def, in mathcomp.algebra.polyXY]
    swapXY_eq0 [prf, in mathcomp.algebra.polyXY]
    swapXY_is_additive [def, in mathcomp.algebra.polyXY]
    swapXY_is_monoid_morphism [prf, in mathcomp.algebra.polyXY]
    swapXY_is_multiplicative [def, in mathcomp.algebra.polyXY]
    swapXY_is_scalable [prf, in mathcomp.algebra.polyXY]
    swapXY_is_zmod_morphism [prf, in mathcomp.algebra.polyXY]
    swapXY_key [prf, in mathcomp.algebra.polyXY]
    swapXY_map [prf, in mathcomp.algebra.polyXY]
    swapXY_map_polyC [prf, in mathcomp.algebra.polyXY]
    swapXY_poly_XaY [prf, in mathcomp.algebra.polyXY]
    swapXY_poly_XmY [prf, in mathcomp.algebra.polyXY]
    swapXY_polyC [prf, in mathcomp.algebra.polyXY]
    swapXY_unlockable [def, in mathcomp.algebra.polyXY]
    swapXY_X [prf, in mathcomp.algebra.polyXY]
    swapXY_Y [prf, in mathcomp.algebra.polyXY]
    swapXYK [prf, in mathcomp.algebra.polyXY]
    swizzle_mx [def, in mathcomp.algebra.matrix]
    swizzle_mx_is_additive [def, in mathcomp.algebra.matrix]
    swizzle_mx_is_nmod_morphism [prf, in mathcomp.algebra.matrix]
    swizzle_mx_is_scalable [prf, in mathcomp.algebra.matrix]
    swizzle_mx_is_semi_additive [def, in mathcomp.algebra.matrix]
    swizzle_mx_is_zmod_morphism [prf, in mathcomp.algebra.matrix]
    SwizzleAdd [abbrev, in mathcomp.algebra.matrix]
    SwizzleLin [abbrev, in mathcomp.algebra.matrix]
    Syl [def, in mathcomp.solvable.pgroup]
    Syl_trans [prf, in mathcomp.solvable.sylow]
    sylow [file, in mathcomp.solvable.sylow]
    Sylow [def, in mathcomp.solvable.pgroup]
    Sylow's_theorem [prf, in mathcomp.solvable.sylow]
    Sylow1 [prf, in mathcomp.solvable.pgroup]
    Sylow_exists [prf, in mathcomp.solvable.sylow]
    Sylow_gen [prf, in mathcomp.solvable.sylow]
    Sylow_Jsub [prf, in mathcomp.solvable.sylow]
    Sylow_setI_normal [prf, in mathcomp.solvable.sylow]
    Sylow_subJ [prf, in mathcomp.solvable.sylow]
    Sylow_subnorm [prf, in mathcomp.solvable.sylow]
    Sylow_superset [prf, in mathcomp.solvable.sylow]
    Sylow_trans [prf, in mathcomp.solvable.sylow]
    Sylow_transversal_gen [prf, in mathcomp.solvable.sylow]
    SylowJ [prf, in mathcomp.solvable.pgroup]
    SylowP [prf, in mathcomp.solvable.pgroup]
    Sylvester_mx [def, in mathcomp.algebra.mxpoly]
    Sylvester_mxE [prf, in mathcomp.algebra.mxpoly]
    Sym [def, in mathcomp.solvable.alt]
    Sym [def, in mathcomp.finite_group.perm]
    sym_connect_sym [prf, in mathcomp.boot.fingraph]
    Sym_group [def, in mathcomp.solvable.alt]
    Sym_group [def, in mathcomp.finite_group.perm]
    Sym_group_set [prf, in mathcomp.finite_group.perm]
    Sym_trans [prf, in mathcomp.solvable.alt]
    SymE [prf, in mathcomp.finite_group.action]
    symmetric_form [abbrev, in mathcomp.algebra.sesquilinear]
    symmetric_normalmx [prf, in mathcomp.algebra.spectral]
    symmetricmx [abbrev, in mathcomp.algebra.sesquilinear]
    symplectic_type_group_structure [prf, in mathcomp.solvable.extremal]
    Generated by rocqnavi