B (Lemmas)

Files

Definitions

Lemmas

Abbreviations

Global Index

B (Lemmas)

Baer_Suzuki [prf, in mathcomp.solvable.sylow]
Baire [prf, in mathcomp.analysis.sequences]
ball0 [prf, in mathcomp.analysis.normedtype_theory.num_normedtype]
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_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_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]
ballxx [prf, in mathcomp.analysis.topology_theory.pseudometric_structure]
banach_fixed_point [prf, in mathcomp.analysis.sequences]
Banach_Steinhauss [prf, in mathcomp.analysis.sequences]
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_suproof [prf, 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]
baseVspace_module [prf, in mathcomp.field.fieldext]
basis_free [prf, in mathcomp.algebra.vector]
basis_mem [prf, in mathcomp.algebra.vector]
basis_not0 [prf, in mathcomp.algebra.vector]
basisEdim [prf, in mathcomp.algebra.vector]
basisEfree [prf, in mathcomp.algebra.vector]
before_find [prf, in mathcomp.boot.seq]
behead_bseqP [prf, in mathcomp.boot.tuple]
behead_map [prf, in mathcomp.boot.seq]
behead_tupleP [prf, 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_tupleP [prf, in mathcomp.boot.tuple]
bernoulli_dirac [prf, 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_probE [prf, in mathcomp.analysis.probability_theory.bernoulli_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_ge0 [prf, in mathcomp.analysis.probability_theory.beta_distribution]
beta_pdf_le_beta_funV [prf, in mathcomp.analysis.probability_theory.beta_distribution]
beta_prob01 [prf, 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]
Bezoutl [prf, in mathcomp.boot.div]
Bezoutr [prf, in mathcomp.boot.div]
Bezoutz [prf, in mathcomp.algebra.intdiv]
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_val [prf, in mathcomp.boot.bigop]
big_enum_val_cond [prf, in mathcomp.boot.bigop]
big_enumP [prf, 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_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_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_cond [prf, in mathcomp.boot.bigop]
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_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]
bigcap0 [prf, 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_fsetD1 [prf, in mathcomp.classical.classical_sets]
bigcap_fsetU1 [prf, in mathcomp.classical.classical_sets]
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]
bigcup0 [prf, in mathcomp.classical.classical_sets]
bigcup0P [prf, in mathcomp.classical.classical_sets]
bigcup0P [prf, in mathcomp.boot.finset]
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_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_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_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.context_big_enough [prf, in mathcomp.bigenough.bigenough]
BigEnough.instantiate_bigger_than [prf, in mathcomp.bigenough.bigenough]
BigEnough.leq_big_internalE [prf, in mathcomp.bigenough.bigenough]
BigEnough.next_bigger_than [prf, in mathcomp.bigenough.bigenough]
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_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]
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]
bigO_bigO_eqO [prf, in mathcomp.analysis.landau]
bigO_class [prf, in mathcomp.analysis.landau]
bigO_eqO [prf, in mathcomp.analysis.landau]
bigO_exP [prf, in mathcomp.analysis.landau]
bigO_littleo_eqo [prf, in mathcomp.analysis.landau]
bigOE [prf, in mathcomp.analysis.landau]
bigOmega [prf, in mathcomp.analysis.landau]
bigOmega_class [prf, in mathcomp.analysis.landau]
bigOmegaP [prf, in mathcomp.analysis.landau]
bigOP [prf, 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]
bigThetaE [prf, in mathcomp.analysis.landau]
bigThetaP [prf, in mathcomp.analysis.landau]
bigU [prf, in mathcomp.boot.bigop]
bigU_idem [prf, in mathcomp.boot.bigop]
bij [prf, 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_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]
bijective_contract [prf, in mathcomp.analysis.ereal]
bijPex [prf, in mathcomp.classical.cardinality]
bijpinv_bij [prf, in mathcomp.classical.functions]
bijTT [prf, in mathcomp.classical.functions]
bilinear_eqo [prf, in mathcomp.analysis.derive]
bilinear_schwarz [prf, in mathcomp.analysis.derive]
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_natK [prf, in mathcomp.boot.ssrnat]
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_mxsum_proof [prf, in mathcomp.algebra.mxalgebra]
binE [prf, in mathcomp.boot.binomial]
binn [prf, in mathcomp.boot.binomial]
binomial_msum [prf, in mathcomp.analysis.probability_theory.binomial_distribution]
binomial_pmf_ge0 [prf, 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]
block_diag_mx_unit [prf, 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_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]
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]
Boole_inequality [prf, in mathcomp.analysis.measure_theory.measure_function]
bottom [prf, in mathcomp.reals.signed]
bottom [prf, in mathcomp.algebra.interval_inference]
bound_extremal_groups [prf, in mathcomp.solvable.extremal]
bound_itvE [prf, in mathcomp.analysis.normedtype_theory.num_normedtype]
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_meetA [prf, in mathcomp.algebra.interval]
bound_meetC [prf, in mathcomp.algebra.interval]
bound_meetKU [prf, in mathcomp.algebra.interval]
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_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_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_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]
bpwedgeE [prf, in mathcomp.analysis.homotopy_theory.wedge_sigT]
BRight_le_map_itv_bound_EFin [prf, in mathcomp.reals.constructive_ereal]
BRight_le_num_itv_bound [prf, in mathcomp.algebra.interval_inference]
bseq0 [prf, 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]
BSide_max [prf, in mathcomp.algebra.interval]
BSide_min [prf, in mathcomp.algebra.interval]
Builders_1.add_continuous [prf, in mathcomp.analysis.normedtype_theory.tvs]
Builders_1.dim_gt0 [prf, in mathcomp.field.falgebra]
Builders_1.iJ [prf, in mathcomp.field.algC]
Builders_1.invgK [prf, in mathcomp.finite_group.fingroup]
Builders_1.invMg [prf, in mathcomp.finite_group.fingroup]
Builders_1.le_outer_measure [prf, in mathcomp.analysis.measure_theory.measure_extension]
Builders_1.leB [prf, in mathcomp.field.algC]
Builders_1.mul2I [prf, 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.nz2 [prf, in mathcomp.field.algC]
Builders_1.opp_continuous [prf, in mathcomp.analysis.normedtype_theory.tvs]
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.sposD [prf, in mathcomp.field.algC]
Builders_1.sposDl [prf, in mathcomp.field.algC]
Builders_1.sqrMi [prf, in mathcomp.field.algC]
Builders_1.sqrtE [prf, in mathcomp.field.algC]
Builders_1.sqrtK [prf, in mathcomp.field.algC]
Builders_109.valM [prf, in mathcomp.boot.monoid]
Builders_118.mulgA [prf, in mathcomp.boot.monoid]
Builders_128.mul1g [prf, in mathcomp.boot.monoid]
Builders_128.mulg1 [prf, in mathcomp.boot.monoid]
Builders_128.val1 [prf, in mathcomp.boot.monoid]
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_14.mD [prf, in mathcomp.analysis.measure_theory.measurable_structure]
Builders_14.mI [prf, in mathcomp.analysis.measure_theory.measurable_structure]
Builders_15.add_unif_continuous [prf, in mathcomp.analysis.normedtype_theory.tvs]
Builders_15.funoK [prf, in mathcomp.classical.functions]
Builders_15.opp_unif_continuous [prf, in mathcomp.analysis.normedtype_theory.tvs]
Builders_151.mulgV [prf, in mathcomp.boot.monoid]
Builders_151.mulVg [prf, in mathcomp.boot.monoid]
Builders_151.umagma_closed [prf, in mathcomp.boot.monoid]
Builders_20.oinvK [prf, in mathcomp.classical.functions]
Builders_20.oinvS [prf, in mathcomp.classical.functions]
Builders_22.opp_unif_continuous [prf, in mathcomp.analysis.normedtype_theory.tvs]
Builders_26.mem_sub_enum [prf, in mathcomp.boot.fintype]
Builders_26.sub_enum_uniq [prf, in mathcomp.boot.fintype]
Builders_26.val_sub_enum [prf, in mathcomp.boot.fintype]
Builders_27.mD [prf, in mathcomp.analysis.measure_theory.measurable_structure]
Builders_27.measurableT [prf, in mathcomp.analysis.measure_theory.measurable_structure]
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.nbhsE [prf, in mathcomp.analysis.normedtype_theory.tvs]
Builders_29.nbhsN [prf, in mathcomp.analysis.normedtype_theory.tvs]
Builders_389.invK [prf, in mathcomp.classical.functions]
Builders_394.exg [prf, in mathcomp.classical.functions]
Builders_41.invg1 [prf, in mathcomp.boot.monoid]
Builders_41.mulg1 [prf, in mathcomp.boot.monoid]
Builders_42.mC [prf, in mathcomp.analysis.measure_theory.measurable_structure]
Builders_42.mU [prf, in mathcomp.analysis.measure_theory.measurable_structure]
Builders_43.sfinite_subdef [prf, in mathcomp.analysis.kernel]
Builders_461.funoK [prf, in mathcomp.classical.functions]
Builders_478.funK [prf, in mathcomp.classical.functions]
Builders_53.invgK [prf, in mathcomp.boot.monoid]
Builders_53.invgM [prf, in mathcomp.boot.monoid]
Builders_53.mulKg [prf, in mathcomp.boot.monoid]
Builders_6.amE [prf, in mathcomp.field.falgebra]
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.mulVr [prf, in mathcomp.field.falgebra]
Builders_6.unitrP [prf, in mathcomp.field.falgebra]
Builders_64.fin_axiom [prf, in mathcomp.classical.classical_sets]
Builders_64.pickleK [prf, in mathcomp.classical.classical_sets]
Builders_69.sfinite [prf, in mathcomp.analysis.measure_theory.measure_function]
Builders_73.eq_find [prf, 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.findP [prf, in mathcomp.classical.classical_sets]
Builders_8.opp_continuous [prf, in mathcomp.analysis.normedtype_theory.tvs]
Builders_82.gmulf1 [prf, in mathcomp.boot.monoid]
Builders_82.gmulfM [prf, in mathcomp.boot.monoid]
Builders_972.normrMn [prf, in mathcomp.analysis.normedtype_theory.normed_module]
Builders_972.normrN [prf, in mathcomp.analysis.normedtype_theory.normed_module]
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_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]