| 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 | +_ | +other | +(23233 entries) | +
| Notation 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 | +_ | +other | +(1373 entries) | +
| Module 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 | +_ | +other | +(213 entries) | +
| Variable 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 | +_ | +other | +(3475 entries) | +
| Library 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 | +_ | +other | +(89 entries) | +
| Lemma 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 | +_ | +other | +(11853 entries) | +
| Constructor 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 | +_ | +other | +(359 entries) | +
| Axiom 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 | +_ | +other | +(47 entries) | +
| Inductive 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 | +_ | +other | +(103 entries) | +
| Projection 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 | +_ | +other | +(266 entries) | +
| Section 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 | +_ | +other | +(1118 entries) | +
| Abbreviation 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 | +_ | +other | +(691 entries) | +
| Definition 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 | +_ | +other | +(3461 entries) | +
| Record 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 | +_ | +other | +(185 entries) | +
M (lemma)
+mactE [in mathcomp.fingroup.action]+mact_is_action [in mathcomp.fingroup.action]
+make_separable [in mathcomp.field.separable]
+mapK [in mathcomp.ssreflect.seq]
+mapP [in mathcomp.ssreflect.seq]
+map_path [in mathcomp.ssreflect.path]
+map_orthonormal [in mathcomp.character.vcharacter]
+map_pairwise_orthogonal [in mathcomp.character.vcharacter]
+map_minPoly [in mathcomp.field.fieldext]
+map_regular_subseries [in mathcomp.character.mxrepresentation]
+map_section_repr [in mathcomp.character.mxrepresentation]
+map_mx_abs_irr [in mathcomp.character.mxrepresentation]
+map_mx_faithful [in mathcomp.character.mxrepresentation]
+map_rfix_mx [in mathcomp.character.mxrepresentation]
+map_group_ring [in mathcomp.character.mxrepresentation]
+map_regular_repr [in mathcomp.character.mxrepresentation]
+map_gring_op [in mathcomp.character.mxrepresentation]
+map_gring_mx [in mathcomp.character.mxrepresentation]
+map_enveloping_algebra_mx [in mathcomp.character.mxrepresentation]
+map_reprJ [in mathcomp.character.mxrepresentation]
+map_reprE [in mathcomp.character.mxrepresentation]
+map_mx_repr [in mathcomp.character.mxrepresentation]
+map_gring_proj [in mathcomp.character.mxrepresentation]
+map_gring_row [in mathcomp.character.mxrepresentation]
+map_regular_mx [in mathcomp.character.mxrepresentation]
+map_poly_divzK [in mathcomp.algebra.intdiv]
+map_tupleP [in mathcomp.ssreflect.tuple]
+map_tnth_enum [in mathcomp.ssreflect.tuple]
+map_mx_eq0 [in mathcomp.algebra.matrix]
+map_mx_inv [in mathcomp.algebra.matrix]
+map_invmx [in mathcomp.algebra.matrix]
+map_mx_unit [in mathcomp.algebra.matrix]
+map_unitmx [in mathcomp.algebra.matrix]
+map_mx_is_scalar [in mathcomp.algebra.matrix]
+map_mx_inj [in mathcomp.algebra.matrix]
+map_lin_mx [in mathcomp.algebra.matrix]
+map_lin1_mx [in mathcomp.algebra.matrix]
+map_mx_is_multiplicative [in mathcomp.algebra.matrix]
+map_copid_mx [in mathcomp.algebra.matrix]
+map_mx_adj [in mathcomp.algebra.matrix]
+map_pid_mx [in mathcomp.algebra.matrix]
+map_tperm_mx [in mathcomp.algebra.matrix]
+map_perm_mx [in mathcomp.algebra.matrix]
+map_mx1 [in mathcomp.algebra.matrix]
+map_scalar_mx [in mathcomp.algebra.matrix]
+map_diag_mx [in mathcomp.algebra.matrix]
+map_delta_mx [in mathcomp.algebra.matrix]
+map_mxM [in mathcomp.algebra.matrix]
+map_mxZ [in mathcomp.algebra.matrix]
+map_mx_sub [in mathcomp.algebra.matrix]
+map_mxD [in mathcomp.algebra.matrix]
+map_mxN [in mathcomp.algebra.matrix]
+map_mx0 [in mathcomp.algebra.matrix]
+map_drsubmx [in mathcomp.algebra.matrix]
+map_dlsubmx [in mathcomp.algebra.matrix]
+map_ursubmx [in mathcomp.algebra.matrix]
+map_ulsubmx [in mathcomp.algebra.matrix]
+map_dsubmx [in mathcomp.algebra.matrix]
+map_usubmx [in mathcomp.algebra.matrix]
+map_rsubmx [in mathcomp.algebra.matrix]
+map_lsubmx [in mathcomp.algebra.matrix]
+map_block_mx [in mathcomp.algebra.matrix]
+map_col_mx [in mathcomp.algebra.matrix]
+map_row_mx [in mathcomp.algebra.matrix]
+map_vec_mx [in mathcomp.algebra.matrix]
+map_mxvec [in mathcomp.algebra.matrix]
+map_conform_mx [in mathcomp.algebra.matrix]
+map_castmx [in mathcomp.algebra.matrix]
+map_xcol [in mathcomp.algebra.matrix]
+map_xrow [in mathcomp.algebra.matrix]
+map_col_perm [in mathcomp.algebra.matrix]
+map_row_perm [in mathcomp.algebra.matrix]
+map_col' [in mathcomp.algebra.matrix]
+map_row' [in mathcomp.algebra.matrix]
+map_col [in mathcomp.algebra.matrix]
+map_row [in mathcomp.algebra.matrix]
+map_const_mx [in mathcomp.algebra.matrix]
+map_trmx [in mathcomp.algebra.matrix]
+map_mx_key [in mathcomp.algebra.matrix]
+map_mx_inv_horner [in mathcomp.algebra.mxpoly]
+map_horner_mx [in mathcomp.algebra.mxpoly]
+map_powers_mx [in mathcomp.algebra.mxpoly]
+map_resultant [in mathcomp.algebra.mxpoly]
+map_char_poly [in mathcomp.algebra.mxpoly]
+map_char_poly_mx [in mathcomp.algebra.mxpoly]
+map_poly_rV [in mathcomp.algebra.mxpoly]
+map_rVpoly [in mathcomp.algebra.mxpoly]
+map_div_annihilantP [in mathcomp.algebra.polyXY]
+map_sub_annihilantP [in mathcomp.algebra.polyXY]
+map_Qnum_poly [in mathcomp.field.algnum]
+map_reshape [in mathcomp.ssreflect.seq]
+map_flatten [in mathcomp.ssreflect.seq]
+map_pK [in mathcomp.ssreflect.seq]
+map_id_in [in mathcomp.ssreflect.seq]
+map_comp [in mathcomp.ssreflect.seq]
+map_id [in mathcomp.ssreflect.seq]
+map_of_seq [in mathcomp.ssreflect.seq]
+map_inj_uniq [in mathcomp.ssreflect.seq]
+map_subseq [in mathcomp.ssreflect.seq]
+map_inj_in_uniq [in mathcomp.ssreflect.seq]
+map_uniq [in mathcomp.ssreflect.seq]
+map_f [in mathcomp.ssreflect.seq]
+map_mask [in mathcomp.ssreflect.seq]
+map_rev [in mathcomp.ssreflect.seq]
+map_rotr [in mathcomp.ssreflect.seq]
+map_rot [in mathcomp.ssreflect.seq]
+map_drop [in mathcomp.ssreflect.seq]
+map_take [in mathcomp.ssreflect.seq]
+map_rcons [in mathcomp.ssreflect.seq]
+map_cat [in mathcomp.ssreflect.seq]
+map_nseq [in mathcomp.ssreflect.seq]
+map_cons [in mathcomp.ssreflect.seq]
+map_preim [in mathcomp.ssreflect.fintype]
+map_cfAut_free [in mathcomp.character.classfun]
+map_orthogonal [in mathcomp.character.classfun]
+map_uniq_roots [in mathcomp.algebra.poly]
+map_diff_roots [in mathcomp.algebra.poly]
+map_poly_com [in mathcomp.algebra.poly]
+map_monic [in mathcomp.algebra.poly]
+map_poly_inj [in mathcomp.algebra.poly]
+map_poly_eq0 [in mathcomp.algebra.poly]
+map_comp_poly [in mathcomp.algebra.poly]
+map_polyC_eq0 [in mathcomp.algebra.poly]
+map_comm_coef [in mathcomp.algebra.poly]
+map_comm_poly [in mathcomp.algebra.poly]
+map_polyXn [in mathcomp.algebra.poly]
+map_polyX [in mathcomp.algebra.poly]
+map_polyZ [in mathcomp.algebra.poly]
+map_poly_is_rmorphism [in mathcomp.algebra.poly]
+map_polyC [in mathcomp.algebra.poly]
+map_poly_is_additive [in mathcomp.algebra.poly]
+map_poly_comp [in mathcomp.algebra.poly]
+map_Poly [in mathcomp.algebra.poly]
+map_polyK [in mathcomp.algebra.poly]
+map_inj_poly [in mathcomp.algebra.poly]
+map_poly_eq0_id0 [in mathcomp.algebra.poly]
+map_poly_comp_id0 [in mathcomp.algebra.poly]
+map_Poly_id0 [in mathcomp.algebra.poly]
+map_poly_id [in mathcomp.algebra.poly]
+map_poly0 [in mathcomp.algebra.poly]
+map_polyE [in mathcomp.algebra.poly]
+map_center_mx [in mathcomp.algebra.mxalgebra]
+map_cent_mx [in mathcomp.algebra.mxalgebra]
+map_mulsmx [in mathcomp.algebra.mxalgebra]
+map_eigenspace [in mathcomp.algebra.mxalgebra]
+map_diffmx [in mathcomp.algebra.mxalgebra]
+map_complmx [in mathcomp.algebra.mxalgebra]
+map_capmx [in mathcomp.algebra.mxalgebra]
+map_capmx_gen [in mathcomp.algebra.mxalgebra]
+map_addsmx [in mathcomp.algebra.mxalgebra]
+map_genmx [in mathcomp.algebra.mxalgebra]
+map_eqmx [in mathcomp.algebra.mxalgebra]
+map_ltmx [in mathcomp.algebra.mxalgebra]
+map_submx [in mathcomp.algebra.mxalgebra]
+map_cokermx [in mathcomp.algebra.mxalgebra]
+map_kermx [in mathcomp.algebra.mxalgebra]
+map_pinvmx [in mathcomp.algebra.mxalgebra]
+map_col_base [in mathcomp.algebra.mxalgebra]
+map_row_base [in mathcomp.algebra.mxalgebra]
+map_col_ebase [in mathcomp.algebra.mxalgebra]
+map_row_ebase [in mathcomp.algebra.mxalgebra]
+mask_subseq [in mathcomp.ssreflect.seq]
+mask_uniq [in mathcomp.ssreflect.seq]
+mask_rot [in mathcomp.ssreflect.seq]
+mask_cat [in mathcomp.ssreflect.seq]
+mask_cons [in mathcomp.ssreflect.seq]
+mask_true [in mathcomp.ssreflect.seq]
+mask_false [in mathcomp.ssreflect.seq]
+mask0 [in mathcomp.ssreflect.seq]
+mask1 [in mathcomp.ssreflect.seq]
+MatrixFormula.eval_row_var [in mathcomp.algebra.mxpoly]
+MatrixFormula.eval_submx [in mathcomp.algebra.mxpoly]
+MatrixFormula.eval_col_mx [in mathcomp.algebra.mxpoly]
+MatrixFormula.eval_mxvec [in mathcomp.algebra.mxpoly]
+MatrixFormula.eval_vec_mx [in mathcomp.algebra.mxpoly]
+MatrixFormula.eval_mxrank [in mathcomp.algebra.mxpoly]
+MatrixFormula.eval_mulmx [in mathcomp.algebra.mxpoly]
+MatrixFormula.eval_mx_term [in mathcomp.algebra.mxpoly]
+MatrixFormula.Exists_rowP [in mathcomp.algebra.mxpoly]
+MatrixFormula.mxrank_form_qf [in mathcomp.algebra.mxpoly]
+MatrixFormula.nth_row_env [in mathcomp.algebra.mxpoly]
+MatrixFormula.nth_seq_of_rV [in mathcomp.algebra.mxpoly]
+MatrixFormula.size_seq_of_rV [in mathcomp.algebra.mxpoly]
+MatrixFormula.submx_form_qf [in mathcomp.algebra.mxpoly]
+MatrixGenField.base_full [in mathcomp.character.mxrepresentation]
+MatrixGenField.base_free [in mathcomp.character.mxrepresentation]
+MatrixGenField.card_gen [in mathcomp.character.mxrepresentation]
+MatrixGenField.eval_gen_term [in mathcomp.character.mxrepresentation]
+MatrixGenField.eval_mulT [in mathcomp.character.mxrepresentation]
+MatrixGenField.genK [in mathcomp.character.mxrepresentation]
+MatrixGenField.gen_satP [in mathcomp.character.mxrepresentation]
+MatrixGenField.gen_mx_faithful [in mathcomp.character.mxrepresentation]
+MatrixGenField.gen_mx_irr [in mathcomp.character.mxrepresentation]
+MatrixGenField.gen_mx_repr [in mathcomp.character.mxrepresentation]
+MatrixGenField.gen_dim_gt0 [in mathcomp.character.mxrepresentation]
+MatrixGenField.gen_dim_factor [in mathcomp.character.mxrepresentation]
+MatrixGenField.gen_dim_ub_proof [in mathcomp.character.mxrepresentation]
+MatrixGenField.gen_dim_ex_proof [in mathcomp.character.mxrepresentation]
+MatrixGenField.gen_is_rmorphism [in mathcomp.character.mxrepresentation]
+MatrixGenField.gen_invr0 [in mathcomp.character.mxrepresentation]
+MatrixGenField.gen_mulVr [in mathcomp.character.mxrepresentation]
+MatrixGenField.gen_ntriv [in mathcomp.character.mxrepresentation]
+MatrixGenField.gen_mulDr [in mathcomp.character.mxrepresentation]
+MatrixGenField.gen_mul1r [in mathcomp.character.mxrepresentation]
+MatrixGenField.gen_mulC [in mathcomp.character.mxrepresentation]
+MatrixGenField.gen_mulA [in mathcomp.character.mxrepresentation]
+MatrixGenField.gen_addNr [in mathcomp.character.mxrepresentation]
+MatrixGenField.gen_add0r [in mathcomp.character.mxrepresentation]
+MatrixGenField.gen_addC [in mathcomp.character.mxrepresentation]
+MatrixGenField.gen_addA [in mathcomp.character.mxrepresentation]
+MatrixGenField.in_genJ [in mathcomp.character.mxrepresentation]
+MatrixGenField.in_gen_row [in mathcomp.character.mxrepresentation]
+MatrixGenField.in_genZ [in mathcomp.character.mxrepresentation]
+MatrixGenField.in_genD [in mathcomp.character.mxrepresentation]
+MatrixGenField.in_genN [in mathcomp.character.mxrepresentation]
+MatrixGenField.in_gen0 [in mathcomp.character.mxrepresentation]
+MatrixGenField.in_genK [in mathcomp.character.mxrepresentation]
+MatrixGenField.map_mxminpoly_groot [in mathcomp.character.mxrepresentation]
+MatrixGenField.mxmodule_rowval_gen [in mathcomp.character.mxrepresentation]
+MatrixGenField.mxvalD [in mathcomp.character.mxrepresentation]
+MatrixGenField.mxvalM [in mathcomp.character.mxrepresentation]
+MatrixGenField.mxvalN [in mathcomp.character.mxrepresentation]
+MatrixGenField.mxvalV [in mathcomp.character.mxrepresentation]
+MatrixGenField.mxval_grootX [in mathcomp.character.mxrepresentation]
+MatrixGenField.mxval_groot [in mathcomp.character.mxrepresentation]
+MatrixGenField.mxval_centg [in mathcomp.character.mxrepresentation]
+MatrixGenField.mxval_is_multiplicative [in mathcomp.character.mxrepresentation]
+MatrixGenField.mxval_sub [in mathcomp.character.mxrepresentation]
+MatrixGenField.mxval_genV [in mathcomp.character.mxrepresentation]
+MatrixGenField.mxval_genM [in mathcomp.character.mxrepresentation]
+MatrixGenField.mxval_gen1 [in mathcomp.character.mxrepresentation]
+MatrixGenField.mxval_inj [in mathcomp.character.mxrepresentation]
+MatrixGenField.mxval0 [in mathcomp.character.mxrepresentation]
+MatrixGenField.mxval1 [in mathcomp.character.mxrepresentation]
+MatrixGenField.non_linear_gen_reducible [in mathcomp.character.mxrepresentation]
+MatrixGenField.nth_map_rVval [in mathcomp.character.mxrepresentation]
+MatrixGenField.rfix_gen [in mathcomp.character.mxrepresentation]
+MatrixGenField.rker_gen [in mathcomp.character.mxrepresentation]
+MatrixGenField.rowval_gen_stable [in mathcomp.character.mxrepresentation]
+MatrixGenField.rowval_genK [in mathcomp.character.mxrepresentation]
+MatrixGenField.row_gen_sum_mxval [in mathcomp.character.mxrepresentation]
+MatrixGenField.rstabs_rowval_gen [in mathcomp.character.mxrepresentation]
+MatrixGenField.rstabs_in_gen [in mathcomp.character.mxrepresentation]
+MatrixGenField.rstab_in_gen [in mathcomp.character.mxrepresentation]
+MatrixGenField.sat_gen_form [in mathcomp.character.mxrepresentation]
+MatrixGenField.set_nth_map_rVval [in mathcomp.character.mxrepresentation]
+MatrixGenField.submx_rowval_gen [in mathcomp.character.mxrepresentation]
+MatrixGenField.submx_in_gen_eq [in mathcomp.character.mxrepresentation]
+MatrixGenField.submx_in_gen [in mathcomp.character.mxrepresentation]
+MatrixGenField.val_genJ [in mathcomp.character.mxrepresentation]
+MatrixGenField.val_genZ [in mathcomp.character.mxrepresentation]
+MatrixGenField.val_gen_row [in mathcomp.character.mxrepresentation]
+MatrixGenField.val_gen_rV [in mathcomp.character.mxrepresentation]
+MatrixGenField.val_genD [in mathcomp.character.mxrepresentation]
+MatrixGenField.val_genN [in mathcomp.character.mxrepresentation]
+MatrixGenField.val_gen0 [in mathcomp.character.mxrepresentation]
+MatrixGenField.val_genK [in mathcomp.character.mxrepresentation]
+matrixP [in mathcomp.algebra.matrix]
+matrix_vect_iso [in mathcomp.algebra.vector]
+matrix_nonzero1 [in mathcomp.algebra.matrix]
+matrix_sum_delta [in mathcomp.algebra.matrix]
+matrix_key [in mathcomp.algebra.matrix]
+matrix_modr [in mathcomp.algebra.mxalgebra]
+matrix_modl [in mathcomp.algebra.mxalgebra]
+maxainvM [in mathcomp.solvable.jordanholder]
+maxainvS [in mathcomp.solvable.jordanholder]
+maxainv_asimple_quo [in mathcomp.solvable.jordanholder]
+maxainv_exists [in mathcomp.solvable.jordanholder]
+maxainv_ainvar [in mathcomp.solvable.jordanholder]
+maxainv_sub [in mathcomp.solvable.jordanholder]
+maxainv_proper [in mathcomp.solvable.jordanholder]
+maxainv_norm [in mathcomp.solvable.jordanholder]
+maxgroupp [in mathcomp.fingroup.fingroup]
+maxgroupP [in mathcomp.fingroup.fingroup]
+maxgroup_exists [in mathcomp.fingroup.fingroup]
+maximalJ [in mathcomp.solvable.gseries]
+maximal_cycle_extremal [in mathcomp.solvable.extremal]
+maximal_eqJ [in mathcomp.solvable.gseries]
+maximal_exists [in mathcomp.solvable.gseries]
+maximal_eqP [in mathcomp.solvable.gseries]
+maxKn [in mathcomp.ssreflect.ssrnat]
+maxminset [in mathcomp.ssreflect.finset]
+maxnA [in mathcomp.ssreflect.ssrnat]
+maxnAC [in mathcomp.ssreflect.ssrnat]
+maxnACA [in mathcomp.ssreflect.ssrnat]
+maxnC [in mathcomp.ssreflect.ssrnat]
+maxnCA [in mathcomp.ssreflect.ssrnat]
+maxnE [in mathcomp.ssreflect.ssrnat]
+maxnK [in mathcomp.ssreflect.ssrnat]
+maxnn [in mathcomp.ssreflect.ssrnat]
+maxnormalM [in mathcomp.solvable.gseries]
+maxnormal_minnormal [in mathcomp.solvable.gseries]
+maxnormal_sub [in mathcomp.solvable.gseries]
+maxnormal_proper [in mathcomp.solvable.gseries]
+maxnormal_normal [in mathcomp.solvable.gseries]
+maxnormal_charsimple [in mathcomp.solvable.maximal]
+maxnSS [in mathcomp.ssreflect.ssrnat]
+maxn_mull [in mathcomp.ssreflect.ssrnat]
+maxn_mulr [in mathcomp.ssreflect.ssrnat]
+maxn_minr [in mathcomp.ssreflect.ssrnat]
+maxn_minl [in mathcomp.ssreflect.ssrnat]
+maxn_idPr [in mathcomp.ssreflect.ssrnat]
+maxn_idPl [in mathcomp.ssreflect.ssrnat]
+maxn0 [in mathcomp.ssreflect.ssrnat]
+maxsetp [in mathcomp.ssreflect.finset]
+maxsetP [in mathcomp.ssreflect.finset]
+maxsetsup [in mathcomp.ssreflect.finset]
+maxset_exists [in mathcomp.ssreflect.finset]
+maxset_eq [in mathcomp.ssreflect.finset]
+maxset_key [in mathcomp.ssreflect.finset]
+max_pgroupJ [in mathcomp.solvable.pgroup]
+max_pdiv_max [in mathcomp.ssreflect.prime]
+max_pdiv_gt0 [in mathcomp.ssreflect.prime]
+max_pdiv_leq [in mathcomp.ssreflect.prime]
+max_pdiv_dvd [in mathcomp.ssreflect.prime]
+max_pdiv_prime [in mathcomp.ssreflect.prime]
+max_size_mx_series [in mathcomp.character.mxrepresentation]
+max_submod_eqmx [in mathcomp.character.mxrepresentation]
+max_submodP [in mathcomp.character.mxrepresentation]
+max_size_evalC [in mathcomp.algebra.polyXY]
+max_size_evalX [in mathcomp.algebra.polyXY]
+max_size_lead_coefXY [in mathcomp.algebra.polyXY]
+max_size_coefXY [in mathcomp.algebra.polyXY]
+max_cfRepr_mx1 [in mathcomp.character.character]
+max_cfRepr_norm_scalar [in mathcomp.character.character]
+max_card_abelian [in mathcomp.solvable.abelian]
+max_SCN [in mathcomp.solvable.maximal]
+max_card [in mathcomp.ssreflect.fintype]
+max_unity_roots [in mathcomp.algebra.poly]
+max_ring_poly_roots [in mathcomp.algebra.poly]
+max_poly_roots [in mathcomp.algebra.poly]
+max_pgroup_Sylow [in mathcomp.solvable.sylow]
+max0n [in mathcomp.ssreflect.ssrnat]
+meet_Ohm1 [in mathcomp.solvable.abelian]
+meet_center_nil [in mathcomp.solvable.nilpotent]
+memJ_norm [in mathcomp.fingroup.fingroup]
+memJ_class_support [in mathcomp.fingroup.fingroup]
+memJ_class [in mathcomp.fingroup.fingroup]
+memJ_conjg [in mathcomp.fingroup.fingroup]
+memmx_cent_envelop [in mathcomp.character.mxrepresentation]
+memmx_map [in mathcomp.algebra.mxalgebra]
+memmx_sumsP [in mathcomp.algebra.mxalgebra]
+memmx_addsP [in mathcomp.algebra.mxalgebra]
+memmx_eqP [in mathcomp.algebra.mxalgebra]
+memmx_subP [in mathcomp.algebra.mxalgebra]
+memmx0 [in mathcomp.algebra.mxalgebra]
+memmx1 [in mathcomp.algebra.mxalgebra]
+memPn [in mathcomp.ssreflect.eqtype]
+memPnC [in mathcomp.ssreflect.eqtype]
+mempx_Fadjoin [in mathcomp.field.fieldext]
+memtE [in mathcomp.ssreflect.tuple]
+memt_nth [in mathcomp.ssreflect.tuple]
+memvB [in mathcomp.algebra.vector]
+memvD [in mathcomp.algebra.vector]
+memvE [in mathcomp.algebra.vector]
+memvf [in mathcomp.algebra.vector]
+memvM [in mathcomp.field.falgebra]
+memvN [in mathcomp.algebra.vector]
+memvV [in mathcomp.field.falgebra]
+memvZ [in mathcomp.algebra.vector]
+memv_gal [in mathcomp.field.galois]
+memv_sum_pi [in mathcomp.algebra.vector]
+memv_projC [in mathcomp.algebra.vector]
+memv_pi2 [in mathcomp.algebra.vector]
+memv_pi1 [in mathcomp.algebra.vector]
+memv_proj [in mathcomp.algebra.vector]
+memv_pi [in mathcomp.algebra.vector]
+memv_preim [in mathcomp.algebra.vector]
+memv_ker [in mathcomp.algebra.vector]
+memv_imgP [in mathcomp.algebra.vector]
+memv_img [in mathcomp.algebra.vector]
+memv_span1 [in mathcomp.algebra.vector]
+memv_span [in mathcomp.algebra.vector]
+memv_capP [in mathcomp.algebra.vector]
+memv_cap [in mathcomp.algebra.vector]
+memv_sumP [in mathcomp.algebra.vector]
+memv_sumr [in mathcomp.algebra.vector]
+memv_addP [in mathcomp.algebra.vector]
+memv_add [in mathcomp.algebra.vector]
+memv_pick [in mathcomp.algebra.vector]
+memv_line [in mathcomp.algebra.vector]
+memv_suml [in mathcomp.algebra.vector]
+memv_submod_closed [in mathcomp.algebra.vector]
+memV_rcosetV [in mathcomp.fingroup.fingroup]
+memV_lcosetV [in mathcomp.fingroup.fingroup]
+memV_invg [in mathcomp.fingroup.fingroup]
+memv_adjoin [in mathcomp.field.falgebra]
+memv_cosetP [in mathcomp.field.falgebra]
+memv_algid [in mathcomp.field.falgebra]
+memv_mul [in mathcomp.field.falgebra]
+memv0 [in mathcomp.algebra.vector]
+mem_galNorm [in mathcomp.field.galois]
+mem_galTrace [in mathcomp.field.galois]
+mem_fixedFieldP [in mathcomp.field.galois]
+mem_Hall_pcore [in mathcomp.solvable.pgroup]
+mem_normal_Hall [in mathcomp.solvable.pgroup]
+mem_p_elt [in mathcomp.solvable.pgroup]
+mem_quotient [in mathcomp.fingroup.quotient]
+mem_repr_coset [in mathcomp.fingroup.quotient]
+mem_sort [in mathcomp.ssreflect.path]
+mem_merge [in mathcomp.ssreflect.path]
+mem_prev [in mathcomp.ssreflect.path]
+mem_next [in mathcomp.ssreflect.path]
+mem_zchar [in mathcomp.character.vcharacter]
+mem_zchar_on [in mathcomp.character.vcharacter]
+mem_baseVspace [in mathcomp.field.fieldext]
+mem_aspaceOver [in mathcomp.field.fieldext]
+mem_vspaceOver [in mathcomp.field.fieldext]
+mem_pcycle [in mathcomp.fingroup.perm]
+mem_primes [in mathcomp.ssreflect.prime]
+mem_prime_decomp [in mathcomp.ssreflect.prime]
+mem_sub_gring [in mathcomp.character.mxrepresentation]
+mem_gring_mx [in mathcomp.character.mxrepresentation]
+mem_bigdprod [in mathcomp.fingroup.gproduct]
+mem_dprod [in mathcomp.fingroup.gproduct]
+mem_sdprod [in mathcomp.fingroup.gproduct]
+mem_divgr [in mathcomp.fingroup.gproduct]
+mem_remgr [in mathcomp.fingroup.gproduct]
+mem_tnth [in mathcomp.ssreflect.tuple]
+mem_Cint_span [in mathcomp.field.algnum]
+mem_Crat_span [in mathcomp.field.algnum]
+mem_irr [in mathcomp.character.character]
+mem_allpairs [in mathcomp.ssreflect.seq]
+mem_iota [in mathcomp.ssreflect.seq]
+mem_pmap_sub [in mathcomp.ssreflect.seq]
+mem_pmap [in mathcomp.ssreflect.seq]
+mem_map [in mathcomp.ssreflect.seq]
+mem_rem_uniq [in mathcomp.ssreflect.seq]
+mem_rem [in mathcomp.ssreflect.seq]
+mem_subseq [in mathcomp.ssreflect.seq]
+mem_mask_rot [in mathcomp.ssreflect.seq]
+mem_mask [in mathcomp.ssreflect.seq]
+mem_mask_cons [in mathcomp.ssreflect.seq]
+mem_rotr [in mathcomp.ssreflect.seq]
+mem_rot [in mathcomp.ssreflect.seq]
+mem_undup [in mathcomp.ssreflect.seq]
+mem_rev [in mathcomp.ssreflect.seq]
+mem_filter [in mathcomp.ssreflect.seq]
+mem_drop [in mathcomp.ssreflect.seq]
+mem_take [in mathcomp.ssreflect.seq]
+mem_nth [in mathcomp.ssreflect.seq]
+mem_belast [in mathcomp.ssreflect.seq]
+mem_behead [in mathcomp.ssreflect.seq]
+mem_last [in mathcomp.ssreflect.seq]
+mem_head [in mathcomp.ssreflect.seq]
+mem_rcons [in mathcomp.ssreflect.seq]
+mem_cat [in mathcomp.ssreflect.seq]
+mem_seq4 [in mathcomp.ssreflect.seq]
+mem_seq3 [in mathcomp.ssreflect.seq]
+mem_seq2 [in mathcomp.ssreflect.seq]
+mem_seq1 [in mathcomp.ssreflect.seq]
+mem_sum_enum [in mathcomp.ssreflect.fintype]
+mem_ord_enum [in mathcomp.ssreflect.fintype]
+mem_seq_sub_enum [in mathcomp.ssreflect.fintype]
+mem_sub_enum [in mathcomp.ssreflect.fintype]
+mem_image [in mathcomp.ssreflect.fintype]
+mem_iinv [in mathcomp.ssreflect.fintype]
+mem_enum [in mathcomp.ssreflect.fintype]
+mem_orbit [in mathcomp.fingroup.action]
+mem_setact [in mathcomp.fingroup.action]
+mem_unity_roots [in mathcomp.algebra.poly]
+mem_root [in mathcomp.algebra.poly]
+mem_index_enum [in mathcomp.ssreflect.bigop]
+mem_index_iota [in mathcomp.ssreflect.bigop]
+mem_rVabelem [in mathcomp.character.mxabelem]
+mem_im_abelem_rV [in mathcomp.character.mxabelem]
+mem_rowg [in mathcomp.character.mxabelem]
+mem_morphpre [in mathcomp.fingroup.morphism]
+mem_morphim [in mathcomp.fingroup.morphism]
+mem_cycle [in mathcomp.fingroup.fingroup]
+mem_commg [in mathcomp.fingroup.fingroup]
+mem_gen [in mathcomp.fingroup.fingroup]
+mem_class_support [in mathcomp.fingroup.fingroup]
+mem_repr_classes [in mathcomp.fingroup.fingroup]
+mem_lcosets [in mathcomp.fingroup.fingroup]
+mem_rcosets [in mathcomp.fingroup.fingroup]
+mem_repr_rcoset [in mathcomp.fingroup.fingroup]
+mem_classes [in mathcomp.fingroup.fingroup]
+mem_conjgV [in mathcomp.fingroup.fingroup]
+mem_conjg [in mathcomp.fingroup.fingroup]
+mem_rcoset [in mathcomp.fingroup.fingroup]
+mem_lcoset [in mathcomp.fingroup.fingroup]
+mem_invg [in mathcomp.fingroup.fingroup]
+mem_prodg [in mathcomp.fingroup.fingroup]
+mem_mulg [in mathcomp.fingroup.fingroup]
+mem_repr [in mathcomp.fingroup.fingroup]
+mem_closure [in mathcomp.ssreflect.fingraph]
+mem_Zp [in mathcomp.algebra.zmodp]
+mem_mulsmx [in mathcomp.algebra.mxalgebra]
+mem_pblock [in mathcomp.ssreflect.finset]
+mem_imset2 [in mathcomp.ssreflect.finset]
+mem_imset [in mathcomp.ssreflect.finset]
+mem0mx [in mathcomp.algebra.mxalgebra]
+mem0v [in mathcomp.algebra.vector]
+mem0_itvoo_xNx [in mathcomp.algebra.interval]
+mem0_itvcc_xNx [in mathcomp.algebra.interval]
+mem1v [in mathcomp.field.fieldext]
+mem2l [in mathcomp.ssreflect.path]
+mem2lf [in mathcomp.ssreflect.path]
+mem2lr_splice [in mathcomp.ssreflect.path]
+mem2l_cat [in mathcomp.ssreflect.path]
+mem2r [in mathcomp.ssreflect.path]
+mem2rf [in mathcomp.ssreflect.path]
+mem2r_cat [in mathcomp.ssreflect.path]
+mem2_map [in mathcomp.ssreflect.path]
+mem2_last [in mathcomp.ssreflect.path]
+mem2_seq1 [in mathcomp.ssreflect.path]
+mem2_cons [in mathcomp.ssreflect.path]
+mem2_splice1 [in mathcomp.ssreflect.path]
+mem2_splice [in mathcomp.ssreflect.path]
+mem2_cat [in mathcomp.ssreflect.path]
+merge_uniq [in mathcomp.ssreflect.path]
+merge_sorted [in mathcomp.ssreflect.path]
+merge_path [in mathcomp.ssreflect.path]
+metacyclicP [in mathcomp.solvable.cyclic]
+metacyclicS [in mathcomp.solvable.cyclic]
+metacyclic_sol [in mathcomp.solvable.nilpotent]
+metacyclic1 [in mathcomp.solvable.cyclic]
+MhoE [in mathcomp.solvable.abelian]
+MhoEabelian [in mathcomp.solvable.abelian]
+MhoJ [in mathcomp.solvable.abelian]
+MhoS [in mathcomp.solvable.abelian]
+Mho_leq [in mathcomp.solvable.abelian]
+Mho_normal [in mathcomp.solvable.abelian]
+Mho_char [in mathcomp.solvable.abelian]
+Mho_dprod [in mathcomp.solvable.abelian]
+Mho_cprod [in mathcomp.solvable.abelian]
+Mho_p_cycle [in mathcomp.solvable.abelian]
+Mho_cont [in mathcomp.solvable.abelian]
+Mho_sub [in mathcomp.solvable.abelian]
+Mho_p_elt [in mathcomp.solvable.abelian]
+Mho0 [in mathcomp.solvable.abelian]
+Mho1 [in mathcomp.solvable.abelian]
+mid_in_itvcc [in mathcomp.algebra.interval]
+mid_in_itvoo [in mathcomp.algebra.interval]
+mid_in_itv [in mathcomp.algebra.interval]
+minCpolyP [in mathcomp.field.algC]
+minCpoly_aut [in mathcomp.field.algC]
+minCpoly_eq0 [in mathcomp.field.algC]
+minCpoly_monic [in mathcomp.field.algC]
+minCpoly_cyclotomic [in mathcomp.field.cyclotomic]
+mingroupp [in mathcomp.fingroup.fingroup]
+mingroupP [in mathcomp.fingroup.fingroup]
+mingroup_exists [in mathcomp.fingroup.fingroup]
+minKn [in mathcomp.ssreflect.ssrnat]
+minmaxset [in mathcomp.ssreflect.finset]
+minnA [in mathcomp.ssreflect.ssrnat]
+minnAC [in mathcomp.ssreflect.ssrnat]
+minnACA [in mathcomp.ssreflect.ssrnat]
+minnC [in mathcomp.ssreflect.ssrnat]
+minnCA [in mathcomp.ssreflect.ssrnat]
+minnE [in mathcomp.ssreflect.ssrnat]
+minnK [in mathcomp.ssreflect.ssrnat]
+minnn [in mathcomp.ssreflect.ssrnat]
+minnormal_maxnormal [in mathcomp.solvable.gseries]
+minnormal_exists [in mathcomp.solvable.gseries]
+minnormal_solvable [in mathcomp.solvable.maximal]
+minnormal_charsimple [in mathcomp.solvable.maximal]
+minnSS [in mathcomp.ssreflect.ssrnat]
+minn_mull [in mathcomp.ssreflect.ssrnat]
+minn_mulr [in mathcomp.ssreflect.ssrnat]
+minn_maxr [in mathcomp.ssreflect.ssrnat]
+minn_maxl [in mathcomp.ssreflect.ssrnat]
+minn_idPr [in mathcomp.ssreflect.ssrnat]
+minn_idPl [in mathcomp.ssreflect.ssrnat]
+minn0 [in mathcomp.ssreflect.ssrnat]
+minPolyOver [in mathcomp.field.fieldext]
+minPolyS [in mathcomp.field.fieldext]
+minPolyxx [in mathcomp.field.fieldext]
+minPoly_dvdp [in mathcomp.field.fieldext]
+minPoly_irr [in mathcomp.field.fieldext]
+minPoly_XsubC [in mathcomp.field.fieldext]
+minpoly_mx_ring [in mathcomp.algebra.mxpoly]
+minpoly_mxM [in mathcomp.algebra.mxpoly]
+minpoly_mx_free [in mathcomp.algebra.mxpoly]
+minpoly_mx1 [in mathcomp.algebra.mxpoly]
+minPoly_decidable_closure [in mathcomp.field.algebraics_fundamentals]
+minsetinf [in mathcomp.ssreflect.finset]
+minsetp [in mathcomp.ssreflect.finset]
+minsetP [in mathcomp.ssreflect.finset]
+minset_exists [in mathcomp.ssreflect.finset]
+minset_eq [in mathcomp.ssreflect.finset]
+minusE [in mathcomp.ssreflect.ssrnat]
+min_subfx_vectAxiom [in mathcomp.field.fieldext]
+min_card_extraspecial [in mathcomp.solvable.maximal]
+min0n [in mathcomp.ssreflect.ssrnat]
+misomP [in mathcomp.fingroup.morphism]
+misom_isog [in mathcomp.fingroup.morphism]
+mker [in mathcomp.fingroup.morphism]
+mkerl [in mathcomp.fingroup.morphism]
+mkerr [in mathcomp.fingroup.morphism]
+mkseq_uniq [in mathcomp.ssreflect.seq]
+mkseq_nth [in mathcomp.ssreflect.seq]
+modactE [in mathcomp.fingroup.action]
+modactEcond [in mathcomp.fingroup.action]
+modact_coset_astab [in mathcomp.fingroup.action]
+modact_is_groupAction [in mathcomp.fingroup.action]
+modact_faithful [in mathcomp.fingroup.action]
+modact_is_action [in mathcomp.fingroup.action]
+modgactE [in mathcomp.fingroup.action]
+modnDl [in mathcomp.ssreflect.div]
+modnDm [in mathcomp.ssreflect.div]
+modnDml [in mathcomp.ssreflect.div]
+modnDmr [in mathcomp.ssreflect.div]
+modnDr [in mathcomp.ssreflect.div]
+modnMDl [in mathcomp.ssreflect.div]
+modnMl [in mathcomp.ssreflect.div]
+modnMm [in mathcomp.ssreflect.div]
+modnMml [in mathcomp.ssreflect.div]
+modnMmr [in mathcomp.ssreflect.div]
+modnMr [in mathcomp.ssreflect.div]
+modnn [in mathcomp.ssreflect.div]
+modnXm [in mathcomp.ssreflect.div]
+modNz_nat [in mathcomp.algebra.intdiv]
+modn_summ [in mathcomp.ssreflect.binomial]
+modn_partP [in mathcomp.ssreflect.prime]
+modn_coprime [in mathcomp.ssreflect.div]
+modn_dvdm [in mathcomp.ssreflect.div]
+modn_mod [in mathcomp.ssreflect.div]
+modn_small [in mathcomp.ssreflect.div]
+modn_def [in mathcomp.ssreflect.div]
+modn0 [in mathcomp.ssreflect.div]
+modn1 [in mathcomp.ssreflect.div]
+modn2 [in mathcomp.ssreflect.div]
+modp_polyOver [in mathcomp.field.fieldext]
+modular_group_classP [in mathcomp.solvable.extremal]
+modular_group_structure [in mathcomp.solvable.extremal]
+module_baseAspace [in mathcomp.field.fieldext]
+module_baseVspace [in mathcomp.field.fieldext]
+modzDl [in mathcomp.algebra.intdiv]
+modzDm [in mathcomp.algebra.intdiv]
+modzDml [in mathcomp.algebra.intdiv]
+modzDmr [in mathcomp.algebra.intdiv]
+modzDr [in mathcomp.algebra.intdiv]
+modzMDl [in mathcomp.algebra.intdiv]
+modzMl [in mathcomp.algebra.intdiv]
+modzMm [in mathcomp.algebra.intdiv]
+modzMml [in mathcomp.algebra.intdiv]
+modzMmr [in mathcomp.algebra.intdiv]
+modzMr [in mathcomp.algebra.intdiv]
+modzN [in mathcomp.algebra.intdiv]
+modzNm [in mathcomp.algebra.intdiv]
+modZp [in mathcomp.algebra.zmodp]
+modzXm [in mathcomp.algebra.intdiv]
+modzz [in mathcomp.algebra.intdiv]
+modz_absm [in mathcomp.algebra.intdiv]
+modz_mod [in mathcomp.algebra.intdiv]
+modz_small [in mathcomp.algebra.intdiv]
+modz_ge0 [in mathcomp.algebra.intdiv]
+modz_nat [in mathcomp.algebra.intdiv]
+modz_abs [in mathcomp.algebra.intdiv]
+modz0 [in mathcomp.algebra.intdiv]
+modz1 [in mathcomp.algebra.intdiv]
+mod_Iirr_bij [in mathcomp.character.character]
+mod_IirrK [in mathcomp.character.character]
+mod_Iirr_eq0 [in mathcomp.character.character]
+mod_IirrE [in mathcomp.character.character]
+mod_Iirr0 [in mathcomp.character.character]
+mod0n [in mathcomp.ssreflect.div]
+mod0z [in mathcomp.algebra.intdiv]
+monicE [in mathcomp.algebra.poly]
+monicMl [in mathcomp.algebra.poly]
+monicMr [in mathcomp.algebra.poly]
+monicP [in mathcomp.algebra.poly]
+monicX [in mathcomp.algebra.poly]
+monicXn [in mathcomp.algebra.poly]
+monicXsubC [in mathcomp.algebra.poly]
+monic_minPoly [in mathcomp.field.fieldext]
+monic_map [in mathcomp.algebra.poly]
+monic_Xn_sub_1 [in mathcomp.algebra.poly]
+monic_comreg [in mathcomp.algebra.poly]
+monic_prod_XsubC [in mathcomp.algebra.poly]
+monic_prod [in mathcomp.algebra.poly]
+monic_exp [in mathcomp.algebra.poly]
+monic_mulr_closed [in mathcomp.algebra.poly]
+monic_neq0 [in mathcomp.algebra.poly]
+monic_key [in mathcomp.algebra.poly]
+monic1 [in mathcomp.algebra.poly]
+Monoid.mulC_dist [in mathcomp.ssreflect.bigop]
+Monoid.mulC_zero [in mathcomp.ssreflect.bigop]
+Monoid.mulC_id [in mathcomp.ssreflect.bigop]
+Monoid.Theory.addmA [in mathcomp.ssreflect.bigop]
+Monoid.Theory.addmAC [in mathcomp.ssreflect.bigop]
+Monoid.Theory.addmC [in mathcomp.ssreflect.bigop]
+Monoid.Theory.addmCA [in mathcomp.ssreflect.bigop]
+Monoid.Theory.addm0 [in mathcomp.ssreflect.bigop]
+Monoid.Theory.add0m [in mathcomp.ssreflect.bigop]
+Monoid.Theory.iteropE [in mathcomp.ssreflect.bigop]
+Monoid.Theory.mulmA [in mathcomp.ssreflect.bigop]
+Monoid.Theory.mulmAC [in mathcomp.ssreflect.bigop]
+Monoid.Theory.mulmACA [in mathcomp.ssreflect.bigop]
+Monoid.Theory.mulmC [in mathcomp.ssreflect.bigop]
+Monoid.Theory.mulmCA [in mathcomp.ssreflect.bigop]
+Monoid.Theory.mulm_addr [in mathcomp.ssreflect.bigop]
+Monoid.Theory.mulm_addl [in mathcomp.ssreflect.bigop]
+Monoid.Theory.mulm0 [in mathcomp.ssreflect.bigop]
+Monoid.Theory.mulm1 [in mathcomp.ssreflect.bigop]
+Monoid.Theory.mul0m [in mathcomp.ssreflect.bigop]
+Monoid.Theory.mul1m [in mathcomp.ssreflect.bigop]
+mono_leqif [in mathcomp.ssreflect.ssrnat]
+morphicP [in mathcomp.fingroup.morphism]
+morphic_aut [in mathcomp.fingroup.automorphism]
+morphimD [in mathcomp.fingroup.morphism]
+morphimDG [in mathcomp.fingroup.morphism]
+morphimD1 [in mathcomp.fingroup.morphism]
+morphimE [in mathcomp.fingroup.morphism]
+morphimEdom [in mathcomp.fingroup.morphism]
+morphimEsub [in mathcomp.fingroup.morphism]
+morphimF [in mathcomp.solvable.gfunctor]
+morphimGI [in mathcomp.fingroup.morphism]
+morphimGK [in mathcomp.fingroup.morphism]
+morphimI [in mathcomp.fingroup.morphism]
+morphimIdom [in mathcomp.fingroup.morphism]
+morphimIG [in mathcomp.fingroup.morphism]
+morphimIim [in mathcomp.fingroup.morphism]
+morphimJ [in mathcomp.fingroup.morphism]
+morphimK [in mathcomp.fingroup.morphism]
+morphimMl [in mathcomp.fingroup.morphism]
+morphimMr [in mathcomp.fingroup.morphism]
+morphimP [in mathcomp.fingroup.morphism]
+morphimR [in mathcomp.fingroup.morphism]
+morphimS [in mathcomp.fingroup.morphism]
+morphimSGK [in mathcomp.fingroup.morphism]
+morphimSK [in mathcomp.fingroup.morphism]
+morphimT [in mathcomp.fingroup.morphism]
+morphimU [in mathcomp.fingroup.morphism]
+morphimV [in mathcomp.fingroup.morphism]
+morphimY [in mathcomp.fingroup.morphism]
+morphim_pseries [in mathcomp.solvable.pgroup]
+morphim_pcore_mod [in mathcomp.solvable.pgroup]
+morphim_pcore [in mathcomp.solvable.pgroup]
+morphim_Sylow [in mathcomp.solvable.pgroup]
+morphim_p_group [in mathcomp.solvable.pgroup]
+morphim_pSylow [in mathcomp.solvable.pgroup]
+morphim_Hall [in mathcomp.solvable.pgroup]
+morphim_pHall [in mathcomp.solvable.pgroup]
+morphim_p_index [in mathcomp.solvable.pgroup]
+morphim_odd [in mathcomp.solvable.pgroup]
+morphim_pgroup [in mathcomp.solvable.pgroup]
+morphim_qisom_inj [in mathcomp.fingroup.quotient]
+morphim_qisom [in mathcomp.fingroup.quotient]
+morphim_quotm [in mathcomp.fingroup.quotient]
+morphim_mx_abs_irr [in mathcomp.character.mxrepresentation]
+morphim_mx_irr [in mathcomp.character.mxrepresentation]
+morphim_mx_repr [in mathcomp.character.mxrepresentation]
+morphim_mxE [in mathcomp.character.mxrepresentation]
+morphim_dprodmr [in mathcomp.fingroup.gproduct]
+morphim_dprodml [in mathcomp.fingroup.gproduct]
+morphim_dprodm [in mathcomp.fingroup.gproduct]
+morphim_cprodmr [in mathcomp.fingroup.gproduct]
+morphim_cprodml [in mathcomp.fingroup.gproduct]
+morphim_cprodm [in mathcomp.fingroup.gproduct]
+morphim_sdprodmr [in mathcomp.fingroup.gproduct]
+morphim_sdprodml [in mathcomp.fingroup.gproduct]
+morphim_sdprodm [in mathcomp.fingroup.gproduct]
+morphim_pprodmr [in mathcomp.fingroup.gproduct]
+morphim_pprodml [in mathcomp.fingroup.gproduct]
+morphim_pprodm [in mathcomp.fingroup.gproduct]
+morphim_sndX [in mathcomp.fingroup.gproduct]
+morphim_fstX [in mathcomp.fingroup.gproduct]
+morphim_pair1g [in mathcomp.fingroup.gproduct]
+morphim_pairg1 [in mathcomp.fingroup.gproduct]
+morphim_coprime_bigdprod [in mathcomp.fingroup.gproduct]
+morphim_bigcprod [in mathcomp.fingroup.gproduct]
+morphim_coprime_dprod [in mathcomp.fingroup.gproduct]
+morphim_cprod [in mathcomp.fingroup.gproduct]
+morphim_coprime_sdprod [in mathcomp.fingroup.gproduct]
+morphim_pprod [in mathcomp.fingroup.gproduct]
+morphim_conj [in mathcomp.fingroup.automorphism]
+morphim_fixP [in mathcomp.fingroup.automorphism]
+morphim_p_rank_abelian [in mathcomp.solvable.abelian]
+morphim_rank_abelian [in mathcomp.solvable.abelian]
+morphim_Ohm [in mathcomp.solvable.abelian]
+morphim_Mho [in mathcomp.solvable.abelian]
+morphim_grank [in mathcomp.solvable.abelian]
+morphim_pnElem [in mathcomp.solvable.abelian]
+morphim_pElem [in mathcomp.solvable.abelian]
+morphim_abelem [in mathcomp.solvable.abelian]
+morphim_Ldiv [in mathcomp.solvable.abelian]
+morphim_LdivT [in mathcomp.solvable.abelian]
+morphim_subnormal [in mathcomp.solvable.gseries]
+morphim_Fitting [in mathcomp.solvable.maximal]
+morphim_Phi [in mathcomp.solvable.maximal]
+morphim_actm [in mathcomp.fingroup.action]
+morphim_sol [in mathcomp.solvable.nilpotent]
+morphim_nil [in mathcomp.solvable.nilpotent]
+morphim_lcn [in mathcomp.solvable.nilpotent]
+morphim_ucn [in mathcomp.solvable.nilpotent]
+morphim_der [in mathcomp.solvable.commutator]
+morphim_homg [in mathcomp.fingroup.morphism]
+morphim_isom [in mathcomp.fingroup.morphism]
+morphim_ifactm [in mathcomp.fingroup.morphism]
+morphim_invmE [in mathcomp.fingroup.morphism]
+morphim_invm [in mathcomp.fingroup.morphism]
+morphim_factm [in mathcomp.fingroup.morphism]
+morphim_comp [in mathcomp.fingroup.morphism]
+morphim_trivm [in mathcomp.fingroup.morphism]
+morphim_restrm [in mathcomp.fingroup.morphism]
+morphim_idm [in mathcomp.fingroup.morphism]
+morphim_injm_eq1 [in mathcomp.fingroup.morphism]
+morphim_subnormG [in mathcomp.fingroup.morphism]
+morphim_normG [in mathcomp.fingroup.morphism]
+morphim_abelian [in mathcomp.fingroup.morphism]
+morphim_subcent [in mathcomp.fingroup.morphism]
+morphim_cents [in mathcomp.fingroup.morphism]
+morphim_cent [in mathcomp.fingroup.morphism]
+morphim_subcent1 [in mathcomp.fingroup.morphism]
+morphim_cent1s [in mathcomp.fingroup.morphism]
+morphim_cent1 [in mathcomp.fingroup.morphism]
+morphim_normal [in mathcomp.fingroup.morphism]
+morphim_subnorm [in mathcomp.fingroup.morphism]
+morphim_norms [in mathcomp.fingroup.morphism]
+morphim_norm [in mathcomp.fingroup.morphism]
+morphim_cycle [in mathcomp.fingroup.morphism]
+morphim_gen [in mathcomp.fingroup.morphism]
+morphim_inj [in mathcomp.fingroup.morphism]
+morphim_injG [in mathcomp.fingroup.morphism]
+morphim_ker [in mathcomp.fingroup.morphism]
+morphim_groupset [in mathcomp.fingroup.morphism]
+morphim_class [in mathcomp.fingroup.morphism]
+morphim_set1 [in mathcomp.fingroup.morphism]
+morphim_eq0 [in mathcomp.fingroup.morphism]
+morphim_setIpre [in mathcomp.fingroup.morphism]
+morphim_sub [in mathcomp.fingroup.morphism]
+morphim_center [in mathcomp.solvable.center]
+morphim_cyclic [in mathcomp.solvable.cyclic]
+morphim_Zgroup [in mathcomp.solvable.sylow]
+morphim0 [in mathcomp.fingroup.morphism]
+morphim1 [in mathcomp.fingroup.morphism]
+morphJ [in mathcomp.fingroup.morphism]
+morphM [in mathcomp.fingroup.morphism]
+morphmE [in mathcomp.fingroup.morphism]
+morphpreD [in mathcomp.fingroup.morphism]
+morphpreE [in mathcomp.fingroup.morphism]
+morphpreI [in mathcomp.fingroup.morphism]
+morphpreIdom [in mathcomp.fingroup.morphism]
+morphpreIim [in mathcomp.fingroup.morphism]
+morphpreJ [in mathcomp.fingroup.morphism]
+morphpreK [in mathcomp.fingroup.morphism]
+morphpreMl [in mathcomp.fingroup.morphism]
+morphpreMr [in mathcomp.fingroup.morphism]
+morphpreP [in mathcomp.fingroup.morphism]
+morphpreS [in mathcomp.fingroup.morphism]
+morphpreSK [in mathcomp.fingroup.morphism]
+morphpreT [in mathcomp.fingroup.morphism]
+morphpreU [in mathcomp.fingroup.morphism]
+morphpreV [in mathcomp.fingroup.morphism]
+morphpre_qisom [in mathcomp.fingroup.quotient]
+morphpre_quotm [in mathcomp.fingroup.quotient]
+morphpre_mx_abs_irr [in mathcomp.character.mxrepresentation]
+morphpre_mx_irr [in mathcomp.character.mxrepresentation]
+morphpre_mx_repr [in mathcomp.character.mxrepresentation]
+morphpre_maximal_eq [in mathcomp.solvable.gseries]
+morphpre_maximal [in mathcomp.solvable.gseries]
+morphpre_ifactm [in mathcomp.fingroup.morphism]
+morphpre_invm [in mathcomp.fingroup.morphism]
+morphpre_factm [in mathcomp.fingroup.morphism]
+morphpre_comp [in mathcomp.fingroup.morphism]
+morphpre_restrm [in mathcomp.fingroup.morphism]
+morphpre_idm [in mathcomp.fingroup.morphism]
+morphpre_subcent [in mathcomp.fingroup.morphism]
+morphpre_cents [in mathcomp.fingroup.morphism]
+morphpre_cent [in mathcomp.fingroup.morphism]
+morphpre_subcent1 [in mathcomp.fingroup.morphism]
+morphpre_cent1s [in mathcomp.fingroup.morphism]
+morphpre_cent1 [in mathcomp.fingroup.morphism]
+morphpre_subnorm [in mathcomp.fingroup.morphism]
+morphpre_normal [in mathcomp.fingroup.morphism]
+morphpre_norms [in mathcomp.fingroup.morphism]
+morphpre_norm [in mathcomp.fingroup.morphism]
+morphpre_gen [in mathcomp.fingroup.morphism]
+morphpre_inj [in mathcomp.fingroup.morphism]
+morphpre_proper [in mathcomp.fingroup.morphism]
+morphpre_set1 [in mathcomp.fingroup.morphism]
+morphpre_groupset [in mathcomp.fingroup.morphism]
+morphpre_sub [in mathcomp.fingroup.morphism]
+morphpre0 [in mathcomp.fingroup.morphism]
+morphR [in mathcomp.fingroup.morphism]
+morphV [in mathcomp.fingroup.morphism]
+morphX [in mathcomp.fingroup.morphism]
+morph_constt [in mathcomp.solvable.pgroup]
+morph_p_elt [in mathcomp.solvable.pgroup]
+morph_Iirr_eq0 [in mathcomp.character.character]
+morph_Iirr_inj [in mathcomp.character.character]
+morph_IirrE [in mathcomp.character.character]
+morph_Iirr0 [in mathcomp.character.character]
+morph_gact_irr [in mathcomp.fingroup.action]
+morph_gacent [in mathcomp.fingroup.action]
+morph_gastab [in mathcomp.fingroup.action]
+morph_gastabs [in mathcomp.fingroup.action]
+morph_afix [in mathcomp.fingroup.action]
+morph_astab [in mathcomp.fingroup.action]
+morph_astabs [in mathcomp.fingroup.action]
+morph_injm_eq1 [in mathcomp.fingroup.morphism]
+morph_dom_groupset [in mathcomp.fingroup.morphism]
+morph_prod [in mathcomp.fingroup.morphism]
+morph_generator [in mathcomp.solvable.cyclic]
+morph_order [in mathcomp.solvable.cyclic]
+morph1 [in mathcomp.fingroup.morphism]
+mpiE [in mathcomp.ssreflect.generic_quotient]
+mulfxA [in mathcomp.field.fieldext]
+mulfxC [in mathcomp.field.fieldext]
+mulfx_addl [in mathcomp.field.fieldext]
+mulgA [in mathcomp.fingroup.fingroup]
+mulgI [in mathcomp.fingroup.fingroup]
+mulGid [in mathcomp.fingroup.fingroup]
+mulGidPl [in mathcomp.fingroup.fingroup]
+mulGidPr [in mathcomp.fingroup.fingroup]
+mulgK [in mathcomp.fingroup.fingroup]
+mulgKV [in mathcomp.fingroup.fingroup]
+mulgmP [in mathcomp.fingroup.gproduct]
+mulGS [in mathcomp.fingroup.fingroup]
+mulgS [in mathcomp.fingroup.fingroup]
+mulGSgid [in mathcomp.fingroup.fingroup]
+mulGSid [in mathcomp.fingroup.fingroup]
+mulgSS [in mathcomp.fingroup.fingroup]
+mulGsubP [in mathcomp.fingroup.fingroup]
+mulgU [in mathcomp.fingroup.fingroup]
+mulgV [in mathcomp.fingroup.fingroup]
+mulg_normal_maximal [in mathcomp.solvable.gseries]
+mulg_exp_card_rcosets [in mathcomp.solvable.finmodule]
+mulg_nil [in mathcomp.solvable.nilpotent]
+mulG_sub [in mathcomp.fingroup.fingroup]
+mulG_subG [in mathcomp.fingroup.fingroup]
+mulG_subr [in mathcomp.fingroup.fingroup]
+mulG_subl [in mathcomp.fingroup.fingroup]
+mulg_set1 [in mathcomp.fingroup.fingroup]
+mulg_subr [in mathcomp.fingroup.fingroup]
+mulg_subl [in mathcomp.fingroup.fingroup]
+mulg0 [in mathcomp.fingroup.gproduct]
+mulg1 [in mathcomp.fingroup.fingroup]
+mulIg [in mathcomp.fingroup.fingroup]
+mulKg [in mathcomp.fingroup.fingroup]
+mulKmx [in mathcomp.algebra.matrix]
+mulKn [in mathcomp.ssreflect.div]
+mulKVg [in mathcomp.fingroup.fingroup]
+mulKVmx [in mathcomp.algebra.matrix]
+mulKz [in mathcomp.algebra.intdiv]
+mulmxA [in mathcomp.algebra.matrix]
+mulmxBl [in mathcomp.algebra.matrix]
+mulmxBr [in mathcomp.algebra.matrix]
+mulmxDl [in mathcomp.algebra.matrix]
+mulmxDr [in mathcomp.algebra.matrix]
+mulmxE [in mathcomp.algebra.matrix]
+mulmxK [in mathcomp.algebra.matrix]
+mulmxKpV [in mathcomp.algebra.mxalgebra]
+mulmxKV [in mathcomp.algebra.matrix]
+mulmxKV_ker [in mathcomp.algebra.mxalgebra]
+mulmxN [in mathcomp.algebra.matrix]
+mulmxnE [in mathcomp.algebra.matrix]
+mulmxr_is_linear [in mathcomp.algebra.matrix]
+mulmxV [in mathcomp.algebra.matrix]
+mulmx_is_scalable [in mathcomp.algebra.matrix]
+mulmx_block [in mathcomp.algebra.matrix]
+mulmx_diag [in mathcomp.algebra.matrix]
+mulmx_sum_row [in mathcomp.algebra.matrix]
+mulmx_sumr [in mathcomp.algebra.matrix]
+mulmx_suml [in mathcomp.algebra.matrix]
+mulmx_key [in mathcomp.algebra.matrix]
+mulmx_ker [in mathcomp.algebra.mxalgebra]
+mulmx_sub [in mathcomp.algebra.mxalgebra]
+mulmx_coker [in mathcomp.algebra.mxalgebra]
+mulmx_max_rank [in mathcomp.algebra.mxalgebra]
+mulmx_base [in mathcomp.algebra.mxalgebra]
+mulmx_ebase [in mathcomp.algebra.mxalgebra]
+mulmx0 [in mathcomp.algebra.matrix]
+mulmx0_rank_max [in mathcomp.algebra.mxalgebra]
+mulmx1 [in mathcomp.algebra.matrix]
+mulmx1C [in mathcomp.algebra.matrix]
+mulmx1_unit [in mathcomp.algebra.matrix]
+mulmx1_min [in mathcomp.algebra.matrix]
+mulmx1_min_rank [in mathcomp.algebra.mxalgebra]
+mulnA [in mathcomp.ssreflect.ssrnat]
+mulnAC [in mathcomp.ssreflect.ssrnat]
+mulnACA [in mathcomp.ssreflect.ssrnat]
+mulnb [in mathcomp.ssreflect.ssrnat]
+mulnbl [in mathcomp.ssreflect.ssrnat]
+mulnBl [in mathcomp.ssreflect.ssrnat]
+mulnbr [in mathcomp.ssreflect.ssrnat]
+mulnBr [in mathcomp.ssreflect.ssrnat]
+mulnC [in mathcomp.ssreflect.ssrnat]
+mulnCA [in mathcomp.ssreflect.ssrnat]
+mulnDl [in mathcomp.ssreflect.ssrnat]
+mulnDr [in mathcomp.ssreflect.ssrnat]
+mulnE [in mathcomp.ssreflect.ssrnat]
+mulnK [in mathcomp.ssreflect.div]
+mulNmx [in mathcomp.algebra.matrix]
+mulnn [in mathcomp.ssreflect.ssrnat]
+mulNrNz [in mathcomp.algebra.ssrint]
+mulNrz [in mathcomp.algebra.ssrint]
+mulnS [in mathcomp.ssreflect.ssrnat]
+mulnSr [in mathcomp.ssreflect.ssrnat]
+muln_lcml [in mathcomp.ssreflect.div]
+muln_lcmr [in mathcomp.ssreflect.div]
+muln_lcm_gcd [in mathcomp.ssreflect.div]
+muln_divCA_gcd [in mathcomp.ssreflect.div]
+muln_gcdl [in mathcomp.ssreflect.div]
+muln_gcdr [in mathcomp.ssreflect.div]
+muln_divCA [in mathcomp.ssreflect.div]
+muln_divA [in mathcomp.ssreflect.div]
+muln_modl [in mathcomp.ssreflect.div]
+muln_modr [in mathcomp.ssreflect.div]
+muln_cfunE [in mathcomp.character.classfun]
+muln_gt0 [in mathcomp.ssreflect.ssrnat]
+muln_eq1 [in mathcomp.ssreflect.ssrnat]
+muln_eq0 [in mathcomp.ssreflect.ssrnat]
+muln0 [in mathcomp.ssreflect.ssrnat]
+muln1 [in mathcomp.ssreflect.ssrnat]
+muln2 [in mathcomp.ssreflect.ssrnat]
+mulpz [in mathcomp.algebra.ssrint]
+mulqA [in mathcomp.algebra.rat]
+mulqC [in mathcomp.algebra.rat]
+mulq_addl [in mathcomp.algebra.rat]
+mulq_frac [in mathcomp.algebra.rat]
+mulq_subdefC [in mathcomp.algebra.rat]
+mulrbz [in mathcomp.algebra.ssrint]
+mulrIz [in mathcomp.algebra.ssrint]
+mulrNz [in mathcomp.algebra.ssrint]
+mulrN1z [in mathcomp.algebra.ssrint]
+mulrzA [in mathcomp.algebra.ssrint]
+mulrzAC [in mathcomp.algebra.ssrint]
+mulrzAl [in mathcomp.algebra.ssrint]
+mulrzAr [in mathcomp.algebra.ssrint]
+mulrzA_C [in mathcomp.algebra.ssrint]
+mulrzBl [in mathcomp.algebra.ssrint]
+mulrzBl_nat [in mathcomp.algebra.ssrint]
+mulrzBr [in mathcomp.algebra.ssrint]
+mulrzDl [in mathcomp.algebra.ssrint]
+mulrzDr [in mathcomp.algebra.ssrint]
+mulrzl [in mathcomp.algebra.ssrint]
+mulrzr [in mathcomp.algebra.ssrint]
+mulrzz [in mathcomp.algebra.ssrint]
+mulrz_neq0 [in mathcomp.algebra.ssrint]
+mulrz_eq0 [in mathcomp.algebra.ssrint]
+mulrz_le0_ge0 [in mathcomp.algebra.ssrint]
+mulrz_ge0_le0 [in mathcomp.algebra.ssrint]
+mulrz_le0 [in mathcomp.algebra.ssrint]
+mulrz_ge0 [in mathcomp.algebra.ssrint]
+mulrz_int [in mathcomp.algebra.ssrint]
+mulrz_suml [in mathcomp.algebra.ssrint]
+mulrz_sumr [in mathcomp.algebra.ssrint]
+mulrz_nat [in mathcomp.algebra.ssrint]
+mulr0z [in mathcomp.algebra.ssrint]
+mulr1z [in mathcomp.algebra.ssrint]
+mulr2z [in mathcomp.algebra.ssrint]
+mulSG [in mathcomp.fingroup.fingroup]
+mulSg [in mathcomp.fingroup.fingroup]
+mulSgGid [in mathcomp.fingroup.fingroup]
+mulSGid [in mathcomp.fingroup.fingroup]
+mulsgP [in mathcomp.fingroup.fingroup]
+mulsmxA [in mathcomp.algebra.mxalgebra]
+mulsmxP [in mathcomp.algebra.mxalgebra]
+mulsmxS [in mathcomp.algebra.mxalgebra]
+mulsmx_addr [in mathcomp.algebra.mxalgebra]
+mulsmx_addl [in mathcomp.algebra.mxalgebra]
+mulsmx_subP [in mathcomp.algebra.mxalgebra]
+mulsmx0 [in mathcomp.algebra.mxalgebra]
+mulSn [in mathcomp.ssreflect.ssrnat]
+mulSnr [in mathcomp.ssreflect.ssrnat]
+muls_eqmx [in mathcomp.algebra.mxalgebra]
+muls0mx [in mathcomp.algebra.mxalgebra]
+multE [in mathcomp.ssreflect.ssrnat]
+multiplicity_XsubC [in mathcomp.algebra.poly]
+mulUg [in mathcomp.fingroup.fingroup]
+mulVg [in mathcomp.fingroup.fingroup]
+mulVmx [in mathcomp.algebra.matrix]
+mulVq [in mathcomp.algebra.rat]
+mulzK [in mathcomp.algebra.intdiv]
+mulz_divCA_gcd [in mathcomp.algebra.intdiv]
+mulz_gcdl [in mathcomp.algebra.intdiv]
+mulz_gcdr [in mathcomp.algebra.intdiv]
+mulz_divCA [in mathcomp.algebra.intdiv]
+mulz_divA [in mathcomp.algebra.intdiv]
+mulz_modl [in mathcomp.algebra.intdiv]
+mulz_modr [in mathcomp.algebra.intdiv]
+mulz_Nsign_abs [in mathcomp.algebra.ssrint]
+mulz_sign_abs [in mathcomp.algebra.ssrint]
+mulz_sg_eqN1 [in mathcomp.algebra.ssrint]
+mulz_sg_eq1 [in mathcomp.algebra.ssrint]
+mulz_sg [in mathcomp.algebra.ssrint]
+mulz2 [in mathcomp.algebra.ssrint]
+mul_subdefA [in mathcomp.algebra.rat]
+mul_bin_left [in mathcomp.ssreflect.binomial]
+mul_bin_down [in mathcomp.ssreflect.binomial]
+mul_bin_diag [in mathcomp.ssreflect.binomial]
+mul_vchar [in mathcomp.character.vcharacter]
+mul_adj_mx [in mathcomp.algebra.matrix]
+mul_mx_adj [in mathcomp.algebra.matrix]
+mul_mx_scalar [in mathcomp.algebra.matrix]
+mul_vec_lin_row [in mathcomp.algebra.matrix]
+mul_vec_lin [in mathcomp.algebra.matrix]
+mul_rV_lin [in mathcomp.algebra.matrix]
+mul_rV_lin1 [in mathcomp.algebra.matrix]
+mul_block_col [in mathcomp.algebra.matrix]
+mul_row_block [in mathcomp.algebra.matrix]
+mul_col_row [in mathcomp.algebra.matrix]
+mul_row_col [in mathcomp.algebra.matrix]
+mul_col_mx [in mathcomp.algebra.matrix]
+mul_mx_row [in mathcomp.algebra.matrix]
+mul_pid_mx_copid [in mathcomp.algebra.matrix]
+mul_copid_mx_pid [in mathcomp.algebra.matrix]
+mul_pid_mx [in mathcomp.algebra.matrix]
+mul_xcol [in mathcomp.algebra.matrix]
+mul_row_perm [in mathcomp.algebra.matrix]
+mul_col_perm [in mathcomp.algebra.matrix]
+mul_scalar_mx [in mathcomp.algebra.matrix]
+mul_mx_diag [in mathcomp.algebra.matrix]
+mul_diag_mx [in mathcomp.algebra.matrix]
+mul_delta_mx_0 [in mathcomp.algebra.matrix]
+mul_delta_mx [in mathcomp.algebra.matrix]
+mul_delta_mx_cond [in mathcomp.algebra.matrix]
+mul_lin_irr [in mathcomp.character.character]
+mul_conjC_lin_char [in mathcomp.character.character]
+mul_char [in mathcomp.character.character]
+mul_card_Ohm_Mho_abelian [in mathcomp.solvable.abelian]
+mul_cfuni_on [in mathcomp.character.classfun]
+mul_cfuni [in mathcomp.character.classfun]
+mul_polyC [in mathcomp.algebra.poly]
+mul_lead_coef [in mathcomp.algebra.poly]
+mul_polyDr [in mathcomp.algebra.poly]
+mul_polyDl [in mathcomp.algebra.poly]
+mul_poly1 [in mathcomp.algebra.poly]
+mul_1poly [in mathcomp.algebra.poly]
+mul_polyA [in mathcomp.algebra.poly]
+mul_poly_key [in mathcomp.algebra.poly]
+mul_cardG [in mathcomp.fingroup.fingroup]
+mul_subG [in mathcomp.fingroup.fingroup]
+mul0g [in mathcomp.fingroup.gproduct]
+mul0mx [in mathcomp.algebra.matrix]
+mul0n [in mathcomp.ssreflect.ssrnat]
+mul0rz [in mathcomp.algebra.ssrint]
+mul1fx [in mathcomp.field.fieldext]
+mul1g [in mathcomp.fingroup.fingroup]
+mul1mx [in mathcomp.algebra.matrix]
+mul1n [in mathcomp.ssreflect.ssrnat]
+mul1q [in mathcomp.algebra.rat]
+mul2n [in mathcomp.ssreflect.ssrnat]
+mul2z [in mathcomp.algebra.ssrint]
+mxdirectE [in mathcomp.algebra.mxalgebra]
+mxdirectEgeq [in mathcomp.algebra.mxalgebra]
+mxdirectP [in mathcomp.algebra.mxalgebra]
+mxdirect_sums_center [in mathcomp.algebra.mxalgebra]
+mxdirect_adds_center [in mathcomp.algebra.mxalgebra]
+mxdirect_delta [in mathcomp.algebra.mxalgebra]
+mxdirect_sum_eigenspace [in mathcomp.algebra.mxalgebra]
+mxdirect_sumsE [in mathcomp.algebra.mxalgebra]
+mxdirect_sumsP [in mathcomp.algebra.mxalgebra]
+mxdirect_addsP [in mathcomp.algebra.mxalgebra]
+mxdirect_addsE [in mathcomp.algebra.mxalgebra]
+mxdirect_trivial [in mathcomp.algebra.mxalgebra]
+mxE [in mathcomp.algebra.matrix]
+mxminpoly_map [in mathcomp.algebra.mxpoly]
+mxminpoly_dvd_char [in mathcomp.algebra.mxpoly]
+mxminpoly_linear_is_scalar [in mathcomp.algebra.mxpoly]
+mxminpoly_min [in mathcomp.algebra.mxpoly]
+mxminpoly_monic [in mathcomp.algebra.mxpoly]
+mxminpoly_nonconstant [in mathcomp.algebra.mxpoly]
+mxmoduleP [in mathcomp.character.mxrepresentation]
+mxmodule_map [in mathcomp.character.mxrepresentation]
+mxmodule_form_qf [in mathcomp.character.mxrepresentation]
+mxmodule_quo [in mathcomp.character.mxrepresentation]
+mxmodule_conj [in mathcomp.character.mxrepresentation]
+mxmodule_morphim [in mathcomp.character.mxrepresentation]
+mxmodule_morphpre [in mathcomp.character.mxrepresentation]
+mxmodule_eqg [in mathcomp.character.mxrepresentation]
+mxmodule_subg [in mathcomp.character.mxrepresentation]
+mxmodule_envelop [in mathcomp.character.mxrepresentation]
+mxmodule_eigenvector [in mathcomp.character.mxrepresentation]
+mxmodule_trans [in mathcomp.character.mxrepresentation]
+mxmodule_abelem_subg [in mathcomp.character.mxabelem]
+mxmodule_abelemG [in mathcomp.character.mxabelem]
+mxmodule_abelem [in mathcomp.character.mxabelem]
+mxmodule0 [in mathcomp.character.mxrepresentation]
+mxmodule1 [in mathcomp.character.mxrepresentation]
+mxnonsimpleP [in mathcomp.character.mxrepresentation]
+mxrankE [in mathcomp.algebra.mxalgebra]
+mxrankMfree [in mathcomp.algebra.mxalgebra]
+mxrankM_maxr [in mathcomp.algebra.mxalgebra]
+mxrankM_maxl [in mathcomp.algebra.mxalgebra]
+mxrankS [in mathcomp.algebra.mxalgebra]
+mxrank_rsim [in mathcomp.character.mxrepresentation]
+mxrank_iso [in mathcomp.character.mxrepresentation]
+mxrank_in_factmod [in mathcomp.character.mxrepresentation]
+mxrank_in_submod [in mathcomp.character.mxrepresentation]
+mxrank_rowg [in mathcomp.character.mxabelem]
+mxrank_map [in mathcomp.algebra.mxalgebra]
+mxrank_sum_leqif [in mathcomp.algebra.mxalgebra]
+mxrank_adds_leqif [in mathcomp.algebra.mxalgebra]
+mxrank_sum_cap [in mathcomp.algebra.mxalgebra]
+mxrank_cap_compl [in mathcomp.algebra.mxalgebra]
+mxrank_disjoint_sum [in mathcomp.algebra.mxalgebra]
+mxrank_injP [in mathcomp.algebra.mxalgebra]
+mxrank_mul_ker [in mathcomp.algebra.mxalgebra]
+mxrank_mul_min [in mathcomp.algebra.mxalgebra]
+mxrank_Frobenius [in mathcomp.algebra.mxalgebra]
+mxrank_coker [in mathcomp.algebra.mxalgebra]
+mxrank_ker [in mathcomp.algebra.mxalgebra]
+mxrank_compl [in mathcomp.algebra.mxalgebra]
+mxrank_leqif_eq [in mathcomp.algebra.mxalgebra]
+mxrank_leqif_sup [in mathcomp.algebra.mxalgebra]
+mxrank_gen [in mathcomp.algebra.mxalgebra]
+mxrank_delta [in mathcomp.algebra.mxalgebra]
+mxrank_unit [in mathcomp.algebra.mxalgebra]
+mxrank_eq0 [in mathcomp.algebra.mxalgebra]
+mxrank_opp [in mathcomp.algebra.mxalgebra]
+mxrank_scale_nz [in mathcomp.algebra.mxalgebra]
+mxrank_scale [in mathcomp.algebra.mxalgebra]
+mxrank_add [in mathcomp.algebra.mxalgebra]
+mxrank_tr [in mathcomp.algebra.mxalgebra]
+mxrank0 [in mathcomp.algebra.mxalgebra]
+mxrank1 [in mathcomp.algebra.mxalgebra]
+mxring_id_uniq [in mathcomp.algebra.mxalgebra]
+mxring_idP [in mathcomp.algebra.mxalgebra]
+mxsemisimpleS [in mathcomp.character.mxrepresentation]
+mxsemisimple_reducible [in mathcomp.character.mxrepresentation]
+mxsemisimple_module [in mathcomp.character.mxrepresentation]
+mxsemisimple0 [in mathcomp.character.mxrepresentation]
+mxsimpleP [in mathcomp.character.mxrepresentation]
+mxsimple_map [in mathcomp.character.mxrepresentation]
+mxsimple_abelian_linear [in mathcomp.character.mxrepresentation]
+mxsimple_morphim [in mathcomp.character.mxrepresentation]
+mxsimple_eqg [in mathcomp.character.mxrepresentation]
+mxsimple_subg [in mathcomp.character.mxrepresentation]
+mxsimple_semisimple [in mathcomp.character.mxrepresentation]
+mxsimple_iso_simple [in mathcomp.character.mxrepresentation]
+mxsimple_isoP [in mathcomp.character.mxrepresentation]
+mxsimple_cyclic [in mathcomp.character.mxrepresentation]
+mxsimple_exists [in mathcomp.character.mxrepresentation]
+mxsimple_module [in mathcomp.character.mxrepresentation]
+mxsimple_abelem_subg [in mathcomp.character.mxabelem]
+mxsimple_abelemGP [in mathcomp.character.mxabelem]
+mxsimple_abelemP [in mathcomp.character.mxabelem]
+mxtraceD [in mathcomp.algebra.matrix]
+mxtraceZ [in mathcomp.algebra.matrix]
+mxtrace_regular [in mathcomp.character.mxrepresentation]
+mxtrace_Socle [in mathcomp.character.mxrepresentation]
+mxtrace_component [in mathcomp.character.mxrepresentation]
+mxtrace_dsum_mod [in mathcomp.character.mxrepresentation]
+mxtrace_dadd_mod [in mathcomp.character.mxrepresentation]
+mxtrace_submod1 [in mathcomp.character.mxrepresentation]
+mxtrace_rsim [in mathcomp.character.mxrepresentation]
+mxtrace_sub_fact_mod [in mathcomp.character.mxrepresentation]
+mxtrace_mulC [in mathcomp.algebra.matrix]
+mxtrace_block [in mathcomp.algebra.matrix]
+mxtrace_scalar [in mathcomp.algebra.matrix]
+mxtrace_diag [in mathcomp.algebra.matrix]
+mxtrace_is_scalar [in mathcomp.algebra.matrix]
+mxtrace_tr [in mathcomp.algebra.matrix]
+mxtrace_prod [in mathcomp.character.character]
+mxtrace0 [in mathcomp.algebra.matrix]
+mxtrace1 [in mathcomp.algebra.matrix]
+mxvecE [in mathcomp.algebra.matrix]
+mxvecK [in mathcomp.algebra.matrix]
+mxvec_dotmul [in mathcomp.algebra.matrix]
+mxvec_delta [in mathcomp.algebra.matrix]
+mxvec_eq0 [in mathcomp.algebra.matrix]
+mxvec_indexP [in mathcomp.algebra.matrix]
+mxvec_cast [in mathcomp.algebra.matrix]
+mx_irr_gring_op_center_scalar [in mathcomp.character.integral_char]
+mx_rsim_map [in mathcomp.character.mxrepresentation]
+mx_irr_map [in mathcomp.character.mxrepresentation]
+mx_JordanHolder_max [in mathcomp.character.mxrepresentation]
+mx_JordanHolder [in mathcomp.character.mxrepresentation]
+mx_JordanHolder_exists [in mathcomp.character.mxrepresentation]
+mx_butterfly [in mathcomp.character.mxrepresentation]
+mx_second_rsim [in mathcomp.character.mxrepresentation]
+mx_Schreier [in mathcomp.character.mxrepresentation]
+mx_series_rcons [in mathcomp.character.mxrepresentation]
+mx_series_repr_irr [in mathcomp.character.mxrepresentation]
+mx_series_lt [in mathcomp.character.mxrepresentation]
+mx_subseries_module' [in mathcomp.character.mxrepresentation]
+mx_subseries_module [in mathcomp.character.mxrepresentation]
+mx_factmod_sub [in mathcomp.character.mxrepresentation]
+mx_rsim_in_submod [in mathcomp.character.mxrepresentation]
+mx_rsim_scalar [in mathcomp.character.mxrepresentation]
+mx_rsim_factmod [in mathcomp.character.mxrepresentation]
+mx_rsim_faithful [in mathcomp.character.mxrepresentation]
+mx_rsim_abs_irr [in mathcomp.character.mxrepresentation]
+mx_rsim_irr [in mathcomp.character.mxrepresentation]
+mx_rsim_iso [in mathcomp.character.mxrepresentation]
+mx_rsim_def [in mathcomp.character.mxrepresentation]
+mx_rsim_trans [in mathcomp.character.mxrepresentation]
+mx_rsim_sym [in mathcomp.character.mxrepresentation]
+mx_rsim_refl [in mathcomp.character.mxrepresentation]
+mx_irr_abelian_linear [in mathcomp.character.mxrepresentation]
+mx_faithful_irr_abelian_cyclic [in mathcomp.character.mxrepresentation]
+mx_faithful_irr_center_cyclic [in mathcomp.character.mxrepresentation]
+mx_Jacobson_density [in mathcomp.character.mxrepresentation]
+mx_abs_irrW [in mathcomp.character.mxrepresentation]
+mx_abs_irr_cent_scalar [in mathcomp.character.mxrepresentation]
+mx_abs_irrP [in mathcomp.character.mxrepresentation]
+mx_Schur [in mathcomp.character.mxrepresentation]
+mx_irrP [in mathcomp.character.mxrepresentation]
+mx_iso_component [in mathcomp.character.mxrepresentation]
+mx_reducible_semisimple [in mathcomp.character.mxrepresentation]
+mx_Maschke [in mathcomp.character.mxrepresentation]
+mx_reducibleS [in mathcomp.character.mxrepresentation]
+mx_Schur_iso [in mathcomp.character.mxrepresentation]
+mx_Schur_inj_iso [in mathcomp.character.mxrepresentation]
+mx_Schur_inj [in mathcomp.character.mxrepresentation]
+mx_Schur_onto [in mathcomp.character.mxrepresentation]
+mx_iso_simple [in mathcomp.character.mxrepresentation]
+mx_iso_module [in mathcomp.character.mxrepresentation]
+mx_iso_trans [in mathcomp.character.mxrepresentation]
+mx_iso_sym [in mathcomp.character.mxrepresentation]
+mx_iso_refl [in mathcomp.character.mxrepresentation]
+mx_faithful_inj [in mathcomp.character.mxrepresentation]
+mx_vec_lin [in mathcomp.algebra.matrix]
+mx_rV_lin [in mathcomp.algebra.matrix]
+mx_root_minpoly [in mathcomp.algebra.mxpoly]
+mx_inv_hornerK [in mathcomp.algebra.mxpoly]
+mx_inv_horner0 [in mathcomp.algebra.mxpoly]
+mx_poly_ring_isom [in mathcomp.algebra.mxpoly]
+mx_rsim_standard [in mathcomp.character.character]
+mx_rsim_socle [in mathcomp.character.character]
+mx_rsim_dsum [in mathcomp.character.character]
+mx_rsim_dadd [in mathcomp.character.character]
+mx_repr0 [in mathcomp.character.character]
+mx_Fp_stable [in mathcomp.character.mxabelem]
+mx_Fp_abelem [in mathcomp.character.mxabelem]
+mx_group_homocyclic [in mathcomp.character.mxabelem]
+mx_repr_action_faithful [in mathcomp.character.mxabelem]
+mx_repr_is_groupAction [in mathcomp.character.mxabelem]
+mx_repr_is_action [in mathcomp.character.mxabelem]
+mx_repr_actE [in mathcomp.character.mxabelem]
+mx'_cast [in mathcomp.algebra.matrix]
+mx0_is_scalar [in mathcomp.algebra.matrix]
+mx1_sum_delta [in mathcomp.algebra.matrix]
+mx11_scalar [in mathcomp.algebra.matrix]
+
| 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 | +_ | +other | +(23233 entries) | +
| Notation 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 | +_ | +other | +(1373 entries) | +
| Module 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 | +_ | +other | +(213 entries) | +
| Variable 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 | +_ | +other | +(3475 entries) | +
| Library 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 | +_ | +other | +(89 entries) | +
| Lemma 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 | +_ | +other | +(11853 entries) | +
| Constructor 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 | +_ | +other | +(359 entries) | +
| Axiom 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 | +_ | +other | +(47 entries) | +
| Inductive 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 | +_ | +other | +(103 entries) | +
| Projection 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 | +_ | +other | +(266 entries) | +
| Section 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 | +_ | +other | +(1118 entries) | +
| Abbreviation 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 | +_ | +other | +(691 entries) | +
| Definition 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 | +_ | +other | +(3461 entries) | +
| Record 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 | +_ | +other | +(185 entries) | +