B (Lemmas)
| Files | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
| Definitions | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
| Lemmas | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
| Abbreviations | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ |
| Notations |
B (Lemmas)
Baer_Suzuki [prf, in mathcomp.solvable.sylow]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]
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_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_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_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_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_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_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_trivIset [prf, in mathcomp.boot.finset]
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]
bigcap_inf [prf, in mathcomp.boot.finset]
bigcap_min [prf, in mathcomp.boot.finset]
bigcap_p'core [prf, in mathcomp.solvable.pgroup]
bigcap_seq [prf, in mathcomp.boot.finset]
bigcap_setU [prf, in mathcomp.boot.finset]
bigcapJ [prf, in mathcomp.finite_group.fingroup]
bigcapmx_inf [prf, in mathcomp.algebra.mxalgebra]
bigcapmx_module [prf, in mathcomp.group_representation.mxrepresentation]
bigcapP [prf, in mathcomp.boot.finset]
bigcapsP [prf, in mathcomp.boot.finset]
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]
bigcprod_rowg [prf, in mathcomp.group_representation.mxabelem]
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]
bigcup0P [prf, in mathcomp.boot.finset]
bigcup_disjoint [prf, in mathcomp.boot.finset]
bigcup_disjointP [prf, in mathcomp.boot.finset]
bigcup_max [prf, in mathcomp.boot.finset]
bigcup_seq [prf, in mathcomp.boot.finset]
bigcup_setU [prf, in mathcomp.boot.finset]
bigcup_sup [prf, in mathcomp.boot.finset]
bigcupJ [prf, in mathcomp.finite_group.fingroup]
bigcupP [prf, in mathcomp.boot.finset]
bigcupsP [prf, in mathcomp.boot.finset]
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]
bigdprod_rowg [prf, in mathcomp.group_representation.mxabelem]
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]
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_leqP [prf, in mathcomp.boot.bigop]
bigmax_leqP_seq [prf, in mathcomp.boot.bigop]
bigmax_sup [prf, in mathcomp.boot.bigop]
bigmaxn_sup_seq [prf, in mathcomp.boot.bigop]
bigprodGE [prf, in mathcomp.finite_group.fingroup]
bigprodGEgen [prf, in mathcomp.finite_group.fingroup]
bigU [prf, in mathcomp.boot.bigop]
bigU_idem [prf, in mathcomp.boot.bigop]
bij_eq [prf, in mathcomp.boot.eqtype]
bij_eq_card [prf, in mathcomp.boot.fintype]
bij_on_codom [prf, in mathcomp.boot.fintype]
bij_on_image [prf, in mathcomp.boot.fintype]
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_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]
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]
bool_enumP [prf, in mathcomp.boot.fintype]
bool_fieldP [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
bool_irrelevance [prf, in mathcomp.boot.eqtype]
bool_of_unitK [prf, in mathcomp.boot.choice]
bottom [prf, in mathcomp.algebra.interval_inference]
bound_extremal_groups [prf, in mathcomp.solvable.extremal]
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]
boundl_in_itv [prf, in mathcomp.algebra.interval]
boundr_in_itv [prf, in mathcomp.algebra.interval]
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.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.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.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.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_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_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_41.invg1 [prf, in mathcomp.boot.monoid]
Builders_41.mulg1 [prf, in mathcomp.boot.monoid]
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.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_82.gmulf1 [prf, in mathcomp.boot.monoid]
Builders_82.gmulfM [prf, in mathcomp.boot.monoid]
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]
Burnside_p_a_q_b [prf, in mathcomp.group_representation.integral_char]