Files

  • mathcomp

    • Top source

    B (Global Index)

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

    B

    b [abbrev, in mathcomp.classical.functions]
    B [abbrev, in mathcomp.analysis.lebesgue_integral_theory.measurable_fun_approximation]
    Baer_Suzuki [prf, in mathcomp.solvable.sylow]
    Baire [prf, in mathcomp.analysis.sequences]
    ball [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
    ball0 [prf, in mathcomp.analysis.normedtype_theory.num_normedtype]
    ball_ [def, in mathcomp.analysis.topology_theory.pseudometric_structure]
    ball_center [prf, in mathcomp.analysis.topology_theory.pseudometric_structure]
    ball_close [prf, in mathcomp.analysis.topology_theory.separation_axioms]
    ball_ereal_ball_fin_le [prf, in mathcomp.analysis.ereal]
    ball_ereal_ball_fin_lt [prf, in mathcomp.analysis.ereal]
    ball_filter [inst, in mathcomp.analysis.topology_theory.pseudometric_structure]
    ball_gt0 [prf, in mathcomp.analysis.normedtype_theory.matrix_normedtype]
    ball_hausdorff [prf, in mathcomp.analysis.topology_theory.separation_axioms]
    ball_inj [prf, in mathcomp.analysis.normedtype_theory.vitali_lemma]
    ball_itv [prf, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
    ball_norm [abbrev, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
    ball_norm_center [prf, in mathcomp.analysis.topology_theory.pseudometric_structure]
    ball_norm_dec [prf, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
    ball_norm_le [prf, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
    ball_norm_sym [prf, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
    ball_norm_symmetric [prf, in mathcomp.analysis.topology_theory.pseudometric_structure]
    ball_norm_triangle [prf, in mathcomp.analysis.topology_theory.pseudometric_structure]
    ball_normE [prf, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
    ball_open [prf, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
    ball_open_nbhs [prf, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
    ball_prod_normE [prf, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
    ball_split [prf, in mathcomp.analysis.topology_theory.pseudometric_structure]
    ball_splitl [prf, in mathcomp.analysis.topology_theory.pseudometric_structure]
    ball_splitr [prf, in mathcomp.analysis.topology_theory.pseudometric_structure]
    ball_subspace_ball [prf, in mathcomp.analysis.topology_theory.subspace_topology]
    ball_sym [prf, in mathcomp.analysis.topology_theory.pseudometric_structure]
    ball_symE [prf, in mathcomp.analysis.topology_theory.pseudometric_structure]
    ball_triangle [prf, in mathcomp.analysis.topology_theory.pseudometric_structure]
    ballE [prf, in mathcomp.analysis.normedtype_theory.vitali_lemma]
    ballEmdist [def, in mathcomp.analysis.topology_theory.metric_structure]
    ballxx [prf, in mathcomp.analysis.topology_theory.pseudometric_structure]
    banach_fixed_point [prf, in mathcomp.analysis.sequences]
    Banach_Steinhauss [prf, in mathcomp.analysis.sequences]
    band [abbrev, in mathcomp.algebra.mxpoly]
    base_aspaceOver [prf, in mathcomp.field.fieldext]
    base_inseparable [prf, in mathcomp.field.separable]
    base_moduleOver [prf, in mathcomp.field.fieldext]
    base_separable [prf, in mathcomp.field.separable]
    base_vspaceOver [prf, in mathcomp.field.fieldext]
    baseAspace [def, in mathcomp.field.fieldext]
    baseAspace_suproof [prf, in mathcomp.field.fieldext]
    baseField_scale [def, in mathcomp.field.fieldext]
    baseField_scale1 [prf, in mathcomp.field.fieldext]
    baseField_scaleA [prf, in mathcomp.field.fieldext]
    baseField_scaleAl [prf, in mathcomp.field.fieldext]
    baseField_scaleDl [prf, in mathcomp.field.fieldext]
    baseField_scaleDr [prf, in mathcomp.field.fieldext]
    baseField_scaleE [prf, in mathcomp.field.fieldext]
    baseField_vectMixin [prf, in mathcomp.field.fieldext]
    baseFieldType [def, in mathcomp.field.fieldext]
    BaseFinGroup [abbrev, in mathcomp.finite_group.fingroup]
    BaseFinGroup [mod, in mathcomp.finite_group.fingroup]
    BaseFinGroup.arg_sort [abbrev, in mathcomp.finite_group.fingroup]
    BaseFinGroup.clone [abbrev, in mathcomp.finite_group.fingroup]
    BaseFinGroup.copy [abbrev, in mathcomp.finite_group.fingroup]
    BaseFinGroup.on [abbrev, in mathcomp.finite_group.fingroup]
    BaseFinGroup.sort [abbrev, in mathcomp.finite_group.fingroup]
    BaseFinGroup_isGroup [abbrev, in mathcomp.finite_group.fingroup]
    BaseFinGroup_isGroup [mod, in mathcomp.finite_group.fingroup]
    BaseFinGroup_isGroup.Build [abbrev, in mathcomp.finite_group.fingroup]
    baseFinGroupType [abbrev, in mathcomp.finite_group.fingroup]
    BaseGroup [abbrev, in mathcomp.boot.monoid]
    BaseGroup [mod, in mathcomp.boot.monoid]
    BaseGroup.axioms_ [rec, in mathcomp.boot.monoid]
    BaseGroup.class [proj, in mathcomp.boot.monoid]
    BaseGroup.clone [abbrev, in mathcomp.boot.monoid]
    BaseGroup.copy [abbrev, in mathcomp.boot.monoid]
    BaseGroup.Exports [mod, in mathcomp.boot.monoid]
    BaseGroup.Exports.baseGroupType [abbrev, in mathcomp.boot.monoid]
    BaseGroup.monoid_hasInv_mixin [proj, in mathcomp.boot.monoid]
    BaseGroup.monoid_hasMul_mixin [proj, in mathcomp.boot.monoid]
    BaseGroup.monoid_hasOne_mixin [proj, in mathcomp.boot.monoid]
    BaseGroup.on [abbrev, in mathcomp.boot.monoid]
    BaseGroup.on_ [abbrev, in mathcomp.boot.monoid]
    BaseGroup.pack_ [def, in mathcomp.boot.monoid]
    BaseGroup.phant_clone [def, in mathcomp.boot.monoid]
    BaseGroup.phant_on_ [def, in mathcomp.boot.monoid]
    BaseGroup.sort [proj, in mathcomp.boot.monoid]
    BaseGroup.type [rec, in mathcomp.boot.monoid]
    BaseGroupElpiOperations [mod, in mathcomp.boot.monoid]
    BaseUMagma [abbrev, in mathcomp.boot.monoid]
    BaseUMagma [mod, in mathcomp.boot.monoid]
    BaseUMagma.axioms_ [rec, in mathcomp.boot.monoid]
    BaseUMagma.class [proj, in mathcomp.boot.monoid]
    BaseUMagma.clone [abbrev, in mathcomp.boot.monoid]
    BaseUMagma.copy [abbrev, in mathcomp.boot.monoid]
    BaseUMagma.Exports [mod, in mathcomp.boot.monoid]
    BaseUMagma.Exports.baseUMagmaType [abbrev, in mathcomp.boot.monoid]
    BaseUMagma.monoid_hasMul_mixin [proj, in mathcomp.boot.monoid]
    BaseUMagma.monoid_hasOne_mixin [proj, in mathcomp.boot.monoid]
    BaseUMagma.on [abbrev, in mathcomp.boot.monoid]
    BaseUMagma.on_ [abbrev, in mathcomp.boot.monoid]
    BaseUMagma.pack_ [def, in mathcomp.boot.monoid]
    BaseUMagma.phant_clone [def, in mathcomp.boot.monoid]
    BaseUMagma.phant_on_ [def, in mathcomp.boot.monoid]
    BaseUMagma.sort [proj, in mathcomp.boot.monoid]
    BaseUMagma.type [rec, in mathcomp.boot.monoid]
    BaseUMagma_isUMagma [abbrev, in mathcomp.boot.monoid]
    BaseUMagma_isUMagma [mod, in mathcomp.boot.monoid]
    BaseUMagma_isUMagma.axioms [abbrev, in mathcomp.boot.monoid]
    BaseUMagma_isUMagma.axioms_ [rec, in mathcomp.boot.monoid]
    BaseUMagma_isUMagma.Build [abbrev, in mathcomp.boot.monoid]
    BaseUMagma_isUMagma.Exports [mod, in mathcomp.boot.monoid]
    BaseUMagma_isUMagma.identity_builder [def, in mathcomp.boot.monoid]
    BaseUMagma_isUMagma.mul1g [proj, in mathcomp.boot.monoid]
    BaseUMagma_isUMagma.mulg1 [proj, in mathcomp.boot.monoid]
    BaseUMagma_isUMagma.phant_axioms [def, in mathcomp.boot.monoid]
    BaseUMagma_isUMagma.phant_Build [def, in mathcomp.boot.monoid]
    BaseUMagmaElpiOperations [mod, in mathcomp.boot.monoid]
    baseVspace [def, in mathcomp.field.fieldext]
    baseVspace_module [prf, in mathcomp.field.fieldext]
    basis [def, in mathcomp.analysis.topology_theory.topology_structure]
    basis_free [prf, in mathcomp.algebra.vector]
    basis_mem [prf, in mathcomp.algebra.vector]
    basis_not0 [prf, in mathcomp.algebra.vector]
    basis_of [def, in mathcomp.algebra.vector]
    basisEdim [prf, in mathcomp.algebra.vector]
    basisEfree [prf, in mathcomp.algebra.vector]
    before_find [prf, in mathcomp.boot.seq]
    behead [def, in mathcomp.boot.seq]
    behead_bseq [def, in mathcomp.boot.tuple]
    behead_bseqP [prf, in mathcomp.boot.tuple]
    behead_map [prf, in mathcomp.boot.seq]
    behead_tuple [def, in mathcomp.boot.tuple]
    behead_tupleP [prf, in mathcomp.boot.tuple]
    belast [def, in mathcomp.boot.seq]
    belast_bseq [def, in mathcomp.boot.tuple]
    belast_bseqP [prf, in mathcomp.boot.tuple]
    belast_cat [prf, in mathcomp.boot.seq]
    belast_map [prf, in mathcomp.boot.seq]
    belast_rcons [prf, in mathcomp.boot.seq]
    belast_tuple [def, in mathcomp.boot.tuple]
    belast_tupleP [prf, in mathcomp.boot.tuple]
    bernoulli [abbrev, in mathcomp.analysis.probability_theory.bernoulli_distribution]
    bernoulli_dirac [prf, in mathcomp.analysis.probability_theory.bernoulli_distribution]
    bernoulli_distribution [file, in mathcomp.analysis.probability_theory.bernoulli_distribution]
    bernoulli_pmf [def, in mathcomp.analysis.probability_theory.bernoulli_distribution]
    bernoulli_pmf1 [prf, in mathcomp.analysis.probability_theory.bernoulli_distribution]
    bernoulli_pmf_ge0 [prf, in mathcomp.analysis.probability_theory.bernoulli_distribution]
    bernoulli_prob [def, in mathcomp.analysis.probability_theory.bernoulli_distribution]
    bernoulli_probE [prf, in mathcomp.analysis.probability_theory.bernoulli_distribution]
    beta_distribution [file, in mathcomp.analysis.probability_theory.beta_distribution]
    beta_fun [def, in mathcomp.analysis.probability_theory.beta_distribution]
    beta_fun00 [prf, in mathcomp.analysis.probability_theory.beta_distribution]
    beta_fun0n [prf, in mathcomp.analysis.probability_theory.beta_distribution]
    beta_fun11 [prf, in mathcomp.analysis.probability_theory.beta_distribution]
    beta_fun1Sn [prf, in mathcomp.analysis.probability_theory.beta_distribution]
    beta_fun_fact [prf, in mathcomp.analysis.probability_theory.beta_distribution]
    beta_fun_ge0 [prf, in mathcomp.analysis.probability_theory.beta_distribution]
    beta_fun_gt0 [prf, in mathcomp.analysis.probability_theory.beta_distribution]
    beta_fun_sym [prf, in mathcomp.analysis.probability_theory.beta_distribution]
    beta_funE [prf, in mathcomp.analysis.probability_theory.beta_distribution]
    beta_funSnSm [prf, in mathcomp.analysis.probability_theory.beta_distribution]
    beta_funSSnSm [prf, in mathcomp.analysis.probability_theory.beta_distribution]
    beta_pdf [def, in mathcomp.analysis.probability_theory.beta_distribution]
    beta_pdf_ge0 [prf, in mathcomp.analysis.probability_theory.beta_distribution]
    beta_pdf_le_beta_funV [prf, in mathcomp.analysis.probability_theory.beta_distribution]
    beta_prob [def, in mathcomp.analysis.probability_theory.beta_distribution]
    beta_prob01 [prf, in mathcomp.analysis.probability_theory.beta_distribution]
    beta_prob_bernoulli_prob [def, in mathcomp.analysis.probability_theory.beta_distribution]
    beta_prob_bernoulli_probE [prf, in mathcomp.analysis.probability_theory.beta_distribution]
    beta_prob_dom [prf, in mathcomp.analysis.probability_theory.beta_distribution]
    beta_prob_fin_num [prf, in mathcomp.analysis.probability_theory.beta_distribution]
    beta_prob_integrable [prf, in mathcomp.analysis.probability_theory.beta_distribution]
    beta_prob_integrable_dirac [prf, in mathcomp.analysis.probability_theory.beta_distribution]
    beta_prob_integrable_onem [prf, in mathcomp.analysis.probability_theory.beta_distribution]
    beta_prob_integrable_onem_dirac [prf, in mathcomp.analysis.probability_theory.beta_distribution]
    beta_prob_uniform [prf, in mathcomp.analysis.probability_theory.beta_distribution]
    Bezout_rec [def, in mathcomp.boot.div]
    Bezoutl [prf, in mathcomp.boot.div]
    Bezoutr [prf, in mathcomp.boot.div]
    Bezoutz [prf, in mathcomp.algebra.intdiv]
    bgFunc_id [def, in mathcomp.solvable.gfunctor]
    big1 [prf, in mathcomp.boot.bigop]
    big1_eq [prf, in mathcomp.boot.bigop]
    big1_fset [prf, in mathcomp.finmap.finmap]
    big1_idem [prf, in mathcomp.boot.bigop]
    big1_seq [prf, in mathcomp.boot.bigop]
    big_AC_mk_monoid [prf, in mathcomp.boot.bigop]
    big_add1 [prf, in mathcomp.boot.bigop]
    big_addn [prf, in mathcomp.boot.bigop]
    big_all [prf, in mathcomp.boot.bigop]
    big_all_cond [prf, in mathcomp.boot.bigop]
    big_allpairs [prf, in mathcomp.boot.bigop]
    big_allpairs_dep [prf, in mathcomp.boot.bigop]
    big_allpairs_dep_idem [prf, in mathcomp.boot.bigop]
    big_allpairs_idem [prf, in mathcomp.boot.bigop]
    big_andbC [prf, in mathcomp.boot.bigop]
    big_andE [prf, in mathcomp.boot.bigop]
    big_bool [prf, in mathcomp.boot.bigop]
    big_cards1 [prf, in mathcomp.boot.finset]
    big_cat [prf, in mathcomp.boot.bigop]
    big_cat_idem [prf, in mathcomp.boot.bigop]
    big_cat_nat [prf, in mathcomp.boot.bigop]
    big_cat_nat_idem [prf, in mathcomp.boot.bigop]
    big_cat_nested [prf, in mathcomp.boot.bigop]
    big_cat_ordfun [prf, in mathcomp.boot.bigop]
    big_catl [prf, in mathcomp.boot.bigop]
    big_catr [prf, in mathcomp.boot.bigop]
    big_change_idx [prf, in mathcomp.boot.bigop]
    big_coef_npoly [prf, in mathcomp.algebra.qpoly]
    big_condT [prf, in mathcomp.boot.bigop]
    big_cons [prf, in mathcomp.boot.bigop]
    big_const [prf, in mathcomp.boot.bigop]
    big_const_idem [prf, in mathcomp.boot.bigop]
    big_const_nat [prf, in mathcomp.boot.bigop]
    big_const_ord [prf, in mathcomp.boot.bigop]
    big_const_seq [prf, in mathcomp.boot.bigop]
    big_distr_big [prf, in mathcomp.boot.bigop]
    big_distr_big_dep [prf, in mathcomp.boot.bigop]
    big_distrl [prf, in mathcomp.boot.bigop]
    big_distrlr [prf, in mathcomp.boot.bigop]
    big_distrr [prf, in mathcomp.boot.bigop]
    big_endo [prf, in mathcomp.boot.bigop]
    big_enum [prf, in mathcomp.boot.bigop]
    big_enum_cond [prf, in mathcomp.boot.bigop]
    big_enum_rank [prf, in mathcomp.boot.bigop]
    big_enum_rank_cond [prf, in mathcomp.boot.bigop]
    big_enum_spec [ind, in mathcomp.boot.bigop]
    big_enum_val [prf, in mathcomp.boot.bigop]
    big_enum_val_cond [prf, in mathcomp.boot.bigop]
    big_enumP [prf, in mathcomp.boot.bigop]
    BIG_F [abbrev, in mathcomp.boot.bigop]
    big_filter [prf, in mathcomp.boot.bigop]
    big_filter_cond [prf, in mathcomp.boot.bigop]
    big_flatten [prf, in mathcomp.boot.bigop]
    big_fprod [prf, in mathcomp.boot.finset]
    big_fprod_dep [prf, in mathcomp.boot.finset]
    big_fset [prf, in mathcomp.finmap.finmap]
    big_fset0 [prf, in mathcomp.finmap.finmap]
    big_fset1 [prf, in mathcomp.finmap.finmap]
    big_fset_condE [prf, in mathcomp.finmap.finmap]
    big_fset_incl [prf, in mathcomp.finmap.finmap]
    big_fsetD1 [prf, in mathcomp.finmap.finmap]
    big_fsetID [prf, in mathcomp.finmap.finmap]
    big_fsetIDcond [prf, in mathcomp.finmap.finmap]
    big_fsetU1 [prf, in mathcomp.finmap.finmap]
    big_geq [prf, in mathcomp.boot.bigop]
    big_geq_mkord [prf, in mathcomp.boot.bigop]
    big_has [prf, in mathcomp.boot.bigop]
    big_has_cond [prf, in mathcomp.boot.bigop]
    big_hasC [prf, in mathcomp.boot.bigop]
    big_id_idem [prf, in mathcomp.boot.bigop]
    big_id_idem_AC [prf, in mathcomp.boot.bigop]
    big_if [prf, in mathcomp.boot.bigop]
    big_image [prf, in mathcomp.boot.bigop]
    big_image_cond [prf, in mathcomp.boot.bigop]
    big_imfset [prf, in mathcomp.finmap.finmap]
    big_imfset2 [prf, in mathcomp.finmap.finmap]
    big_imset [prf, in mathcomp.boot.finset]
    big_imset_cond [prf, in mathcomp.boot.finset]
    big_imset_idem [prf, in mathcomp.boot.finset]
    big_ind [prf, in mathcomp.boot.bigop]
    big_ind2 [prf, in mathcomp.boot.bigop]
    big_ind3 [prf, in mathcomp.boot.bigop]
    big_index_uniq [prf, in mathcomp.boot.bigop]
    big_lex_bot [prf, in mathcomp.classical.classical_orders]
    big_lex_top [prf, in mathcomp.classical.classical_orders]
    big_lexi_le [def, in mathcomp.classical.classical_orders]
    big_lexi_le_anti [prf, in mathcomp.classical.classical_orders]
    big_lexi_le_reflexive [prf, in mathcomp.classical.classical_orders]
    big_lexi_le_total [prf, in mathcomp.classical.classical_orders]
    big_lexi_le_trans [prf, in mathcomp.classical.classical_orders]
    big_lexi_ord_anti [prf, in mathcomp.classical.classical_orders]
    big_lexi_ord_reflexive [prf, in mathcomp.classical.classical_orders]
    big_lexi_ord_total [prf, in mathcomp.classical.classical_orders]
    big_lexi_ord_trans [prf, in mathcomp.classical.classical_orders]
    big_lexi_order [def, in mathcomp.classical.classical_orders]
    big_lexi_order_between [prf, in mathcomp.classical.classical_orders]
    big_lexi_order_interval_prefix [prf, in mathcomp.classical.classical_orders]
    big_lexi_order_prefix_closed_itv [prf, in mathcomp.classical.classical_orders]
    big_lexi_order_prefix_gt [prf, in mathcomp.classical.classical_orders]
    big_lexi_order_prefix_lt [prf, in mathcomp.classical.classical_orders]
    big_load [prf, in mathcomp.boot.bigop]
    big_ltn [prf, in mathcomp.boot.bigop]
    big_ltn_cond [prf, in mathcomp.boot.bigop]
    big_map [prf, in mathcomp.boot.bigop]
    big_map_id [prf, in mathcomp.boot.bigop]
    big_mask [prf, in mathcomp.boot.bigop]
    big_mask_tuple [prf, in mathcomp.boot.bigop]
    big_mk_option_monoid [prf, in mathcomp.boot.bigop]
    big_mkcond [prf, in mathcomp.boot.bigop]
    big_mkcond_idem [prf, in mathcomp.boot.bigop]
    big_mkcondl [prf, in mathcomp.boot.bigop]
    big_mkcondl_idem [prf, in mathcomp.boot.bigop]
    big_mkcondr [prf, in mathcomp.boot.bigop]
    big_mkcondr_idem [prf, in mathcomp.boot.bigop]
    big_mknat [prf, in mathcomp.boot.bigop]
    big_mkord [prf, in mathcomp.boot.bigop]
    big_morph [prf, in mathcomp.boot.bigop]
    big_morph_in [prf, in mathcomp.boot.bigop]
    big_mset [prf, in mathcomp.finmap.multiset]
    big_mset0 [prf, in mathcomp.finmap.multiset]
    big_msetn [prf, in mathcomp.finmap.multiset]
    big_nat [prf, in mathcomp.boot.bigop]
    big_nat1 [prf, in mathcomp.boot.bigop]
    big_nat1_cond_eq [prf, in mathcomp.boot.bigop]
    big_nat1_eq [prf, in mathcomp.boot.bigop]
    big_nat1_id [prf, in mathcomp.boot.bigop]
    big_nat_cond [prf, in mathcomp.boot.bigop]
    big_nat_mul [prf, in mathcomp.boot.bigop]
    big_nat_recl [prf, in mathcomp.boot.bigop]
    big_nat_recr [prf, in mathcomp.boot.bigop]
    big_nat_rev [prf, in mathcomp.boot.bigop]
    big_nat_widen [prf, in mathcomp.boot.bigop]
    big_nat_widenl [prf, in mathcomp.boot.bigop]
    big_nil [prf, in mathcomp.boot.bigop]
    big_nseq [prf, in mathcomp.boot.bigop]
    big_nseq_cond [prf, in mathcomp.boot.bigop]
    big_nth [prf, in mathcomp.boot.bigop]
    big_only1 [prf, in mathcomp.boot.bigop]
    big_ord0 [prf, in mathcomp.boot.bigop]
    big_ord1 [prf, in mathcomp.boot.bigop]
    big_ord1 [abbrev, in mathcomp.algebra.zmodp]
    big_ord1_cond [prf, in mathcomp.boot.bigop]
    big_ord1_cond [abbrev, in mathcomp.algebra.zmodp]
    big_ord1_cond_eq [prf, in mathcomp.boot.bigop]
    big_ord1_eq [prf, in mathcomp.boot.bigop]
    big_ord_narrow [prf, in mathcomp.boot.bigop]
    big_ord_narrow_cond [prf, in mathcomp.boot.bigop]
    big_ord_narrow_cond_leq [prf, in mathcomp.boot.bigop]
    big_ord_narrow_leq [prf, in mathcomp.boot.bigop]
    big_ord_recl [prf, in mathcomp.boot.bigop]
    big_ord_recr [prf, in mathcomp.boot.bigop]
    big_ord_widen [prf, in mathcomp.boot.bigop]
    big_ord_widen_cond [prf, in mathcomp.boot.bigop]
    big_ord_widen_leq [prf, in mathcomp.boot.bigop]
    big_orE [prf, in mathcomp.boot.bigop]
    BIG_P [abbrev, in mathcomp.boot.bigop]
    big_pmap [prf, in mathcomp.boot.bigop]
    big_pred0 [prf, in mathcomp.boot.bigop]
    big_pred0_eq [prf, in mathcomp.boot.bigop]
    big_pred1 [prf, in mathcomp.boot.bigop]
    big_pred1_eq [prf, in mathcomp.boot.bigop]
    big_pred1_eq_id [prf, in mathcomp.boot.bigop]
    big_pred1_id [prf, in mathcomp.boot.bigop]
    big_rcons [prf, in mathcomp.boot.bigop]
    big_rcons_op [prf, in mathcomp.boot.bigop]
    big_rec [prf, in mathcomp.boot.bigop]
    big_rec2 [prf, in mathcomp.boot.bigop]
    big_rec3 [prf, in mathcomp.boot.bigop]
    big_rem [prf, in mathcomp.boot.bigop]
    big_rem_AC [prf, in mathcomp.boot.bigop]
    big_rev [prf, in mathcomp.boot.bigop]
    big_rev_mkord [prf, in mathcomp.boot.bigop]
    big_rmcond [prf, in mathcomp.boot.bigop]
    big_rmcond_idem [prf, in mathcomp.boot.bigop]
    big_rmcond_in [prf, in mathcomp.boot.bigop]
    big_rmcond_in_idem [prf, in mathcomp.boot.bigop]
    big_seq [prf, in mathcomp.boot.bigop]
    big_seq1 [prf, in mathcomp.boot.bigop]
    big_seq1_id [prf, in mathcomp.boot.bigop]
    big_seq_cond [prf, in mathcomp.boot.bigop]
    big_seq_fset0 [prf, in mathcomp.finmap.finmap]
    big_seq_fset1 [prf, in mathcomp.finmap.finmap]
    big_seq_fsetE [prf, in mathcomp.finmap.finmap]
    big_set [prf, in mathcomp.boot.finset]
    big_set0 [prf, in mathcomp.boot.finset]
    big_set1 [prf, in mathcomp.boot.finset]
    big_set1E [prf, in mathcomp.boot.finset]
    big_setD1 [prf, in mathcomp.boot.finset]
    big_setID [prf, in mathcomp.boot.finset]
    big_setIDcond [prf, in mathcomp.boot.finset]
    big_setU [prf, in mathcomp.boot.finset]
    big_setU1 [prf, in mathcomp.boot.finset]
    big_setU_cond [prf, in mathcomp.boot.finset]
    big_split [prf, in mathcomp.boot.bigop]
    big_split_idem [prf, in mathcomp.boot.bigop]
    big_split_ord [prf, in mathcomp.boot.bigop]
    big_split_ord_idem [prf, in mathcomp.boot.bigop]
    big_sub [prf, in mathcomp.boot.bigop]
    big_sub_cond [prf, in mathcomp.boot.bigop]
    big_subset_idem [prf, in mathcomp.boot.finset]
    big_subset_idem_cond [prf, in mathcomp.boot.finset]
    big_sumType [prf, in mathcomp.boot.bigop]
    big_tag [prf, in mathcomp.boot.finset]
    big_tag_cond [prf, in mathcomp.boot.finset]
    big_tnth [prf, in mathcomp.boot.bigop]
    big_trivIfset [prf, in mathcomp.finmap.finmap]
    big_trivIset [prf, in mathcomp.boot.finset]
    big_trivIset [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    big_trivIset_cond [prf, in mathcomp.boot.finset]
    big_tuple [prf, in mathcomp.boot.bigop]
    big_undup [prf, in mathcomp.boot.bigop]
    big_undup_iterop_count [prf, in mathcomp.boot.bigop]
    big_uniq [prf, in mathcomp.boot.bigop]
    bigA_distr [prf, in mathcomp.boot.finset]
    bigA_distr_big [prf, in mathcomp.boot.bigop]
    bigA_distr_big_dep [prf, in mathcomp.boot.bigop]
    bigA_distr_bigA [prf, in mathcomp.boot.bigop]
    BigBody [constr, in mathcomp.boot.bigop]
    bigbody [ind, in mathcomp.boot.bigop]
    bigcap [def, in mathcomp.classical.classical_sets]
    bigcap0 [prf, in mathcomp.classical.classical_sets]
    bigcap2 [def, in mathcomp.classical.classical_sets]
    bigcap2E [prf, in mathcomp.classical.classical_sets]
    bigcap2inE [prf, in mathcomp.classical.classical_sets]
    bigcap_addn [prf, in mathcomp.classical.classical_sets]
    bigcap_bigcup [prf, in mathcomp.classical.functions]
    bigcap_const [prf, in mathcomp.classical.classical_sets]
    bigcap_fset [prf, in mathcomp.classical.classical_sets]
    bigcap_fset_set [abbrev, in mathcomp.classical.cardinality]
    bigcap_fsetD1 [prf, in mathcomp.classical.classical_sets]
    bigcap_fsetU1 [prf, in mathcomp.classical.classical_sets]
    bigcap_group [def, in mathcomp.finite_group.fingroup]
    bigcap_image [prf, in mathcomp.classical.classical_sets]
    bigcap_inf [prf, in mathcomp.classical.classical_sets]
    bigcap_inf [prf, in mathcomp.boot.finset]
    bigcap_measurable [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    bigcap_measurableType [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    bigcap_min [prf, in mathcomp.boot.finset]
    bigcap_mkcond [prf, in mathcomp.classical.classical_sets]
    bigcap_mkcondl [prf, in mathcomp.classical.classical_sets]
    bigcap_mkcondr [prf, in mathcomp.classical.classical_sets]
    bigcap_mkord [prf, in mathcomp.classical.classical_sets]
    bigcap_p'core [prf, in mathcomp.solvable.pgroup]
    bigcap_seq [prf, in mathcomp.classical.classical_sets]
    bigcap_seq [prf, in mathcomp.boot.finset]
    bigcap_seq_cond [prf, in mathcomp.classical.classical_sets]
    bigcap_set0 [prf, in mathcomp.classical.classical_sets]
    bigcap_set1 [prf, in mathcomp.classical.classical_sets]
    bigcap_set_type [prf, in mathcomp.classical.classical_sets]
    bigcap_setD1 [prf, in mathcomp.classical.classical_sets]
    bigcap_setU [prf, in mathcomp.classical.classical_sets]
    bigcap_setU [prf, in mathcomp.boot.finset]
    bigcap_setU1 [prf, in mathcomp.classical.classical_sets]
    bigcap_splitn [prf, in mathcomp.classical.classical_sets]
    bigcapI [prf, in mathcomp.classical.classical_sets]
    bigcapID [prf, in mathcomp.classical.classical_sets]
    bigcapIl [prf, in mathcomp.classical.classical_sets]
    bigcapIr [prf, in mathcomp.classical.classical_sets]
    bigcapJ [prf, in mathcomp.finite_group.fingroup]
    bigcapmx_inf [prf, in mathcomp.algebra.mxalgebra]
    bigcapP [prf, in mathcomp.boot.finset]
    bigcapsP [prf, in mathcomp.boot.finset]
    bigcapT [prf, in mathcomp.classical.classical_sets]
    bigcapT_measurable [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    bigcapTP [prf, in mathcomp.classical.classical_sets]
    bigcapv_inf [prf, in mathcomp.algebra.vector]
    bigcat_basis [prf, in mathcomp.algebra.vector]
    bigcat_free [prf, in mathcomp.algebra.vector]
    bigcprod_card_dprod [prf, in mathcomp.finite_group.gproduct]
    bigcprod_coprime_dprod [prf, in mathcomp.finite_group.gproduct]
    bigcprodEY [prf, in mathcomp.finite_group.gproduct]
    bigcprodW [prf, in mathcomp.finite_group.gproduct]
    bigcprodWY [prf, in mathcomp.finite_group.gproduct]
    bigcprodYP [prf, in mathcomp.finite_group.gproduct]
    bigcup [def, in mathcomp.classical.classical_sets]
    bigcup0 [prf, in mathcomp.classical.classical_sets]
    bigcup0P [prf, in mathcomp.classical.classical_sets]
    bigcup0P [prf, in mathcomp.boot.finset]
    bigcup2 [def, in mathcomp.classical.classical_sets]
    bigcup2E [prf, in mathcomp.classical.classical_sets]
    bigcup2inE [prf, in mathcomp.classical.classical_sets]
    bigcup_addn [prf, in mathcomp.classical.classical_sets]
    bigcup_ballT [prf, in mathcomp.analysis.normedtype_theory.num_normedtype]
    bigcup_bigcup [prf, in mathcomp.classical.classical_sets]
    bigcup_bigsetU_bigcup [prf, in mathcomp.analysis.sequences]
    bigcup_connected [prf, in mathcomp.analysis.topology_theory.connected]
    bigcup_const [prf, in mathcomp.classical.classical_sets]
    bigcup_countable [prf, in mathcomp.classical.cardinality]
    bigcup_disjoint [prf, in mathcomp.boot.finset]
    bigcup_disjointP [prf, in mathcomp.boot.finset]
    bigcup_finite [prf, in mathcomp.classical.cardinality]
    bigcup_fset [prf, in mathcomp.classical.classical_sets]
    bigcup_fset_set [abbrev, in mathcomp.classical.cardinality]
    bigcup_fset_set_cond [abbrev, in mathcomp.classical.cardinality]
    bigcup_fsetD1 [prf, in mathcomp.classical.classical_sets]
    bigcup_fsetU1 [prf, in mathcomp.classical.classical_sets]
    bigcup_image [prf, in mathcomp.classical.classical_sets]
    bigcup_imset1 [prf, in mathcomp.classical.classical_sets]
    bigcup_itvT [prf, in mathcomp.reals.real_interval]
    bigcup_max [prf, in mathcomp.boot.finset]
    bigcup_measurable [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    bigcup_mkcond [prf, in mathcomp.classical.classical_sets]
    bigcup_mkcondl [prf, in mathcomp.classical.classical_sets]
    bigcup_mkcondr [prf, in mathcomp.classical.classical_sets]
    bigcup_mkord [prf, in mathcomp.classical.classical_sets]
    bigcup_mkord_ord [prf, in mathcomp.classical.classical_sets]
    bigcup_negative_set [prf, in mathcomp.analysis.charge]
    bigcup_nonempty [prf, in mathcomp.classical.classical_sets]
    bigcup_ointsub [def, in mathcomp.analysis.normedtype_theory.num_normedtype]
    bigcup_ointsub0 [prf, in mathcomp.analysis.normedtype_theory.num_normedtype]
    bigcup_ointsub_mem [prf, in mathcomp.analysis.normedtype_theory.num_normedtype]
    bigcup_ointsub_sub [prf, in mathcomp.analysis.normedtype_theory.num_normedtype]
    bigcup_ointsub_sup [prf, in mathcomp.analysis.normedtype_theory.num_normedtype]
    bigcup_ointsubxx [prf, in mathcomp.analysis.normedtype_theory.normed_module]
    bigcup_open [prf, in mathcomp.analysis.topology_theory.topology_structure]
    bigcup_pred [prf, in mathcomp.classical.classical_sets]
    bigcup_recl [prf, in mathcomp.classical.classical_sets]
    bigcup_seq [prf, in mathcomp.classical.classical_sets]
    bigcup_seq [prf, in mathcomp.boot.finset]
    bigcup_seq_cond [prf, in mathcomp.classical.classical_sets]
    bigcup_set0 [prf, in mathcomp.classical.classical_sets]
    bigcup_set1 [prf, in mathcomp.classical.classical_sets]
    bigcup_set_type [prf, in mathcomp.classical.classical_sets]
    bigcup_setD1 [prf, in mathcomp.classical.classical_sets]
    bigcup_setU [prf, in mathcomp.classical.classical_sets]
    bigcup_setU [prf, in mathcomp.boot.finset]
    bigcup_setU1 [prf, in mathcomp.classical.classical_sets]
    bigcup_setX [prf, in mathcomp.classical.classical_sets]
    bigcup_setX_dep [prf, in mathcomp.classical.classical_sets]
    bigcup_splitn [prf, in mathcomp.classical.classical_sets]
    bigcup_sub [prf, in mathcomp.classical.classical_sets]
    bigcup_subset [prf, in mathcomp.classical.classical_sets]
    bigcup_sup [prf, in mathcomp.classical.classical_sets]
    bigcup_sup [prf, in mathcomp.boot.finset]
    bigcupDr [prf, in mathcomp.classical.classical_sets]
    bigcupID [prf, in mathcomp.classical.classical_sets]
    bigcupJ [prf, in mathcomp.finite_group.fingroup]
    bigcupP [prf, in mathcomp.boot.finset]
    bigcupsP [prf, in mathcomp.boot.finset]
    bigcupT [prf, in mathcomp.classical.classical_sets]
    bigcupT_emeasurable [prf, in mathcomp.analysis.measurable_realfun]
    bigcupT_measurable [def, in mathcomp.analysis.measure_theory.measurable_structure]
    bigcupT_measurable_rat [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    bigcupU [prf, in mathcomp.classical.classical_sets]
    bigcupUl [prf, in mathcomp.classical.classical_sets]
    bigcupUr [prf, in mathcomp.classical.classical_sets]
    bigcupX1l [prf, in mathcomp.classical.classical_sets]
    bigcupX1r [prf, in mathcomp.classical.classical_sets]
    bigD1 [prf, in mathcomp.boot.bigop]
    bigD1_ord [prf, in mathcomp.boot.bigop]
    bigD1_seq [prf, in mathcomp.boot.bigop]
    bigdprod_card [prf, in mathcomp.finite_group.gproduct]
    bigdprod_nil [prf, in mathcomp.solvable.nilpotent]
    bigdprodW [prf, in mathcomp.finite_group.gproduct]
    bigdprodWcp [prf, in mathcomp.finite_group.gproduct]
    bigdprodWY [prf, in mathcomp.finite_group.gproduct]
    bigdprodYP [prf, in mathcomp.finite_group.gproduct]
    bigenough [file, in mathcomp.bigenough.bigenough]
    BigEnough [mod, in mathcomp.bigenough.bigenough]
    BigEnough.big_enough_nat [def, in mathcomp.bigenough.bigenough]
    BigEnough.big_rel_class [proj, in mathcomp.bigenough.bigenough]
    BigEnough.big_rel_class_of [rec, in mathcomp.bigenough.bigenough]
    BigEnough.big_rel_leq_class [def, in mathcomp.bigenough.bigenough]
    BigEnough.big_rel_of [rec, in mathcomp.bigenough.bigenough]
    BigEnough.bigger_than [abbrev, in mathcomp.bigenough.bigenough]
    BigEnough.bigger_than_of [def, in mathcomp.bigenough.bigenough]
    BigEnough.bigger_than_op [proj, in mathcomp.bigenough.bigenough]
    BigEnough.closed [def, in mathcomp.bigenough.bigenough]
    BigEnough.context_big_enough [prf, in mathcomp.bigenough.bigenough]
    BigEnough.instantiate_bigger_than [prf, in mathcomp.bigenough.bigenough]
    BigEnough.leq_big [proj, in mathcomp.bigenough.bigenough]
    BigEnough.leq_big_internal [abbrev, in mathcomp.bigenough.bigenough]
    BigEnough.leq_big_internal_of [def, in mathcomp.bigenough.bigenough]
    BigEnough.leq_big_internal_op [proj, in mathcomp.bigenough.bigenough]
    BigEnough.leq_big_internalE [prf, in mathcomp.bigenough.bigenough]
    BigEnough.next_bigger_than [prf, in mathcomp.bigenough.bigenough]
    BigEnumSpec [constr, in mathcomp.boot.bigop]
    bigfcup_imfset [prf, in mathcomp.finmap.finmap]
    bigfcup_imfset1 [prf, in mathcomp.finmap.finmap]
    bigfcup_sup [prf, in mathcomp.finmap.finmap]
    bigfcup_undup [prf, in mathcomp.finmap.finmap]
    bigfcupP [prf, in mathcomp.finmap.finmap]
    bigfcupsP [prf, in mathcomp.finmap.finmap]
    bigfs [prf, in mathcomp.classical.fsbigop]
    biggcdn_inf [prf, in mathcomp.boot.bigop]
    bigID [prf, in mathcomp.boot.bigop]
    bigID_idem [prf, in mathcomp.boot.bigop]
    biglcmn_sup [prf, in mathcomp.boot.bigop]
    bigmax_eq_arg [prf, in mathcomp.boot.bigop]
    bigmax_geP [prf, in mathcomp.classical.boolp]
    bigmax_gtP [prf, in mathcomp.classical.boolp]
    bigmax_leqP [prf, in mathcomp.boot.bigop]
    bigmax_leqP_seq [prf, in mathcomp.boot.bigop]
    bigmax_nnsfun [def, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
    bigmax_nnsfunE [prf, in mathcomp.analysis.lebesgue_integral_theory.simple_functions]
    bigmax_sup [prf, in mathcomp.boot.bigop]
    bigmax_sup_seq [prf, in mathcomp.classical.unstable]
    bigmax_sup_seq [abbrev, in mathcomp.boot.bigop]
    bigmaxe_fin_num [prf, in mathcomp.reals.constructive_ereal]
    bigmaxn_sup_seq [prf, in mathcomp.boot.bigop]
    bigmin_leP [prf, in mathcomp.classical.boolp]
    bigmin_ltP [prf, in mathcomp.classical.boolp]
    bigO [prf, in mathcomp.analysis.landau]
    bigO0 [def, in mathcomp.analysis.landau]
    bigO_bigO_eqO [prf, in mathcomp.analysis.landau]
    bigO_class [prf, in mathcomp.analysis.landau]
    bigO_clone [def, in mathcomp.analysis.landau]
    bigO_eqO [prf, in mathcomp.analysis.landau]
    bigO_exP [prf, in mathcomp.analysis.landau]
    bigO_fun [proj, in mathcomp.analysis.landau]
    bigO_littleo_eqo [prf, in mathcomp.analysis.landau]
    bigO_spec [ind, in mathcomp.analysis.landau]
    bigO_type [rec, in mathcomp.analysis.landau]
    bigOE [prf, in mathcomp.analysis.landau]
    bigOmega [prf, in mathcomp.analysis.landau]
    bigOmega_class [prf, in mathcomp.analysis.landau]
    bigOmega_clone [def, in mathcomp.analysis.landau]
    bigOmega_fun [proj, in mathcomp.analysis.landau]
    bigOmega_refl [def, in mathcomp.analysis.landau]
    bigOmega_spec [ind, in mathcomp.analysis.landau]
    bigOmega_type [rec, in mathcomp.analysis.landau]
    bigOmegaP [prf, in mathcomp.analysis.landau]
    BigOmegaSpec [constr, in mathcomp.analysis.landau]
    bigop [file, in mathcomp.boot.bigop]
    bigop [abbrev, in mathcomp.boot.bigop]
    bigop [mod, in mathcomp.boot.bigop]
    bigOP [prf, in mathcomp.analysis.landau]
    bigop.body [def, in mathcomp.boot.bigop]
    bigop.unlock [def, in mathcomp.boot.bigop]
    bigop_Locked [modtype, in mathcomp.boot.bigop]
    bigop_Locked.body [ax, in mathcomp.boot.bigop]
    bigop_Locked.unlock [ax, in mathcomp.boot.bigop]
    bigop_unlock [def, in mathcomp.boot.bigop]
    bigop_unlock_subterm [def, in mathcomp.boot.bigop]
    BigOSpec [constr, in mathcomp.analysis.landau]
    bigprodGE [prf, in mathcomp.finite_group.fingroup]
    bigprodGEgen [prf, in mathcomp.finite_group.fingroup]
    bigsetI_bigcap2 [prf, in mathcomp.classical.classical_sets]
    bigsetI_fset_set [prf, in mathcomp.classical.cardinality]
    bigsetI_fset_set_cond [prf, in mathcomp.classical.cardinality]
    bigsetI_measurable [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    bigsetU_bigcup [prf, in mathcomp.classical.classical_sets]
    bigsetU_bigcup2 [prf, in mathcomp.classical.classical_sets]
    bigsetU_compact [prf, in mathcomp.analysis.topology_theory.compact]
    bigsetU_dyadic_itv [prf, in mathcomp.analysis.lebesgue_integral_theory.measurable_fun_approximation]
    bigsetU_fset_set [prf, in mathcomp.classical.cardinality]
    bigsetU_fset_set_cond [prf, in mathcomp.classical.cardinality]
    bigsetU_measurable [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    bigsetU_seqD [prf, in mathcomp.analysis.sequences]
    bigsetU_seqDU [prf, in mathcomp.analysis.sequences]
    bigsetU_sup [prf, in mathcomp.classical.classical_sets]
    bigTheta [prf, in mathcomp.analysis.landau]
    bigTheta_class [prf, in mathcomp.analysis.landau]
    bigTheta_clone [def, in mathcomp.analysis.landau]
    bigTheta_fun [proj, in mathcomp.analysis.landau]
    bigTheta_refl [def, in mathcomp.analysis.landau]
    bigTheta_spec [ind, in mathcomp.analysis.landau]
    bigTheta_type [rec, in mathcomp.analysis.landau]
    bigThetaE [prf, in mathcomp.analysis.landau]
    bigThetaP [prf, in mathcomp.analysis.landau]
    BigThetaSpec [constr, in mathcomp.analysis.landau]
    bigU [prf, in mathcomp.boot.bigop]
    bigU_idem [prf, in mathcomp.boot.bigop]
    bij [prf, in mathcomp.classical.functions]
    Bij [abbrev, in mathcomp.classical.functions]
    Bij [mod, in mathcomp.classical.functions]
    Bij.axioms_ [rec, in mathcomp.classical.functions]
    Bij.class [proj, in mathcomp.classical.functions]
    Bij.clone [abbrev, in mathcomp.classical.functions]
    Bij.copy [abbrev, in mathcomp.classical.functions]
    Bij.Exports [mod, in mathcomp.classical.functions]
    Bij.Exports.join_functions_Bij_between_functions_Inject_and_functions_Surject [def, in mathcomp.classical.functions]
    Bij.Exports.join_functions_Bij_between_functions_Inject_and_functions_SurjFun [def, in mathcomp.classical.functions]
    Bij.Exports.join_functions_Bij_between_functions_InjFun_and_functions_Surject [def, in mathcomp.classical.functions]
    Bij.Exports.join_functions_Bij_between_functions_InjFun_and_functions_SurjFun [def, in mathcomp.classical.functions]
    Bij.functions_isFun_mixin [proj, in mathcomp.classical.functions]
    Bij.functions_OInv_Can_mixin [proj, in mathcomp.classical.functions]
    Bij.functions_OInv_CanV_mixin [proj, in mathcomp.classical.functions]
    Bij.functions_OInv_mixin [proj, in mathcomp.classical.functions]
    Bij.on [abbrev, in mathcomp.classical.functions]
    Bij.on_ [abbrev, in mathcomp.classical.functions]
    Bij.pack_ [def, in mathcomp.classical.functions]
    Bij.phant_clone [def, in mathcomp.classical.functions]
    Bij.phant_on_ [def, in mathcomp.classical.functions]
    Bij.sort [proj, in mathcomp.classical.functions]
    Bij.type [rec, in mathcomp.classical.functions]
    bij_eq [prf, in mathcomp.boot.eqtype]
    bij_eq_card [prf, in mathcomp.boot.fintype]
    bij_forall [prf, in mathcomp.classical.unstable]
    bij_II_D1 [prf, in mathcomp.classical.functions]
    bij_of_set_bijection [def, in mathcomp.classical.functions]
    bij_olift [prf, in mathcomp.classical.functions]
    bij_omap [prf, in mathcomp.classical.functions]
    bij_on_codom [prf, in mathcomp.boot.fintype]
    bij_on_image [prf, in mathcomp.boot.fintype]
    bij_sub [prf, in mathcomp.classical.functions]
    bij_sub_setUll [prf, in mathcomp.classical.functions]
    bij_sub_setUlr [prf, in mathcomp.classical.functions]
    bij_sub_setUrl [prf, in mathcomp.classical.functions]
    bij_sub_setUrr [prf, in mathcomp.classical.functions]
    bij_sub_sym [prf, in mathcomp.classical.functions]
    bij_subl [prf, in mathcomp.classical.functions]
    bij_subr [prf, in mathcomp.classical.functions]
    bijection_of_bijective [def, in mathcomp.classical.functions]
    bijective_contract [prf, in mathcomp.analysis.ereal]
    BijElpiOperations [mod, in mathcomp.classical.functions]
    bijPex [prf, in mathcomp.classical.cardinality]
    bijpinv_bij [prf, in mathcomp.classical.functions]
    bijTT [prf, in mathcomp.classical.functions]
    BijTT [abbrev, in mathcomp.classical.functions]
    BijTT [mod, in mathcomp.classical.functions]
    BijTT.axioms [abbrev, in mathcomp.classical.functions]
    BijTT.axioms_ [rec, in mathcomp.classical.functions]
    BijTT.bij [proj, in mathcomp.classical.functions]
    BijTT.Build [abbrev, in mathcomp.classical.functions]
    BijTT.Exports [mod, in mathcomp.classical.functions]
    BijTT.phant_axioms [def, in mathcomp.classical.functions]
    BijTT.phant_Build [def, in mathcomp.classical.functions]
    Bilinear [abbrev, in mathcomp.algebra.sesquilinear]
    Bilinear [mod, in mathcomp.algebra.sesquilinear]
    Bilinear.axioms_ [rec, in mathcomp.algebra.sesquilinear]
    Bilinear.class [proj, in mathcomp.algebra.sesquilinear]
    Bilinear.clone [abbrev, in mathcomp.algebra.sesquilinear]
    Bilinear.copy [abbrev, in mathcomp.algebra.sesquilinear]
    Bilinear.Exports [mod, in mathcomp.algebra.sesquilinear]
    Bilinear.Exports.bilinear [abbrev, in mathcomp.algebra.sesquilinear]
    Bilinear.on [abbrev, in mathcomp.algebra.sesquilinear]
    Bilinear.on_ [abbrev, in mathcomp.algebra.sesquilinear]
    Bilinear.pack_ [def, in mathcomp.algebra.sesquilinear]
    Bilinear.phant_clone [def, in mathcomp.algebra.sesquilinear]
    Bilinear.phant_on_ [def, in mathcomp.algebra.sesquilinear]
    Bilinear.sesquilinear_isBilinear_mixin [proj, in mathcomp.algebra.sesquilinear]
    Bilinear.sort [proj, in mathcomp.algebra.sesquilinear]
    Bilinear.type [rec, in mathcomp.algebra.sesquilinear]
    bilinear_eqo [prf, in mathcomp.analysis.derive]
    bilinear_for [def, in mathcomp.algebra.sesquilinear]
    bilinear_isBilinear [abbrev, in mathcomp.algebra.sesquilinear]
    bilinear_isBilinear [mod, in mathcomp.algebra.sesquilinear]
    bilinear_isBilinear.axioms [abbrev, in mathcomp.algebra.sesquilinear]
    bilinear_isBilinear.axioms_ [rec, in mathcomp.algebra.sesquilinear]
    bilinear_isBilinear.Build [abbrev, in mathcomp.algebra.sesquilinear]
    bilinear_isBilinear.Exports [mod, in mathcomp.algebra.sesquilinear]
    bilinear_isBilinear.phant_axioms [def, in mathcomp.algebra.sesquilinear]
    bilinear_isBilinear.phant_Build [def, in mathcomp.algebra.sesquilinear]
    bilinear_schwarz [prf, in mathcomp.analysis.derive]
    BilinearElpiOperations [mod, in mathcomp.algebra.sesquilinear]
    BilinearExports [mod, in mathcomp.algebra.sesquilinear]
    BilinearExports.Bilinear [mod, in mathcomp.algebra.sesquilinear]
    BilinearExports.Bilinear.bilinear [abbrev, in mathcomp.algebra.sesquilinear]
    BilinearExports.Bilinear.biscalar [abbrev, in mathcomp.algebra.sesquilinear]
    BilinearExports.Bilinear.map_at_both [def, in mathcomp.algebra.sesquilinear]
    BilinearExports.Bilinear.map_at_left [def, in mathcomp.algebra.sesquilinear]
    BilinearExports.Bilinear.map_at_right [def, in mathcomp.algebra.sesquilinear]
    BilinearExports.Bilinear.map_class [def, in mathcomp.algebra.sesquilinear]
    BilinearExports.Bilinear.map_for_both [rec, in mathcomp.algebra.sesquilinear]
    BilinearExports.Bilinear.map_for_both_map [proj, in mathcomp.algebra.sesquilinear]
    BilinearExports.Bilinear.map_for_left [rec, in mathcomp.algebra.sesquilinear]
    BilinearExports.Bilinear.map_for_left_map [proj, in mathcomp.algebra.sesquilinear]
    BilinearExports.Bilinear.map_for_right [rec, in mathcomp.algebra.sesquilinear]
    BilinearExports.Bilinear.map_for_right_map [proj, in mathcomp.algebra.sesquilinear]
    BilinearExports.Bilinear.mapUUV [abbrev, in mathcomp.algebra.sesquilinear]
    BilinearExports.Bilinear.unify_map_at_both [def, in mathcomp.algebra.sesquilinear]
    BilinearExports.Bilinear.unify_map_at_left [def, in mathcomp.algebra.sesquilinear]
    BilinearExports.Bilinear.unify_map_at_right [def, in mathcomp.algebra.sesquilinear]
    BilinearExports.Bilinear.unwrap [proj, in mathcomp.algebra.sesquilinear]
    BilinearExports.Bilinear.wrap [def, in mathcomp.algebra.sesquilinear]
    BilinearExports.Bilinear.wrapped [rec, in mathcomp.algebra.sesquilinear]
    bin0 [prf, in mathcomp.boot.binomial]
    bin0n [prf, in mathcomp.boot.binomial]
    bin1 [prf, in mathcomp.boot.binomial]
    bin2 [prf, in mathcomp.boot.binomial]
    bin2_sum [prf, in mathcomp.boot.binomial]
    bin2odd [prf, in mathcomp.boot.binomial]
    bin_fact [prf, in mathcomp.boot.binomial]
    bin_factd [prf, in mathcomp.boot.binomial]
    bin_ffact [prf, in mathcomp.boot.binomial]
    bin_ffactd [prf, in mathcomp.boot.binomial]
    bin_gt0 [prf, in mathcomp.boot.binomial]
    bin_of_nat [def, in mathcomp.boot.ssrnat]
    bin_of_natK [prf, in mathcomp.boot.ssrnat]
    bin_of_number [proj, in mathcomp.boot.ssrnat]
    bin_prob [def, in mathcomp.analysis.probability_theory.binomial_distribution]
    bin_prob0 [prf, in mathcomp.analysis.probability_theory.binomial_distribution]
    bin_prob1 [prf, in mathcomp.analysis.probability_theory.binomial_distribution]
    bin_small [prf, in mathcomp.boot.binomial]
    bin_sub [prf, in mathcomp.boot.binomial]
    binary_addv_expr [def, in mathcomp.algebra.vector]
    binary_mxsum_expr [def, in mathcomp.algebra.mxalgebra]
    binary_mxsum_proof [prf, in mathcomp.algebra.mxalgebra]
    binE [prf, in mathcomp.boot.binomial]
    BInfty [constr, in mathcomp.algebra.interval]
    binn [prf, in mathcomp.boot.binomial]
    binnums [file, in mathcomp.algebra.binnums]
    binomial [file, in mathcomp.boot.binomial]
    binomial [def, in mathcomp.boot.binomial]
    binomial [abbrev, in mathcomp.analysis.probability_theory.binomial_distribution]
    binomial_distribution [file, in mathcomp.analysis.probability_theory.binomial_distribution]
    binomial_msum [prf, in mathcomp.analysis.probability_theory.binomial_distribution]
    binomial_pmf [def, in mathcomp.analysis.probability_theory.binomial_distribution]
    binomial_pmf_ge0 [prf, in mathcomp.analysis.probability_theory.binomial_distribution]
    binomial_prob [def, in mathcomp.analysis.probability_theory.binomial_distribution]
    binomial_probE [prf, in mathcomp.analysis.probability_theory.binomial_distribution]
    binS [prf, in mathcomp.boot.binomial]
    binSn [prf, in mathcomp.boot.binomial]
    BiPointed [abbrev, in mathcomp.classical.classical_sets]
    BiPointed [mod, in mathcomp.classical.classical_sets]
    BiPointed.axioms_ [rec, in mathcomp.classical.classical_sets]
    BiPointed.choice_hasChoice_mixin [proj, in mathcomp.classical.classical_sets]
    BiPointed.class [proj, in mathcomp.classical.classical_sets]
    BiPointed.classical_sets_isBiPointed_mixin [proj, in mathcomp.classical.classical_sets]
    BiPointed.clone [abbrev, in mathcomp.classical.classical_sets]
    BiPointed.copy [abbrev, in mathcomp.classical.classical_sets]
    BiPointed.eqtype_hasDecEq_mixin [proj, in mathcomp.classical.classical_sets]
    BiPointed.Exports [mod, in mathcomp.classical.classical_sets]
    BiPointed.Exports.biPointedType [abbrev, in mathcomp.classical.classical_sets]
    BiPointed.on [abbrev, in mathcomp.classical.classical_sets]
    BiPointed.on_ [abbrev, in mathcomp.classical.classical_sets]
    BiPointed.pack_ [def, in mathcomp.classical.classical_sets]
    BiPointed.phant_clone [def, in mathcomp.classical.classical_sets]
    BiPointed.phant_on_ [def, in mathcomp.classical.classical_sets]
    BiPointed.sort [proj, in mathcomp.classical.classical_sets]
    BiPointed.type [rec, in mathcomp.classical.classical_sets]
    BiPointedElpiOperations [mod, in mathcomp.classical.classical_sets]
    BiPointedTopological [abbrev, in mathcomp.analysis.topology_theory.topology_structure]
    BiPointedTopological [mod, in mathcomp.analysis.topology_theory.topology_structure]
    BiPointedTopological.axioms_ [rec, in mathcomp.analysis.topology_theory.topology_structure]
    BiPointedTopological.choice_hasChoice_mixin [proj, in mathcomp.analysis.topology_theory.topology_structure]
    BiPointedTopological.class [proj, in mathcomp.analysis.topology_theory.topology_structure]
    BiPointedTopological.classical_sets_isBiPointed_mixin [proj, in mathcomp.analysis.topology_theory.topology_structure]
    BiPointedTopological.clone [abbrev, in mathcomp.analysis.topology_theory.topology_structure]
    BiPointedTopological.copy [abbrev, in mathcomp.analysis.topology_theory.topology_structure]
    BiPointedTopological.eqtype_hasDecEq_mixin [proj, in mathcomp.analysis.topology_theory.topology_structure]
    BiPointedTopological.Exports [mod, in mathcomp.analysis.topology_theory.topology_structure]
    BiPointedTopological.Exports.bpTopologicalType [abbrev, in mathcomp.analysis.topology_theory.topology_structure]
    BiPointedTopological.Exports.join_topology_structure_BiPointedTopological_between_classical_sets_BiPointed_and_filter_Filtered [def, in mathcomp.analysis.topology_theory.topology_structure]
    BiPointedTopological.Exports.join_topology_structure_BiPointedTopological_between_classical_sets_BiPointed_and_filter_Nbhs [def, in mathcomp.analysis.topology_theory.topology_structure]
    BiPointedTopological.Exports.join_topology_structure_BiPointedTopological_between_classical_sets_BiPointed_and_topology_structure_Topological [def, in mathcomp.analysis.topology_theory.topology_structure]
    BiPointedTopological.filter_isFiltered_mixin [proj, in mathcomp.analysis.topology_theory.topology_structure]
    BiPointedTopological.filter_selfFiltered_mixin [proj, in mathcomp.analysis.topology_theory.topology_structure]
    BiPointedTopological.on [abbrev, in mathcomp.analysis.topology_theory.topology_structure]
    BiPointedTopological.on_ [abbrev, in mathcomp.analysis.topology_theory.topology_structure]
    BiPointedTopological.pack_ [def, in mathcomp.analysis.topology_theory.topology_structure]
    BiPointedTopological.phant_clone [def, in mathcomp.analysis.topology_theory.topology_structure]
    BiPointedTopological.phant_on_ [def, in mathcomp.analysis.topology_theory.topology_structure]
    BiPointedTopological.sort [proj, in mathcomp.analysis.topology_theory.topology_structure]
    BiPointedTopological.topology_structure_Nbhs_isTopological_mixin [proj, in mathcomp.analysis.topology_theory.topology_structure]
    BiPointedTopological.type [rec, in mathcomp.analysis.topology_theory.topology_structure]
    BiPointedTopologicalElpiOperations [mod, in mathcomp.analysis.topology_theory.topology_structure]
    bitseq [def, in mathcomp.boot.seq]
    bitseq_predType [def, in mathcomp.boot.seq]
    BLeft [abbrev, in mathcomp.algebra.interval]
    block_diag_mx_unit [prf, in mathcomp.algebra.matrix]
    block_mx [def, in mathcomp.algebra.matrix]
    block_mx0 [prf, in mathcomp.algebra.matrix]
    block_mx_const [prf, in mathcomp.algebra.matrix]
    block_mx_eq0 [prf, in mathcomp.algebra.matrix]
    block_mxA [prf, in mathcomp.algebra.matrix]
    block_mxAx [def, in mathcomp.algebra.matrix]
    block_mxEdl [prf, in mathcomp.algebra.matrix]
    block_mxEdr [prf, in mathcomp.algebra.matrix]
    block_mxEh [prf, in mathcomp.algebra.matrix]
    block_mxEul [prf, in mathcomp.algebra.matrix]
    block_mxEur [prf, in mathcomp.algebra.matrix]
    block_mxEv [prf, in mathcomp.algebra.matrix]
    block_mxKdl [prf, in mathcomp.algebra.matrix]
    block_mxKdr [prf, in mathcomp.algebra.matrix]
    block_mxKul [prf, in mathcomp.algebra.matrix]
    block_mxKur [prf, in mathcomp.algebra.matrix]
    bnd_simp [def, in mathcomp.algebra.interval]
    bolzano_weierstrass [prf, in mathcomp.analysis.sequences]
    bool_compact [prf, in mathcomp.analysis.topology_theory.bool_topology]
    bool_enumP [prf, in mathcomp.boot.fintype]
    bool_fieldP [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
    bool_irrelevance [prf, in mathcomp.boot.eqtype]
    bool_nbhs_itv [prf, in mathcomp.analysis.topology_theory.bool_topology]
    bool_of_unitK [prf, in mathcomp.boot.choice]
    bool_topology [file, in mathcomp.analysis.topology_theory.bool_topology]
    Boole_inequality [prf, in mathcomp.analysis.measure_theory.measure_function]
    boolp [file, in mathcomp.classical.boolp]
    BoolProp [ind, in mathcomp.classical.boolp]
    boot [file, in mathcomp.boot.boot]
    borel_hierarchy [file, in mathcomp.analysis.borel_hierarchy]
    bottom [prf, in mathcomp.reals.signed]
    bottom [prf, in mathcomp.algebra.interval_inference]
    bound_extremal_groups [prf, in mathcomp.solvable.extremal]
    bound_in_itv [def, in mathcomp.algebra.interval]
    bound_itvE [prf, in mathcomp.analysis.normedtype_theory.num_normedtype]
    bound_join [def, in mathcomp.algebra.interval]
    bound_joinA [prf, in mathcomp.algebra.interval]
    bound_joinC [prf, in mathcomp.algebra.interval]
    bound_joinKI [prf, in mathcomp.algebra.interval]
    bound_le0x [prf, in mathcomp.algebra.interval]
    bound_leEmeet [prf, in mathcomp.algebra.interval]
    bound_lex1 [prf, in mathcomp.algebra.interval]
    bound_lexx [prf, in mathcomp.algebra.interval]
    bound_ltxx [prf, in mathcomp.algebra.interval]
    bound_meet [def, in mathcomp.algebra.interval]
    bound_meetA [prf, in mathcomp.algebra.interval]
    bound_meetC [prf, in mathcomp.algebra.interval]
    bound_meetKU [prf, in mathcomp.algebra.interval]
    bound_side [def, in mathcomp.classical.unstable]
    bounded_beta_pdf_01 [prf, in mathcomp.analysis.probability_theory.beta_distribution]
    bounded_closed_compact [prf, in mathcomp.analysis.normedtype_theory.matrix_normedtype]
    bounded_cst [prf, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
    bounded_fun [abbrev, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
    bounded_fun_has_lbound [prf, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
    bounded_fun_has_lbound_sups [prf, in mathcomp.analysis.sequences]
    bounded_fun_has_ubound [prf, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
    bounded_fun_has_ubound_infs [prf, in mathcomp.analysis.sequences]
    bounded_fun_norm [def, in mathcomp.analysis.sequences]
    bounded_funD [prf, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
    bounded_funN [prf, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
    bounded_funP [prf, in mathcomp.analysis.normedtype_theory.normed_module]
    bounded_indic [prf, in mathcomp.analysis.numfun]
    bounded_landau [prf, in mathcomp.analysis.sequences]
    bounded_linear_continuous [prf, in mathcomp.analysis.normedtype_theory.normed_module]
    bounded_locally [prf, in mathcomp.analysis.normedtype_theory.normed_module]
    bounded_near [def, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
    bounded_set [abbrev, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
    bounded_variation [def, in mathcomp.analysis.numfun]
    bounded_variation_pos_neg_tvE [prf, in mathcomp.analysis.realfun]
    bounded_variationD [prf, in mathcomp.analysis.numfun]
    bounded_variationl [prf, in mathcomp.analysis.numfun]
    bounded_variationN [prf, in mathcomp.analysis.numfun]
    bounded_variationP [prf, in mathcomp.analysis.realfun]
    bounded_variationr [prf, in mathcomp.analysis.numfun]
    bounded_variationxx [prf, in mathcomp.analysis.numfun]
    bounded_XMonemX [prf, in mathcomp.analysis.probability_theory.beta_distribution]
    boundedE [prf, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
    boundl_in_itv [prf, in mathcomp.algebra.interval]
    boundr_in_itv [prf, in mathcomp.algebra.interval]
    Box [constr, in mathcomp.classical.unstable]
    boxed [ind, in mathcomp.classical.unstable]
    boxed_ind [scheme, in mathcomp.classical.unstable]
    boxed_rec [scheme, in mathcomp.classical.unstable]
    boxed_rect [scheme, in mathcomp.classical.unstable]
    boxed_sind [scheme, in mathcomp.classical.unstable]
    bpwedge [abbrev, in mathcomp.analysis.homotopy_theory.wedge_sigT]
    bpwedge [abbrev, in mathcomp.analysis.homotopy_theory.wedge_sigT]
    bpwedge_lift [abbrev, in mathcomp.analysis.homotopy_theory.wedge_sigT]
    bpwedge_lift [abbrev, in mathcomp.analysis.homotopy_theory.wedge_sigT]
    bpwedge_shared_pt [def, in mathcomp.analysis.homotopy_theory.wedge_sigT]
    bpwedgeE [prf, in mathcomp.analysis.homotopy_theory.wedge_sigT]
    branch_apx [def, in mathcomp.analysis.cantor]
    BRight [abbrev, in mathcomp.algebra.interval]
    BRight_le_map_itv_bound_EFin [prf, in mathcomp.reals.constructive_ereal]
    BRight_le_num_itv_bound [prf, in mathcomp.algebra.interval_inference]
    bsCA [abbrev, in mathcomp.boot.seq]
    bseq [def, in mathcomp.boot.tuple]
    bseq0 [prf, in mathcomp.boot.tuple]
    bseq_hasChoice [def, in mathcomp.boot.tuple]
    bseq_hasDecEq [def, in mathcomp.boot.tuple]
    bseq_isCountable [def, in mathcomp.boot.tuple]
    bseq_of [rec, in mathcomp.boot.tuple]
    bseq_of_tuple [def, in mathcomp.boot.tuple]
    bseq_predType [def, in mathcomp.boot.tuple]
    bseq_tagged_tuple [def, in mathcomp.boot.tuple]
    bseq_tagged_tuple_bij [prf, in mathcomp.boot.tuple]
    bseq_tagged_tupleK [prf, in mathcomp.boot.tuple]
    bseqE [prf, in mathcomp.boot.tuple]
    bseqval [proj, in mathcomp.boot.tuple]
    BSide [constr, in mathcomp.algebra.interval]
    BSide_max [prf, in mathcomp.algebra.interval]
    BSide_min [prf, in mathcomp.algebra.interval]
    Build_ProperFilter_ex [def, in mathcomp.classical.filter]
    Builders_1 [mod, in mathcomp.finite_group.fingroup]
    Builders_1 [mod, in mathcomp.field.falgebra]
    Builders_1 [mod, in mathcomp.field.closed_field]
    Builders_1 [mod, in mathcomp.field.algC]
    Builders_1 [mod, in mathcomp.classical.functions]
    Builders_1 [mod, in mathcomp.boot.monoid]
    Builders_1 [mod, in mathcomp.analysis.topology_theory.uniform_structure]
    Builders_1 [mod, in mathcomp.analysis.topology_theory.topology_structure]
    Builders_1 [mod, in mathcomp.analysis.topology_theory.pseudometric_structure]
    Builders_1 [mod, in mathcomp.analysis.topology_theory.metric_structure]
    Builders_1 [mod, in mathcomp.analysis.topology_theory.discrete_topology]
    Builders_1 [mod, in mathcomp.analysis.normedtype_theory.tvs]
    Builders_1 [mod, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
    Builders_1 [mod, in mathcomp.analysis.normedtype_theory.normed_module]
    Builders_1 [mod, in mathcomp.analysis.measure_theory.probability_measure]
    Builders_1 [mod, in mathcomp.analysis.measure_theory.measure_function]
    Builders_1 [mod, in mathcomp.analysis.measure_theory.measure_extension]
    Builders_1 [mod, in mathcomp.analysis.measure_theory.measurable_structure]
    Builders_1 [mod, in mathcomp.analysis.charge]
    Builders_1 [mod, in mathcomp.algebra.vector]
    Builders_1.add_continuous [prf, in mathcomp.analysis.normedtype_theory.tvs]
    Builders_1.ball [abbrev, in mathcomp.analysis.topology_theory.pseudometric_structure]
    Builders_1.ball_center [abbrev, in mathcomp.analysis.topology_theory.pseudometric_structure]
    Builders_1.ball_sym [abbrev, in mathcomp.analysis.topology_theory.pseudometric_structure]
    Builders_1.ball_triangle [abbrev, in mathcomp.analysis.topology_theory.pseudometric_structure]
    Builders_1.bigcupT_measurable [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
    Builders_1.Builders_Export_10 [mod, in mathcomp.algebra.vector]
    Builders_1.Builders_Export_12 [mod, in mathcomp.finite_group.fingroup]
    Builders_1.Builders_Export_12 [mod, in mathcomp.analysis.topology_theory.metric_structure]
    Builders_1.Builders_Export_12 [mod, in mathcomp.analysis.normedtype_theory.normed_module]
    Builders_1.Builders_Export_13 [mod, in mathcomp.field.algC]
    Builders_1.Builders_Export_5 [mod, in mathcomp.field.falgebra]
    Builders_1.Builders_Export_5 [mod, in mathcomp.analysis.topology_theory.topology_structure]
    Builders_1.Builders_Export_5 [mod, in mathcomp.analysis.topology_theory.discrete_topology]
    Builders_1.Builders_Export_5 [mod, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
    Builders_1.Builders_Export_5 [mod, in mathcomp.analysis.measure_theory.measure_extension]
    Builders_1.Builders_Export_5 [mod, in mathcomp.analysis.measure_theory.measurable_structure]
    Builders_1.Builders_Export_7 [mod, in mathcomp.field.closed_field]
    Builders_1.Builders_Export_7 [mod, in mathcomp.classical.functions]
    Builders_1.Builders_Export_7 [mod, in mathcomp.boot.monoid]
    Builders_1.Builders_Export_7 [mod, in mathcomp.analysis.topology_theory.uniform_structure]
    Builders_1.Builders_Export_7 [mod, in mathcomp.analysis.normedtype_theory.tvs]
    Builders_1.Builders_Export_7 [mod, in mathcomp.analysis.measure_theory.measure_function]
    Builders_1.Builders_Export_8 [mod, in mathcomp.analysis.topology_theory.pseudometric_structure]
    Builders_1.Builders_Export_9 [mod, in mathcomp.analysis.measure_theory.probability_measure]
    Builders_1.Builders_Export_9 [mod, in mathcomp.analysis.charge]
    Builders_1.charge0 [abbrev, in mathcomp.analysis.charge]
    Builders_1.charge_finite [abbrev, in mathcomp.analysis.charge]
    Builders_1.charge_sigma_additive [abbrev, in mathcomp.analysis.charge]
    Builders_1.conj [abbrev, in mathcomp.field.algC]
    Builders_1.conj_nt [abbrev, in mathcomp.field.algC]
    Builders_1.conjK [abbrev, in mathcomp.field.algC]
    Builders_1.dim [abbrev, in mathcomp.algebra.vector]
    Builders_1.dim_gt0 [prf, in mathcomp.field.falgebra]
    Builders_1.ent [abbrev, in mathcomp.analysis.topology_theory.pseudometric_structure]
    Builders_1.entourage [abbrev, in mathcomp.analysis.topology_theory.uniform_structure]
    Builders_1.entourage_diagonal [abbrev, in mathcomp.analysis.topology_theory.uniform_structure]
    Builders_1.entourage_filter [abbrev, in mathcomp.analysis.topology_theory.uniform_structure]
    Builders_1.entourage_inv [abbrev, in mathcomp.analysis.topology_theory.uniform_structure]
    Builders_1.entourage_split_ex [abbrev, in mathcomp.analysis.topology_theory.uniform_structure]
    Builders_1.entourageE [abbrev, in mathcomp.analysis.topology_theory.pseudometric_structure]
    Builders_1.i [def, in mathcomp.field.algC]
    Builders_1.iJ [prf, in mathcomp.field.algC]
    Builders_1.inv [abbrev, in mathcomp.finite_group.fingroup]
    Builders_1.inv [abbrev, in mathcomp.classical.functions]
    Builders_1.invgK [prf, in mathcomp.finite_group.fingroup]
    Builders_1.invMg [prf, in mathcomp.finite_group.fingroup]
    Builders_1.le [def, in mathcomp.field.algC]
    Builders_1.le_outer_measure [prf, in mathcomp.analysis.measure_theory.measure_extension]
    Builders_1.leB [prf, in mathcomp.field.algC]
    Builders_1.lt [def, in mathcomp.field.algC]
    Builders_1.mdist [abbrev, in mathcomp.analysis.topology_theory.metric_structure]
    Builders_1.mdist_norm [abbrev, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
    Builders_1.mdist_positivity [abbrev, in mathcomp.analysis.topology_theory.metric_structure]
    Builders_1.mdist_sym [abbrev, in mathcomp.analysis.topology_theory.metric_structure]
    Builders_1.mdist_triangle [abbrev, in mathcomp.analysis.topology_theory.metric_structure]
    Builders_1.mdistxx [abbrev, in mathcomp.analysis.topology_theory.metric_structure]
    Builders_1.measure0 [abbrev, in mathcomp.analysis.measure_theory.measure_function]
    Builders_1.measure_ge0 [abbrev, in mathcomp.analysis.measure_theory.measure_function]
    Builders_1.measure_semi_sigma_additive [abbrev, in mathcomp.analysis.measure_theory.measure_function]
    Builders_1.mul [abbrev, in mathcomp.finite_group.fingroup]
    Builders_1.mul [abbrev, in mathcomp.boot.monoid]
    Builders_1.mul1g [abbrev, in mathcomp.finite_group.fingroup]
    Builders_1.mul2I [prf, in mathcomp.field.algC]
    Builders_1.mulgA [abbrev, in mathcomp.finite_group.fingroup]
    Builders_1.mulgA [abbrev, in mathcomp.boot.monoid]
    Builders_1.mulVg [abbrev, in mathcomp.finite_group.fingroup]
    Builders_1.nbhs_filter [abbrev, in mathcomp.analysis.topology_theory.topology_structure]
    Builders_1.nbhs_nbhs [abbrev, in mathcomp.analysis.topology_theory.topology_structure]
    Builders_1.nbhs_principalE [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
    Builders_1.nbhs_singleton [abbrev, in mathcomp.analysis.topology_theory.topology_structure]
    Builders_1.nbhsE [abbrev, in mathcomp.analysis.topology_theory.uniform_structure]
    Builders_1.nbhsE [abbrev, in mathcomp.analysis.topology_theory.pseudometric_structure]
    Builders_1.norm [def, in mathcomp.field.algC]
    Builders_1.norm_eq0 [prf, in mathcomp.field.algC]
    Builders_1.normD [prf, in mathcomp.field.algC]
    Builders_1.normE [prf, in mathcomp.field.algC]
    Builders_1.normK [prf, in mathcomp.field.algC]
    Builders_1.normM [prf, in mathcomp.field.algC]
    Builders_1.normN [prf, in mathcomp.field.algC]
    Builders_1.normrZ [abbrev, in mathcomp.analysis.normedtype_theory.normed_module]
    Builders_1.nz2 [prf, in mathcomp.field.algC]
    Builders_1.one [abbrev, in mathcomp.finite_group.fingroup]
    Builders_1.open_of_nbhs [def, in mathcomp.analysis.topology_theory.topology_structure]
    Builders_1.opp_continuous [prf, in mathcomp.analysis.normedtype_theory.tvs]
    Builders_1.outer_measure0 [abbrev, in mathcomp.analysis.measure_theory.measure_extension]
    Builders_1.outer_measure_ge0 [abbrev, in mathcomp.analysis.measure_theory.measure_extension]
    Builders_1.outer_measure_sigma_subadditive [prf, in mathcomp.analysis.measure_theory.measure_extension]
    Builders_1.pos_linear [prf, in mathcomp.field.algC]
    Builders_1.posE [prf, in mathcomp.field.algC]
    Builders_1.posJ [prf, in mathcomp.field.algC]
    Builders_1.posP [prf, in mathcomp.field.algC]
    Builders_1.principal_nbhs_filter [prf, in mathcomp.analysis.topology_theory.discrete_topology]
    Builders_1.principal_nbhs_nbhs [prf, in mathcomp.analysis.topology_theory.discrete_topology]
    Builders_1.principal_nbhs_singleton [prf, in mathcomp.analysis.topology_theory.discrete_topology]
    Builders_1.solve_monicpoly [abbrev, in mathcomp.field.closed_field]
    Builders_1.sposD [prf, in mathcomp.field.algC]
    Builders_1.sposDl [prf, in mathcomp.field.algC]
    Builders_1.sprobability_setT [abbrev, in mathcomp.analysis.measure_theory.probability_measure]
    Builders_1.sqrMi [prf, in mathcomp.field.algC]
    Builders_1.sqrt [def, in mathcomp.field.algC]
    Builders_1.sqrtE [prf, in mathcomp.field.algC]
    Builders_1.sqrtK [prf, in mathcomp.field.algC]
    Builders_1.sub_continuous [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
    Builders_1.subset_outer_measure_sigma_subadditive [abbrev, in mathcomp.analysis.measure_theory.measure_extension]
    Builders_1.Super [mod, in mathcomp.finite_group.fingroup]
    Builders_1.Super [mod, in mathcomp.field.falgebra]
    Builders_1.Super [mod, in mathcomp.field.closed_field]
    Builders_1.Super [mod, in mathcomp.field.algC]
    Builders_1.Super [mod, in mathcomp.classical.functions]
    Builders_1.Super [mod, in mathcomp.boot.monoid]
    Builders_1.Super [mod, in mathcomp.analysis.topology_theory.uniform_structure]
    Builders_1.Super [mod, in mathcomp.analysis.topology_theory.topology_structure]
    Builders_1.Super [mod, in mathcomp.analysis.topology_theory.pseudometric_structure]
    Builders_1.Super [mod, in mathcomp.analysis.topology_theory.metric_structure]
    Builders_1.Super [mod, in mathcomp.analysis.topology_theory.discrete_topology]
    Builders_1.Super [mod, in mathcomp.analysis.normedtype_theory.tvs]
    Builders_1.Super [mod, in mathcomp.analysis.normedtype_theory.pseudometric_normed_Zmodule]
    Builders_1.Super [mod, in mathcomp.analysis.normedtype_theory.normed_module]
    Builders_1.Super [mod, in mathcomp.analysis.measure_theory.probability_measure]
    Builders_1.Super [mod, in mathcomp.analysis.measure_theory.measure_function]
    Builders_1.Super [mod, in mathcomp.analysis.measure_theory.measure_extension]
    Builders_1.Super [mod, in mathcomp.analysis.measure_theory.measurable_structure]
    Builders_1.Super [mod, in mathcomp.analysis.charge]
    Builders_1.Super [mod, in mathcomp.algebra.vector]
    Builders_1.v2r [def, in mathcomp.algebra.vector]
    Builders_1.vector_subdef [abbrev, in mathcomp.algebra.vector]
    Builders_10 [mod, in mathcomp.boot.monoid]
    Builders_10.Builders_Export_16 [mod, in mathcomp.boot.monoid]
    Builders_10.mul1g [abbrev, in mathcomp.boot.monoid]
    Builders_10.mulg1 [abbrev, in mathcomp.boot.monoid]
    Builders_10.one [abbrev, in mathcomp.boot.monoid]
    Builders_10.Super [mod, in mathcomp.boot.monoid]
    Builders_108 [mod, in mathcomp.analysis.measure_theory.measure_function]
    Builders_108.Builders_Export_112 [mod, in mathcomp.analysis.measure_theory.measure_function]
    Builders_108.s_finite [abbrev, in mathcomp.analysis.measure_theory.measure_function]
    Builders_108.Super [mod, in mathcomp.analysis.measure_theory.measure_function]
    Builders_109 [mod, in mathcomp.boot.monoid]
    Builders_109.Builders_Export_117 [mod, in mathcomp.boot.monoid]
    Builders_109.Super [mod, in mathcomp.boot.monoid]
    Builders_109.valM [prf, in mathcomp.boot.monoid]
    Builders_118 [mod, in mathcomp.boot.monoid]
    Builders_118.Builders_Export_125 [mod, in mathcomp.boot.monoid]
    Builders_118.mulgA [prf, in mathcomp.boot.monoid]
    Builders_118.Super [mod, in mathcomp.boot.monoid]
    Builders_128 [mod, in mathcomp.boot.monoid]
    Builders_128.Builders_Export_139 [mod, in mathcomp.boot.monoid]
    Builders_128.mul1g [prf, in mathcomp.boot.monoid]
    Builders_128.mulg1 [prf, in mathcomp.boot.monoid]
    Builders_128.Super [mod, in mathcomp.boot.monoid]
    Builders_128.val1 [prf, in mathcomp.boot.monoid]
    Builders_13 [mod, in mathcomp.field.galois]
    Builders_13 [mod, in mathcomp.analysis.topology_theory.discrete_topology]
    Builders_13.Builders_Export_17 [mod, in mathcomp.field.galois]
    Builders_13.Builders_Export_19 [mod, in mathcomp.analysis.topology_theory.discrete_topology]
    Builders_13.discrete_ball_center [prf, in mathcomp.analysis.topology_theory.discrete_topology]
    Builders_13.discrete_ball_sym [prf, in mathcomp.analysis.topology_theory.discrete_topology]
    Builders_13.discrete_ball_triangle [prf, in mathcomp.analysis.topology_theory.discrete_topology]
    Builders_13.discrete_ballE [prf, in mathcomp.analysis.topology_theory.discrete_topology]
    Builders_13.discrete_entourageE [prf, in mathcomp.analysis.topology_theory.discrete_topology]
    Builders_13.normal_field_splitting_axiom [abbrev, in mathcomp.field.galois]
    Builders_13.Super [mod, in mathcomp.field.galois]
    Builders_13.Super [mod, in mathcomp.analysis.topology_theory.discrete_topology]
    Builders_14 [mod, in mathcomp.analysis.topology_theory.topology_structure]
    Builders_14 [mod, in mathcomp.analysis.measure_theory.measurable_structure]
    Builders_14.b [abbrev, in mathcomp.analysis.topology_theory.topology_structure]
    Builders_14.b_cover [abbrev, in mathcomp.analysis.topology_theory.topology_structure]
    Builders_14.b_join [abbrev, in mathcomp.analysis.topology_theory.topology_structure]
    Builders_14.Builders_Export_20 [mod, in mathcomp.analysis.topology_theory.topology_structure]
    Builders_14.Builders_Export_20 [mod, in mathcomp.analysis.measure_theory.measurable_structure]
    Builders_14.D [abbrev, in mathcomp.analysis.topology_theory.topology_structure]
    Builders_14.I [abbrev, in mathcomp.analysis.topology_theory.topology_structure]
    Builders_14.mD [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    Builders_14.measurable [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
    Builders_14.measurable0 [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
    Builders_14.measurableD [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
    Builders_14.measurableU [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
    Builders_14.mI [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    Builders_14.open_from [def, in mathcomp.analysis.topology_theory.topology_structure]
    Builders_14.Super [mod, in mathcomp.analysis.topology_theory.topology_structure]
    Builders_14.Super [mod, in mathcomp.analysis.measure_theory.measurable_structure]
    Builders_140 [mod, in mathcomp.boot.monoid]
    Builders_140.Builders_Export_150 [mod, in mathcomp.boot.monoid]
    Builders_140.Super [mod, in mathcomp.boot.monoid]
    Builders_15 [mod, in mathcomp.classical.functions]
    Builders_15 [mod, in mathcomp.analysis.normedtype_theory.tvs]
    Builders_15.add_unif_continuous [prf, in mathcomp.analysis.normedtype_theory.tvs]
    Builders_15.Builders_Export_19 [mod, in mathcomp.classical.functions]
    Builders_15.Builders_Export_21 [mod, in mathcomp.analysis.normedtype_theory.tvs]
    Builders_15.funK [abbrev, in mathcomp.classical.functions]
    Builders_15.funoK [prf, in mathcomp.classical.functions]
    Builders_15.opp_unif_continuous [prf, in mathcomp.analysis.normedtype_theory.tvs]
    Builders_15.sub_unif_continuous [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
    Builders_15.Super [mod, in mathcomp.classical.functions]
    Builders_15.Super [mod, in mathcomp.analysis.normedtype_theory.tvs]
    Builders_151 [mod, in mathcomp.boot.monoid]
    Builders_151.Builders_Export_167 [mod, in mathcomp.boot.monoid]
    Builders_151.mulgV [prf, in mathcomp.boot.monoid]
    Builders_151.mulVg [prf, in mathcomp.boot.monoid]
    Builders_151.Super [mod, in mathcomp.boot.monoid]
    Builders_151.umagma_closed [prf, in mathcomp.boot.monoid]
    Builders_17 [mod, in mathcomp.boot.monoid]
    Builders_17.Builders_Export_22 [mod, in mathcomp.boot.monoid]
    Builders_17.mul1g [abbrev, in mathcomp.boot.monoid]
    Builders_17.mulg1 [abbrev, in mathcomp.boot.monoid]
    Builders_17.one [abbrev, in mathcomp.boot.monoid]
    Builders_17.Super [mod, in mathcomp.boot.monoid]
    Builders_19 [mod, in mathcomp.classical.filter]
    Builders_19.Builders_Export_25 [mod, in mathcomp.classical.filter]
    Builders_19.nbhs [abbrev, in mathcomp.classical.filter]
    Builders_19.Super [mod, in mathcomp.classical.filter]
    Builders_20 [mod, in mathcomp.classical.functions]
    Builders_20.Builders_Export_24 [mod, in mathcomp.classical.functions]
    Builders_20.invK [abbrev, in mathcomp.classical.functions]
    Builders_20.invS [abbrev, in mathcomp.classical.functions]
    Builders_20.oinvK [prf, in mathcomp.classical.functions]
    Builders_20.oinvS [prf, in mathcomp.classical.functions]
    Builders_20.Super [mod, in mathcomp.classical.functions]
    Builders_21 [mod, in mathcomp.analysis.topology_theory.topology_structure]
    Builders_21 [mod, in mathcomp.analysis.measure_theory.measurable_structure]
    Builders_21.b [abbrev, in mathcomp.analysis.topology_theory.topology_structure]
    Builders_21.Builders_Export_26 [mod, in mathcomp.analysis.measure_theory.measurable_structure]
    Builders_21.Builders_Export_27 [mod, in mathcomp.analysis.topology_theory.topology_structure]
    Builders_21.D [abbrev, in mathcomp.analysis.topology_theory.topology_structure]
    Builders_21.finI_from [abbrev, in mathcomp.analysis.topology_theory.topology_structure]
    Builders_21.I [abbrev, in mathcomp.analysis.topology_theory.topology_structure]
    Builders_21.measurable [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
    Builders_21.measurable_nonempty [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
    Builders_21.measurable_setI [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
    Builders_21.measurable_setY [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
    Builders_21.Super [mod, in mathcomp.analysis.topology_theory.topology_structure]
    Builders_21.Super [mod, in mathcomp.analysis.measure_theory.measurable_structure]
    Builders_22 [mod, in mathcomp.analysis.normedtype_theory.tvs]
    Builders_22.Builders_Export_28 [mod, in mathcomp.analysis.normedtype_theory.tvs]
    Builders_22.opp_unif_continuous [prf, in mathcomp.analysis.normedtype_theory.tvs]
    Builders_22.scale_unif_continuous [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
    Builders_22.Super [mod, in mathcomp.analysis.normedtype_theory.tvs]
    Builders_23 [mod, in mathcomp.boot.monoid]
    Builders_23 [mod, in mathcomp.analysis.measure_theory.probability_measure]
    Builders_23.Builders_Export_27 [mod, in mathcomp.boot.monoid]
    Builders_23.Builders_Export_32 [mod, in mathcomp.analysis.measure_theory.probability_measure]
    Builders_23.mulgA [abbrev, in mathcomp.boot.monoid]
    Builders_23.probability_setT [abbrev, in mathcomp.analysis.measure_theory.probability_measure]
    Builders_23.Super [mod, in mathcomp.boot.monoid]
    Builders_23.Super [mod, in mathcomp.analysis.measure_theory.probability_measure]
    Builders_26 [mod, in mathcomp.boot.fintype]
    Builders_26.Builders_Export_28 [mod, in mathcomp.boot.fintype]
    Builders_26.mem_sub_enum [prf, in mathcomp.boot.fintype]
    Builders_26.sub_enum [def, in mathcomp.boot.fintype]
    Builders_26.sub_enum_uniq [prf, in mathcomp.boot.fintype]
    Builders_26.SubFinMixin [def, in mathcomp.boot.fintype]
    Builders_26.Super [mod, in mathcomp.boot.fintype]
    Builders_26.val_sub_enum [prf, in mathcomp.boot.fintype]
    Builders_27 [mod, in mathcomp.analysis.measure_theory.measurable_structure]
    Builders_27.Builders_Export_33 [mod, in mathcomp.analysis.measure_theory.measurable_structure]
    Builders_27.mD [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    Builders_27.measurable [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
    Builders_27.measurable0 [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
    Builders_27.measurableC [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
    Builders_27.measurableT [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    Builders_27.measurableU [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
    Builders_27.Super [mod, in mathcomp.analysis.measure_theory.measurable_structure]
    Builders_27.T_isRingOfSets [def, in mathcomp.analysis.measure_theory.measurable_structure]
    Builders_28 [mod, in mathcomp.boot.monoid]
    Builders_28.Builders_Export_37 [mod, in mathcomp.boot.monoid]
    Builders_28.mul [abbrev, in mathcomp.boot.monoid]
    Builders_28.mul1g [abbrev, in mathcomp.boot.monoid]
    Builders_28.mulg1 [abbrev, in mathcomp.boot.monoid]
    Builders_28.mulgA [abbrev, in mathcomp.boot.monoid]
    Builders_28.one [abbrev, in mathcomp.boot.monoid]
    Builders_28.Super [mod, in mathcomp.boot.monoid]
    Builders_29 [mod, in mathcomp.analysis.normedtype_theory.tvs]
    Builders_29.add_continuous [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
    Builders_29.Builders_Export_33 [mod, in mathcomp.analysis.normedtype_theory.tvs]
    Builders_29.entourage [def, in mathcomp.analysis.normedtype_theory.tvs]
    Builders_29.entourage_filter [prf, in mathcomp.analysis.normedtype_theory.tvs]
    Builders_29.entourage_inv [prf, in mathcomp.analysis.normedtype_theory.tvs]
    Builders_29.entourage_refl [prf, in mathcomp.analysis.normedtype_theory.tvs]
    Builders_29.entourage_split_ex [prf, in mathcomp.analysis.normedtype_theory.tvs]
    Builders_29.locally_convex [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
    Builders_29.nbhsE [prf, in mathcomp.analysis.normedtype_theory.tvs]
    Builders_29.nbhsN [prf, in mathcomp.analysis.normedtype_theory.tvs]
    Builders_29.scale_continuous [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
    Builders_29.Super [mod, in mathcomp.analysis.normedtype_theory.tvs]
    Builders_30 [mod, in mathcomp.analysis.numfun]
    Builders_30.Builders_Export_34 [mod, in mathcomp.analysis.numfun]
    Builders_30.fimfunE [abbrev, in mathcomp.analysis.numfun]
    Builders_30.Super [mod, in mathcomp.analysis.numfun]
    Builders_336 [mod, in mathcomp.classical.functions]
    Builders_336.Builders_Export_343 [mod, in mathcomp.classical.functions]
    Builders_336.inv [abbrev, in mathcomp.classical.functions]
    Builders_336.invK [abbrev, in mathcomp.classical.functions]
    Builders_336.invS [abbrev, in mathcomp.classical.functions]
    Builders_336.Super [mod, in mathcomp.classical.functions]
    Builders_34 [mod, in mathcomp.analysis.measure_theory.measurable_structure]
    Builders_34.Builders_Export_41 [mod, in mathcomp.analysis.measure_theory.measurable_structure]
    Builders_34.measurable [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
    Builders_34.measurableD [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
    Builders_34.measurableT [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
    Builders_34.Super [mod, in mathcomp.analysis.measure_theory.measurable_structure]
    Builders_344 [mod, in mathcomp.classical.functions]
    Builders_344.Builders_Export_352 [mod, in mathcomp.classical.functions]
    Builders_344.funoK [abbrev, in mathcomp.classical.functions]
    Builders_344.funS [abbrev, in mathcomp.classical.functions]
    Builders_344.oinvK [abbrev, in mathcomp.classical.functions]
    Builders_344.oinvS [abbrev, in mathcomp.classical.functions]
    Builders_344.Super [mod, in mathcomp.classical.functions]
    Builders_353 [mod, in mathcomp.classical.functions]
    Builders_353.Builders_Export_361 [mod, in mathcomp.classical.functions]
    Builders_353.funoK [abbrev, in mathcomp.classical.functions]
    Builders_353.funS [abbrev, in mathcomp.classical.functions]
    Builders_353.oinv [abbrev, in mathcomp.classical.functions]
    Builders_353.oinvK [abbrev, in mathcomp.classical.functions]
    Builders_353.oinvS [abbrev, in mathcomp.classical.functions]
    Builders_353.Super [mod, in mathcomp.classical.functions]
    Builders_362 [mod, in mathcomp.classical.functions]
    Builders_362.Builders_Export_369 [mod, in mathcomp.classical.functions]
    Builders_362.funK [abbrev, in mathcomp.classical.functions]
    Builders_362.inv [abbrev, in mathcomp.classical.functions]
    Builders_362.Super [mod, in mathcomp.classical.functions]
    Builders_370 [mod, in mathcomp.classical.functions]
    Builders_370.Builders_Export_378 [mod, in mathcomp.classical.functions]
    Builders_370.funK [abbrev, in mathcomp.classical.functions]
    Builders_370.funS [abbrev, in mathcomp.classical.functions]
    Builders_370.invK [abbrev, in mathcomp.classical.functions]
    Builders_370.invS [abbrev, in mathcomp.classical.functions]
    Builders_370.Super [mod, in mathcomp.classical.functions]
    Builders_379 [mod, in mathcomp.classical.functions]
    Builders_379.Builders_Export_388 [mod, in mathcomp.classical.functions]
    Builders_379.funK [abbrev, in mathcomp.classical.functions]
    Builders_379.funS [abbrev, in mathcomp.classical.functions]
    Builders_379.inv [abbrev, in mathcomp.classical.functions]
    Builders_379.invK [abbrev, in mathcomp.classical.functions]
    Builders_379.invS [abbrev, in mathcomp.classical.functions]
    Builders_379.Super [mod, in mathcomp.classical.functions]
    Builders_389 [mod, in mathcomp.classical.functions]
    Builders_389.Builders_Export_393 [mod, in mathcomp.classical.functions]
    Builders_389.injV [abbrev, in mathcomp.classical.functions]
    Builders_389.invK [prf, in mathcomp.classical.functions]
    Builders_389.invS [abbrev, in mathcomp.classical.functions]
    Builders_389.Super [mod, in mathcomp.classical.functions]
    Builders_394 [mod, in mathcomp.classical.functions]
    Builders_394.bij [abbrev, in mathcomp.classical.functions]
    Builders_394.Builders_Export_402 [mod, in mathcomp.classical.functions]
    Builders_394.exg [prf, in mathcomp.classical.functions]
    Builders_394.Super [mod, in mathcomp.classical.functions]
    Builders_41 [mod, in mathcomp.boot.monoid]
    Builders_41.Builders_Export_52 [mod, in mathcomp.boot.monoid]
    Builders_41.inv [abbrev, in mathcomp.boot.monoid]
    Builders_41.invg1 [prf, in mathcomp.boot.monoid]
    Builders_41.invgK [abbrev, in mathcomp.boot.monoid]
    Builders_41.invgM [abbrev, in mathcomp.boot.monoid]
    Builders_41.mul [abbrev, in mathcomp.boot.monoid]
    Builders_41.mul1g [abbrev, in mathcomp.boot.monoid]
    Builders_41.mulg1 [prf, in mathcomp.boot.monoid]
    Builders_41.mulgA [abbrev, in mathcomp.boot.monoid]
    Builders_41.one [abbrev, in mathcomp.boot.monoid]
    Builders_41.Super [mod, in mathcomp.boot.monoid]
    Builders_42 [mod, in mathcomp.analysis.measure_theory.measurable_structure]
    Builders_42.Builders_Export_50 [mod, in mathcomp.analysis.measure_theory.measurable_structure]
    Builders_42.mC [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    Builders_42.measurable [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
    Builders_42.measurable0 [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
    Builders_42.measurable_bigcup [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
    Builders_42.measurableC [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
    Builders_42.mU [prf, in mathcomp.analysis.measure_theory.measurable_structure]
    Builders_42.Super [mod, in mathcomp.analysis.measure_theory.measurable_structure]
    Builders_43 [mod, in mathcomp.analysis.kernel]
    Builders_43.Builders_Export_47 [mod, in mathcomp.analysis.kernel]
    Builders_43.sfinite [abbrev, in mathcomp.analysis.kernel]
    Builders_43.sfinite_subdef [prf, in mathcomp.analysis.kernel]
    Builders_43.Super [mod, in mathcomp.analysis.kernel]
    Builders_461 [mod, in mathcomp.classical.functions]
    Builders_461.Builders_Export_467 [mod, in mathcomp.classical.functions]
    Builders_461.funoK [prf, in mathcomp.classical.functions]
    Builders_461.inj [abbrev, in mathcomp.classical.functions]
    Builders_461.Super [mod, in mathcomp.classical.functions]
    Builders_468 [mod, in mathcomp.classical.functions]
    Builders_468.Builders_Export_477 [mod, in mathcomp.classical.functions]
    Builders_468.inj [abbrev, in mathcomp.classical.functions]
    Builders_468.Super [mod, in mathcomp.classical.functions]
    Builders_478 [mod, in mathcomp.classical.functions]
    Builders_478.Builders_Export_482 [mod, in mathcomp.classical.functions]
    Builders_478.funK [prf, in mathcomp.classical.functions]
    Builders_478.inj [abbrev, in mathcomp.classical.functions]
    Builders_478.Super [mod, in mathcomp.classical.functions]
    Builders_5 [mod, in mathcomp.analysis.kernel]
    Builders_5 [mod, in mathcomp.algebra.sesquilinear]
    Builders_5.Builders_Export_15 [mod, in mathcomp.analysis.kernel]
    Builders_5.Builders_Export_9 [mod, in mathcomp.algebra.sesquilinear]
    Builders_5.measure_uub [abbrev, in mathcomp.analysis.kernel]
    Builders_5.Super [mod, in mathcomp.analysis.kernel]
    Builders_5.Super [mod, in mathcomp.algebra.sesquilinear]
    Builders_50 [mod, in mathcomp.analysis.kernel]
    Builders_50.Builders_Export_59 [mod, in mathcomp.analysis.kernel]
    Builders_50.sprob_kernel [abbrev, in mathcomp.analysis.kernel]
    Builders_50.Super [mod, in mathcomp.analysis.kernel]
    Builders_53 [mod, in mathcomp.boot.monoid]
    Builders_53.Builders_Export_59 [mod, in mathcomp.boot.monoid]
    Builders_53.invgK [prf, in mathcomp.boot.monoid]
    Builders_53.invgM [prf, in mathcomp.boot.monoid]
    Builders_53.mulgV [abbrev, in mathcomp.boot.monoid]
    Builders_53.mulKg [prf, in mathcomp.boot.monoid]
    Builders_53.mulVg [abbrev, in mathcomp.boot.monoid]
    Builders_53.Super [mod, in mathcomp.boot.monoid]
    Builders_55 [mod, in mathcomp.analysis.measure_theory.measure_function]
    Builders_55.Builders_Export_59 [mod, in mathcomp.analysis.measure_theory.measure_function]
    Builders_55.measure_sigma_subadditive [abbrev, in mathcomp.analysis.measure_theory.measure_function]
    Builders_55.Super [mod, in mathcomp.analysis.measure_theory.measure_function]
    Builders_6 [mod, in mathcomp.field.falgebra]
    Builders_6 [mod, in mathcomp.analysis.topology_theory.topology_structure]
    Builders_6 [mod, in mathcomp.analysis.topology_theory.discrete_topology]
    Builders_6 [mod, in mathcomp.analysis.measure_theory.measurable_structure]
    Builders_6 [mod, in mathcomp.algebra.ring_quotient]
    Builders_6.amE [prf, in mathcomp.field.falgebra]
    Builders_6.bigcupT_measurable [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
    Builders_6.Builders_Export_12 [mod, in mathcomp.field.falgebra]
    Builders_6.Builders_Export_12 [mod, in mathcomp.analysis.topology_theory.discrete_topology]
    Builders_6.Builders_Export_13 [mod, in mathcomp.analysis.topology_theory.topology_structure]
    Builders_6.Builders_Export_13 [mod, in mathcomp.analysis.measure_theory.measurable_structure]
    Builders_6.Builders_Export_13 [mod, in mathcomp.algebra.ring_quotient]
    Builders_6.d [abbrev, in mathcomp.analysis.topology_theory.discrete_topology]
    Builders_6.discrete_entourage_diagonal [prf, in mathcomp.analysis.topology_theory.discrete_topology]
    Builders_6.discrete_entourage_filter [prf, in mathcomp.analysis.topology_theory.discrete_topology]
    Builders_6.discrete_entourage_inv [prf, in mathcomp.analysis.topology_theory.discrete_topology]
    Builders_6.discrete_entourage_nbhsE [prf, in mathcomp.analysis.topology_theory.discrete_topology]
    Builders_6.discrete_entourage_split_ex [prf, in mathcomp.analysis.topology_theory.discrete_topology]
    Builders_6.divrr [prf, in mathcomp.field.falgebra]
    Builders_6.invr_out [prf, in mathcomp.field.falgebra]
    Builders_6.measurable [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
    Builders_6.measurable0 [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
    Builders_6.measurableD [abbrev, in mathcomp.analysis.measure_theory.measurable_structure]
    Builders_6.mulVr [prf, in mathcomp.field.falgebra]
    Builders_6.op [abbrev, in mathcomp.analysis.topology_theory.topology_structure]
    Builders_6.op_bigU [abbrev, in mathcomp.analysis.topology_theory.topology_structure]
    Builders_6.opI [abbrev, in mathcomp.analysis.topology_theory.topology_structure]
    Builders_6.opT [abbrev, in mathcomp.analysis.topology_theory.topology_structure]
    Builders_6.Super [mod, in mathcomp.field.falgebra]
    Builders_6.Super [mod, in mathcomp.analysis.topology_theory.topology_structure]
    Builders_6.Super [mod, in mathcomp.analysis.topology_theory.discrete_topology]
    Builders_6.Super [mod, in mathcomp.analysis.measure_theory.measurable_structure]
    Builders_6.Super [mod, in mathcomp.algebra.ring_quotient]
    Builders_6.unitrP [prf, in mathcomp.field.falgebra]
    Builders_60 [mod, in mathcomp.boot.monoid]
    Builders_60 [mod, in mathcomp.analysis.kernel]
    Builders_60.Builders_Export_70 [mod, in mathcomp.analysis.kernel]
    Builders_60.Builders_Export_74 [mod, in mathcomp.boot.monoid]
    Builders_60.inv [abbrev, in mathcomp.boot.monoid]
    Builders_60.mul [abbrev, in mathcomp.boot.monoid]
    Builders_60.mul1g [abbrev, in mathcomp.boot.monoid]
    Builders_60.mulg1 [abbrev, in mathcomp.boot.monoid]
    Builders_60.mulgA [abbrev, in mathcomp.boot.monoid]
    Builders_60.mulgV [abbrev, in mathcomp.boot.monoid]
    Builders_60.mulVg [abbrev, in mathcomp.boot.monoid]
    Builders_60.one [abbrev, in mathcomp.boot.monoid]
    Builders_60.prob_kernel [abbrev, in mathcomp.analysis.kernel]
    Builders_60.Super [mod, in mathcomp.boot.monoid]
    Builders_60.Super [mod, in mathcomp.analysis.kernel]
    Builders_64 [mod, in mathcomp.classical.classical_sets]
    Builders_64.axiom [abbrev, in mathcomp.classical.classical_sets]
    Builders_64.Builders_Export_72 [mod, in mathcomp.classical.classical_sets]
    Builders_64.fin_axiom [prf, in mathcomp.classical.classical_sets]
    Builders_64.pickle [def, in mathcomp.classical.classical_sets]
    Builders_64.pickleK [prf, in mathcomp.classical.classical_sets]
    Builders_64.Super [mod, in mathcomp.classical.classical_sets]
    Builders_64.unpickle [def, in mathcomp.classical.classical_sets]
    Builders_69 [mod, in mathcomp.analysis.measure_theory.measure_function]
    Builders_69.Builders_Export_75 [mod, in mathcomp.analysis.measure_theory.measure_function]
    Builders_69.sfinite [prf, in mathcomp.analysis.measure_theory.measure_function]
    Builders_69.sigma_finiteT [abbrev, in mathcomp.analysis.measure_theory.measure_function]
    Builders_69.Super [mod, in mathcomp.analysis.measure_theory.measure_function]
    Builders_73 [mod, in mathcomp.classical.classical_sets]
    Builders_73.axiom [abbrev, in mathcomp.classical.classical_sets]
    Builders_73.Builders_Export_83 [mod, in mathcomp.classical.classical_sets]
    Builders_73.eq_find [prf, in mathcomp.classical.classical_sets]
    Builders_73.eq_op [def, in mathcomp.classical.classical_sets]
    Builders_73.eq_opP [prf, in mathcomp.classical.classical_sets]
    Builders_73.ex_find [prf, in mathcomp.classical.classical_sets]
    Builders_73.find [def, in mathcomp.classical.classical_sets]
    Builders_73.findP [prf, in mathcomp.classical.classical_sets]
    Builders_73.Super [mod, in mathcomp.classical.classical_sets]
    Builders_75 [mod, in mathcomp.boot.monoid]
    Builders_75.Builders_Export_81 [mod, in mathcomp.boot.monoid]
    Builders_75.Super [mod, in mathcomp.boot.monoid]
    Builders_77 [mod, in mathcomp.boot.choice]
    Builders_77.Builders_Export_85 [mod, in mathcomp.boot.choice]
    Builders_77.pickle [abbrev, in mathcomp.boot.choice]
    Builders_77.pickleK [abbrev, in mathcomp.boot.choice]
    Builders_77.Super [mod, in mathcomp.boot.choice]
    Builders_77.unpickle [abbrev, in mathcomp.boot.choice]
    Builders_8 [mod, in mathcomp.classical.functions]
    Builders_8 [mod, in mathcomp.analysis.topology_theory.uniform_structure]
    Builders_8 [mod, in mathcomp.analysis.normedtype_theory.tvs]
    Builders_8.Builders_Export_14 [mod, in mathcomp.classical.functions]
    Builders_8.Builders_Export_14 [mod, in mathcomp.analysis.normedtype_theory.tvs]
    Builders_8.Builders_Export_16 [mod, in mathcomp.analysis.topology_theory.uniform_structure]
    Builders_8.entourage [abbrev, in mathcomp.analysis.topology_theory.uniform_structure]
    Builders_8.entourage_diagonal [abbrev, in mathcomp.analysis.topology_theory.uniform_structure]
    Builders_8.entourage_filter [abbrev, in mathcomp.analysis.topology_theory.uniform_structure]
    Builders_8.entourage_inv [abbrev, in mathcomp.analysis.topology_theory.uniform_structure]
    Builders_8.entourage_split_ex [abbrev, in mathcomp.analysis.topology_theory.uniform_structure]
    Builders_8.oinv [abbrev, in mathcomp.classical.functions]
    Builders_8.oinvK [abbrev, in mathcomp.classical.functions]
    Builders_8.oinvS [abbrev, in mathcomp.classical.functions]
    Builders_8.opp_continuous [prf, in mathcomp.analysis.normedtype_theory.tvs]
    Builders_8.scale_continuous [abbrev, in mathcomp.analysis.normedtype_theory.tvs]
    Builders_8.Super [mod, in mathcomp.classical.functions]
    Builders_8.Super [mod, in mathcomp.analysis.topology_theory.uniform_structure]
    Builders_8.Super [mod, in mathcomp.analysis.normedtype_theory.tvs]
    Builders_82 [mod, in mathcomp.boot.monoid]
    Builders_82 [mod, in mathcomp.analysis.measure_theory.measure_function]
    Builders_82.Builders_Export_88 [mod, in mathcomp.boot.monoid]
    Builders_82.Builders_Export_90 [mod, in mathcomp.analysis.measure_theory.measure_function]
    Builders_82.fin_num_measure [abbrev, in mathcomp.analysis.measure_theory.measure_function]
    Builders_82.gmulf1 [prf, in mathcomp.boot.monoid]
    Builders_82.gmulfF [abbrev, in mathcomp.boot.monoid]
    Builders_82.gmulfM [prf, in mathcomp.boot.monoid]
    Builders_82.Super [mod, in mathcomp.boot.monoid]
    Builders_82.Super [mod, in mathcomp.analysis.measure_theory.measure_function]
    Builders_88 [mod, in mathcomp.analysis.charge]
    Builders_88.Builders_Export_94 [mod, in mathcomp.analysis.charge]
    Builders_88.fin_num_measure [abbrev, in mathcomp.analysis.charge]
    Builders_88.Super [mod, in mathcomp.analysis.charge]
    Builders_972 [mod, in mathcomp.analysis.normedtype_theory.normed_module]
    Builders_972.Builders_Export_993 [mod, in mathcomp.analysis.normedtype_theory.normed_module]
    Builders_972.ler_normD [abbrev, in mathcomp.analysis.normedtype_theory.normed_module]
    Builders_972.norm [abbrev, in mathcomp.analysis.normedtype_theory.normed_module]
    Builders_972.normr0_eq0 [abbrev, in mathcomp.analysis.normedtype_theory.normed_module]
    Builders_972.normrMn [prf, in mathcomp.analysis.normedtype_theory.normed_module]
    Builders_972.normrN [prf, in mathcomp.analysis.normedtype_theory.normed_module]
    Builders_972.normrZ [abbrev, in mathcomp.analysis.normedtype_theory.normed_module]
    Builders_972.Super [mod, in mathcomp.analysis.normedtype_theory.normed_module]
    bump [def, in mathcomp.boot.fintype]
    bumpC [prf, in mathcomp.boot.fintype]
    bumpDl [prf, in mathcomp.boot.fintype]
    bumpK [prf, in mathcomp.boot.fintype]
    bumpS [prf, in mathcomp.boot.fintype]
    burnside_app [file, in mathcomp.solvable.burnside_app]
    burnside_app2 [prf, in mathcomp.solvable.burnside_app]
    burnside_app_iso [prf, in mathcomp.solvable.burnside_app]
    burnside_app_iso3 [prf, in mathcomp.solvable.burnside_app]
    burnside_app_iso_2_4col [prf, in mathcomp.solvable.burnside_app]
    burnside_app_iso_3_3col [prf, in mathcomp.solvable.burnside_app]
    burnside_app_rot [prf, in mathcomp.solvable.burnside_app]
    burnside_formula [prf, in mathcomp.solvable.burnside_app]
    BV [abbrev, in mathcomp.analysis.realfun]
    BV [abbrev, in mathcomp.analysis.realfun]
    BV [abbrev, in mathcomp.analysis.numfun]
    Generated by rocqnavi