M (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 |
M (Lemmas)
mact_is_action [prf, in mathcomp.finite_group.action]mactE [prf, in mathcomp.finite_group.action]
make_separable [prf, in mathcomp.field.separable]
map2_0mx [prf, in mathcomp.algebra.matrix]
map2_1mx [prf, in mathcomp.algebra.matrix]
map2_block_mx [prf, in mathcomp.algebra.matrix]
map2_castmx [prf, in mathcomp.algebra.matrix]
map2_col [prf, in mathcomp.algebra.matrix]
map2_col' [prf, in mathcomp.algebra.matrix]
map2_col_mx [prf, in mathcomp.algebra.matrix]
map2_col_perm [prf, in mathcomp.algebra.matrix]
map2_conform_mx [prf, in mathcomp.algebra.matrix]
map2_const_mx [prf, in mathcomp.algebra.matrix]
map2_dlsubmx [prf, in mathcomp.algebra.matrix]
map2_drsubmx [prf, in mathcomp.algebra.matrix]
map2_dsubmx [prf, in mathcomp.algebra.matrix]
map2_lsubmx [prf, in mathcomp.algebra.matrix]
map2_mx0 [prf, in mathcomp.algebra.matrix]
map2_mx1 [prf, in mathcomp.algebra.matrix]
map2_mx_key [prf, in mathcomp.algebra.matrix]
map2_mx_left [prf, in mathcomp.algebra.matrix]
map2_mx_left_in [prf, in mathcomp.algebra.matrix]
map2_mx_right [prf, in mathcomp.algebra.matrix]
map2_mx_right_in [prf, in mathcomp.algebra.matrix]
map2_mxA [prf, in mathcomp.algebra.matrix]
map2_mxC [prf, in mathcomp.algebra.matrix]
map2_mxDl [prf, in mathcomp.algebra.matrix]
map2_mxDr [prf, in mathcomp.algebra.matrix]
map2_mxsub [prf, in mathcomp.algebra.matrix]
map2_mxvec [prf, in mathcomp.algebra.matrix]
map2_row [prf, in mathcomp.algebra.matrix]
map2_row' [prf, in mathcomp.algebra.matrix]
map2_row_mx [prf, in mathcomp.algebra.matrix]
map2_row_perm [prf, in mathcomp.algebra.matrix]
map2_rsubmx [prf, in mathcomp.algebra.matrix]
map2_trmx [prf, in mathcomp.algebra.matrix]
map2_ulsubmx [prf, in mathcomp.algebra.matrix]
map2_ursubmx [prf, in mathcomp.algebra.matrix]
map2_usubmx [prf, in mathcomp.algebra.matrix]
map2_vec_mx [prf, in mathcomp.algebra.matrix]
map2_xcol [prf, in mathcomp.algebra.matrix]
map2_xrow [prf, in mathcomp.algebra.matrix]
map_addsmx [prf, in mathcomp.algebra.mxalgebra]
map_allpairs [prf, in mathcomp.boot.seq]
map_block_mx [prf, in mathcomp.algebra.matrix]
map_bseqP [prf, in mathcomp.boot.tuple]
map_capmx [prf, in mathcomp.algebra.mxalgebra]
map_capmx_gen [prf, in mathcomp.algebra.mxalgebra]
map_castmx [prf, in mathcomp.algebra.matrix]
map_cat [prf, in mathcomp.boot.seq]
map_cent_mx [prf, in mathcomp.algebra.mxalgebra]
map_center_mx [prf, in mathcomp.algebra.mxalgebra]
map_cfAut_free [prf, in mathcomp.group_representation.classfun]
map_char_poly [prf, in mathcomp.algebra.mxpoly]
map_char_poly_mx [prf, in mathcomp.algebra.mxpoly]
map_cokermx [prf, in mathcomp.algebra.mxalgebra]
map_col [prf, in mathcomp.algebra.matrix]
map_col' [prf, in mathcomp.algebra.matrix]
map_col_base [prf, in mathcomp.algebra.mxalgebra]
map_col_ebase [prf, in mathcomp.algebra.mxalgebra]
map_col_mx [prf, in mathcomp.algebra.matrix]
map_col_perm [prf, in mathcomp.algebra.matrix]
map_comm_coef [prf, in mathcomp.algebra.poly]
map_comm_poly [prf, in mathcomp.algebra.poly]
map_comp [prf, in mathcomp.boot.seq]
map_comp_poly [prf, in mathcomp.algebra.poly]
map_complmx [prf, in mathcomp.algebra.mxalgebra]
map_conform_mx [prf, in mathcomp.algebra.matrix]
map_cons [prf, in mathcomp.boot.seq]
map_const_mx [prf, in mathcomp.algebra.matrix]
map_copid_mx [prf, in mathcomp.algebra.matrix]
map_delta_mx [prf, in mathcomp.algebra.matrix]
map_diag_mx [prf, in mathcomp.algebra.matrix]
map_diff_roots [prf, in mathcomp.algebra.poly]
map_diffmx [prf, in mathcomp.algebra.mxalgebra]
map_div_annihilantP [prf, in mathcomp.algebra.polyXY]
map_dlsubmx [prf, in mathcomp.algebra.matrix]
map_drop [prf, in mathcomp.boot.seq]
map_drsubmx [prf, in mathcomp.algebra.matrix]
map_dsubmx [prf, in mathcomp.algebra.matrix]
map_eigenspace [prf, in mathcomp.algebra.mxalgebra]
map_enveloping_algebra_mx [prf, in mathcomp.group_representation.mxrepresentation]
map_eqmx [prf, in mathcomp.algebra.mxalgebra]
map_f [prf, in mathcomp.boot.seq]
map_flatten [prf, in mathcomp.boot.seq]
map_fpoly_div_inj [prf, in mathcomp.field.qfpoly]
map_geigenspace [prf, in mathcomp.algebra.mxpoly]
map_genmx [prf, in mathcomp.algebra.mxalgebra]
map_gring_mx [prf, in mathcomp.group_representation.mxrepresentation]
map_gring_op [prf, in mathcomp.group_representation.mxrepresentation]
map_gring_proj [prf, in mathcomp.group_representation.mxrepresentation]
map_gring_row [prf, in mathcomp.group_representation.mxrepresentation]
map_group_ring [prf, in mathcomp.group_representation.mxrepresentation]
map_horner_mx [prf, in mathcomp.algebra.mxpoly]
map_id [prf, in mathcomp.boot.seq]
map_id_in [prf, in mathcomp.boot.seq]
map_inj_in_uniq [prf, in mathcomp.boot.seq]
map_inj_poly [prf, in mathcomp.algebra.poly]
map_inj_uniq [prf, in mathcomp.boot.seq]
map_invmx [prf, in mathcomp.algebra.matrix]
map_itv_bound_comp [prf, in mathcomp.algebra.interval_inference]
map_itv_comp [prf, in mathcomp.algebra.interval_inference]
map_kermx [prf, in mathcomp.algebra.mxalgebra]
map_kermxpoly [prf, in mathcomp.algebra.mxpoly]
map_lin1_mx [prf, in mathcomp.algebra.matrix]
map_lin_mx [prf, in mathcomp.algebra.matrix]
map_lsubmx [prf, in mathcomp.algebra.matrix]
map_ltmx [prf, in mathcomp.algebra.mxalgebra]
map_mask [prf, in mathcomp.boot.seq]
map_merge [prf, in mathcomp.boot.path]
map_minPoly [prf, in mathcomp.field.fieldext]
map_monic [prf, in mathcomp.algebra.poly]
map_mulsmx [prf, in mathcomp.algebra.mxalgebra]
map_mx0 [prf, in mathcomp.algebra.matrix]
map_mx1 [prf, in mathcomp.algebra.matrix]
map_mx_abs_irr [prf, in mathcomp.group_representation.mxrepresentation]
map_mx_adj [prf, in mathcomp.algebra.matrix]
map_mx_comp [prf, in mathcomp.algebra.matrix]
map_mx_companion [prf, in mathcomp.algebra.mxpoly]
map_mx_eq0 [prf, in mathcomp.algebra.matrix]
map_mx_faithful [prf, in mathcomp.group_representation.mxrepresentation]
map_mx_id [prf, in mathcomp.algebra.matrix]
map_mx_id_in [prf, in mathcomp.algebra.matrix]
map_mx_inj [prf, in mathcomp.algebra.matrix]
map_mx_inv [prf, in mathcomp.algebra.matrix]
map_mx_inv_horner [prf, in mathcomp.algebra.mxpoly]
map_mx_is_monoid_morphism [prf, in mathcomp.algebra.matrix]
map_mx_is_scalar [prf, in mathcomp.algebra.matrix]
map_mx_key [prf, in mathcomp.algebra.matrix]
map_mx_repr [prf, in mathcomp.group_representation.mxrepresentation]
map_mx_unit [prf, in mathcomp.algebra.matrix]
map_mxB [prf, in mathcomp.algebra.matrix]
map_mxCK [prf, in mathcomp.algebra.sesquilinear]
map_mxD [prf, in mathcomp.algebra.matrix]
map_mxM [prf, in mathcomp.algebra.matrix]
map_mxN [prf, in mathcomp.algebra.matrix]
map_mxsub [prf, in mathcomp.algebra.matrix]
map_mxvec [prf, in mathcomp.algebra.matrix]
map_mxZ [prf, in mathcomp.algebra.matrix]
map_nseq [prf, in mathcomp.boot.seq]
map_nth [prf, in mathcomp.boot.seq]
map_nth_iota [prf, in mathcomp.boot.seq]
map_nth_iota0 [prf, in mathcomp.boot.seq]
map_of_seq [prf, in mathcomp.boot.seq]
map_orthogonal [prf, in mathcomp.group_representation.classfun]
map_orthonormal [prf, in mathcomp.group_representation.vcharacter]
map_pairwise_orthogonal [prf, in mathcomp.group_representation.vcharacter]
map_path [prf, in mathcomp.boot.path]
map_perm_mx [prf, in mathcomp.algebra.matrix]
map_pid_mx [prf, in mathcomp.algebra.matrix]
map_pinvmx [prf, in mathcomp.algebra.mxalgebra]
map_pK [prf, in mathcomp.boot.seq]
map_Poly [prf, in mathcomp.algebra.poly]
map_poly0 [prf, in mathcomp.algebra.poly]
map_poly_com [prf, in mathcomp.algebra.poly]
map_poly_comp [prf, in mathcomp.algebra.poly]
map_poly_comp_id0 [prf, in mathcomp.algebra.poly]
map_poly_div_inj [prf, in mathcomp.field.qfpoly]
map_poly_divzK [prf, in mathcomp.algebra.intdiv]
map_poly_eq0 [prf, in mathcomp.algebra.poly]
map_poly_eq0_id0 [prf, in mathcomp.algebra.poly]
map_poly_id [prf, in mathcomp.algebra.poly]
map_Poly_id0 [prf, in mathcomp.algebra.poly]
map_poly_inj [prf, in mathcomp.algebra.poly]
map_poly_is_additive [prf, in mathcomp.algebra.poly]
map_poly_is_monoid_morphism [prf, in mathcomp.algebra.poly]
map_poly_is_nmod_morphism [prf, in mathcomp.algebra.poly]
map_poly_is_zmod_morphism [prf, in mathcomp.algebra.poly]
map_poly_rV [prf, in mathcomp.algebra.mxpoly]
map_polyC [prf, in mathcomp.algebra.poly]
map_polyC_eq0 [prf, in mathcomp.algebra.poly]
map_polyE [prf, in mathcomp.algebra.poly]
map_polyK [prf, in mathcomp.algebra.poly]
map_polyX [prf, in mathcomp.algebra.poly]
map_polyXaddC [prf, in mathcomp.algebra.poly]
map_polyXn [prf, in mathcomp.algebra.poly]
map_polyXsubC [prf, in mathcomp.algebra.poly]
map_polyZ [prf, in mathcomp.algebra.poly]
map_powers_mx [prf, in mathcomp.algebra.mxpoly]
map_preim [prf, in mathcomp.boot.fintype]
map_prod_XsubC [prf, in mathcomp.algebra.poly]
map_Qnum_poly [prf, in mathcomp.field.algnum]
map_rcons [prf, in mathcomp.boot.seq]
map_regular_mx [prf, in mathcomp.group_representation.mxrepresentation]
map_regular_repr [prf, in mathcomp.group_representation.mxrepresentation]
map_regular_subseries [prf, in mathcomp.group_representation.mxrepresentation]
map_reprE [prf, in mathcomp.group_representation.mxrepresentation]
map_reprJ [prf, in mathcomp.group_representation.mxrepresentation]
map_reshape [prf, in mathcomp.boot.seq]
map_resultant [prf, in mathcomp.algebra.mxpoly]
map_rev [prf, in mathcomp.boot.seq]
map_rfix_mx [prf, in mathcomp.group_representation.mxrepresentation]
map_rot [prf, in mathcomp.boot.seq]
map_rotr [prf, in mathcomp.boot.seq]
map_row [prf, in mathcomp.algebra.matrix]
map_row' [prf, in mathcomp.algebra.matrix]
map_row_base [prf, in mathcomp.algebra.mxalgebra]
map_row_ebase [prf, in mathcomp.algebra.mxalgebra]
map_row_mx [prf, in mathcomp.algebra.matrix]
map_row_perm [prf, in mathcomp.algebra.matrix]
map_rsubmx [prf, in mathcomp.algebra.matrix]
map_rVpoly [prf, in mathcomp.algebra.mxpoly]
map_scalar_mx [prf, in mathcomp.algebra.matrix]
map_section_repr [prf, in mathcomp.group_representation.mxrepresentation]
map_sort [prf, in mathcomp.boot.path]
map_sub_annihilantP [prf, in mathcomp.algebra.polyXY]
map_submx [prf, in mathcomp.algebra.mxalgebra]
map_subseq [prf, in mathcomp.boot.seq]
map_subset [prf, in mathcomp.boot.fintype]
map_take [prf, in mathcomp.boot.seq]
map_tnth_enum [prf, in mathcomp.boot.tuple]
map_tperm_mx [prf, in mathcomp.algebra.matrix]
map_trmx [prf, in mathcomp.algebra.matrix]
map_tupleP [prf, in mathcomp.boot.tuple]
map_ulsubmx [prf, in mathcomp.algebra.matrix]
map_uniq [prf, in mathcomp.boot.seq]
map_uniq_roots [prf, in mathcomp.algebra.poly]
map_unitmx [prf, in mathcomp.algebra.matrix]
map_ursubmx [prf, in mathcomp.algebra.matrix]
map_usubmx [prf, in mathcomp.algebra.matrix]
map_vec_mx [prf, in mathcomp.algebra.matrix]
map_xcol [prf, in mathcomp.algebra.matrix]
map_xrow [prf, in mathcomp.algebra.matrix]
mapf_root [prf, in mathcomp.algebra.poly]
mapK [prf, in mathcomp.boot.seq]
mapK_in [prf, in mathcomp.boot.seq]
mapP [prf, in mathcomp.boot.seq]
maptrmx_hermitian [prf, in mathcomp.algebra.sesquilinear]
maptrmx_sesqui [prf, in mathcomp.algebra.sesquilinear]
mask0 [prf, in mathcomp.boot.seq]
mask0s [prf, in mathcomp.boot.seq]
mask1 [prf, in mathcomp.boot.seq]
mask_cat [prf, in mathcomp.boot.seq]
mask_cons [prf, in mathcomp.boot.seq]
mask_enum_ord [prf, in mathcomp.boot.fintype]
mask_false [prf, in mathcomp.boot.seq]
mask_filter [prf, in mathcomp.boot.seq]
mask_nat_double [prf, in mathcomp.algebra.binnums]
mask_nat_double_pred [prf, in mathcomp.algebra.binnums]
mask_nat_succ_double [prf, in mathcomp.algebra.binnums]
mask_natB [prf, in mathcomp.algebra.binnums]
mask_rcons [prf, in mathcomp.boot.seq]
mask_rot [prf, in mathcomp.boot.seq]
mask_sort [prf, in mathcomp.boot.path]
mask_sort_in [prf, in mathcomp.boot.path]
mask_subseq [prf, in mathcomp.boot.seq]
mask_true [prf, in mathcomp.boot.seq]
mask_uniq [prf, in mathcomp.boot.seq]
matrix0Pn [prf, in mathcomp.algebra.matrix]
matrix_eq0 [prf, in mathcomp.algebra.matrix]
matrix_key [prf, in mathcomp.algebra.matrix]
matrix_modl [prf, in mathcomp.algebra.mxalgebra]
matrix_modr [prf, in mathcomp.algebra.mxalgebra]
matrix_nonzero1 [prf, in mathcomp.algebra.matrix]
matrix_of_formE [prf, in mathcomp.algebra.sesquilinear]
matrix_of_formK [prf, in mathcomp.algebra.sesquilinear]
matrix_of_tensorK [prf, in mathcomp.algebra.tensor]
matrix_sum_delta [prf, in mathcomp.algebra.matrix]
matrix_vect_iso [prf, in mathcomp.algebra.vector]
MatrixFormula.eval_col_mx [prf, in mathcomp.algebra.mxpoly]
MatrixFormula.eval_mulmx [prf, in mathcomp.algebra.mxpoly]
MatrixFormula.eval_mx_term [prf, in mathcomp.algebra.mxpoly]
MatrixFormula.eval_mxrank [prf, in mathcomp.algebra.mxpoly]
MatrixFormula.eval_mxvec [prf, in mathcomp.algebra.mxpoly]
MatrixFormula.eval_row_var [prf, in mathcomp.algebra.mxpoly]
MatrixFormula.eval_submx [prf, in mathcomp.algebra.mxpoly]
MatrixFormula.eval_vec_mx [prf, in mathcomp.algebra.mxpoly]
MatrixFormula.Exists_rowP [prf, in mathcomp.algebra.mxpoly]
MatrixFormula.mxrank_form_qf [prf, in mathcomp.algebra.mxpoly]
MatrixFormula.nth_row_env [prf, in mathcomp.algebra.mxpoly]
MatrixFormula.nth_seq_of_rV [prf, in mathcomp.algebra.mxpoly]
MatrixFormula.size_seq_of_rV [prf, in mathcomp.algebra.mxpoly]
MatrixFormula.submx_form_qf [prf, in mathcomp.algebra.mxpoly]
MatrixGenField.base_free [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.base_full [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.card_gen [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.eval_gen_term [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.eval_mulT [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.gen_add0r [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.gen_addA [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.gen_addC [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.gen_addNr [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.gen_dim_ex_proof [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.gen_dim_factor [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.gen_dim_gt0 [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.gen_dim_ub_proof [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.gen_invr0 [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.gen_is_monoid_morphism [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.gen_is_zmod_morphism [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.gen_mul1r [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.gen_mulA [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.gen_mulC [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.gen_mulDr [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.gen_mulVr [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.gen_mx_faithful [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.gen_mx_irr [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.gen_mx_repr [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.gen_ntriv [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.gen_satP [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.genK [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.in_gen0 [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.in_gen_row [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.in_genD [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.in_genJ [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.in_genK [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.in_genN [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.in_genZ [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.map_mxminpoly_groot [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.mxmodule_rowval_gen [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.mxval0 [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.mxval1 [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.mxval_centg [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.mxval_gen1 [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.mxval_genM [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.mxval_genV [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.mxval_groot [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.mxval_grootXn [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.mxval_inj [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.mxval_is_monoid_morphism [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.mxval_is_zmod_morphism [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.mxvalD [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.mxvalM [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.mxvalN [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.mxvalV [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.non_linear_gen_reducible [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.nth_map_rVval [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.rfix_gen [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.rker_gen [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.row_gen_sum_mxval [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.rowval_gen_stable [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.rowval_genK [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.rstab_in_gen [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.rstabs_in_gen [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.rstabs_rowval_gen [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.sat_gen_form [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.set_nth_map_rVval [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.submx_in_gen [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.submx_in_gen_eq [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.submx_rowval_gen [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.val_gen0 [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.val_gen_row [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.val_gen_rV [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.val_genD [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.val_genJ [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.val_genK [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.val_genN [prf, in mathcomp.group_representation.mxrepresentation]
MatrixGenField.val_genZ [prf, in mathcomp.group_representation.mxrepresentation]
matrixP [prf, in mathcomp.algebra.matrix]
max0n [prf, in mathcomp.boot.ssrnat]
max_card [prf, in mathcomp.boot.fintype]
max_card_abelian [prf, in mathcomp.solvable.abelian]
max_cfRepr_mx1 [prf, in mathcomp.group_representation.character]
max_cfRepr_norm_scalar [prf, in mathcomp.group_representation.character]
max_pdiv_dvd [prf, in mathcomp.boot.prime]
max_pdiv_gt0 [prf, in mathcomp.boot.prime]
max_pdiv_leq [prf, in mathcomp.boot.prime]
max_pdiv_max [prf, in mathcomp.boot.prime]
max_pdiv_prime [prf, in mathcomp.boot.prime]
max_pgroup_Sylow [prf, in mathcomp.solvable.sylow]
max_pgroupJ [prf, in mathcomp.solvable.pgroup]
max_poly_roots [prf, in mathcomp.algebra.poly]
max_ring_poly_roots [prf, in mathcomp.algebra.poly]
max_SCN [prf, in mathcomp.solvable.maximal]
max_size_coefXY [prf, in mathcomp.algebra.polyXY]
max_size_evalC [prf, in mathcomp.algebra.polyXY]
max_size_evalX [prf, in mathcomp.algebra.polyXY]
max_size_lead_coefXY [prf, in mathcomp.algebra.polyXY]
max_size_mx_series [prf, in mathcomp.group_representation.mxrepresentation]
max_submod_eqmx [prf, in mathcomp.group_representation.mxrepresentation]
max_submodP [prf, in mathcomp.group_representation.mxrepresentation]
max_unity_roots [prf, in mathcomp.algebra.poly]
maxainv_ainvar [prf, in mathcomp.solvable.jordanholder]
maxainv_asimple_quo [prf, in mathcomp.solvable.jordanholder]
maxainv_exists [prf, in mathcomp.solvable.jordanholder]
maxainv_norm [prf, in mathcomp.solvable.jordanholder]
maxainv_proper [prf, in mathcomp.solvable.jordanholder]
maxainv_sub [prf, in mathcomp.solvable.jordanholder]
maxainvM [prf, in mathcomp.solvable.jordanholder]
maxainvS [prf, in mathcomp.solvable.jordanholder]
maxgroup_exists [prf, in mathcomp.finite_group.fingroup]
maxgroupp [prf, in mathcomp.finite_group.fingroup]
maxgroupP [prf, in mathcomp.finite_group.fingroup]
maximal_cycle_extremal [prf, in mathcomp.solvable.extremal]
maximal_eqJ [prf, in mathcomp.solvable.gseries]
maximal_eqP [prf, in mathcomp.solvable.gseries]
maximal_exists [prf, in mathcomp.solvable.gseries]
maximalJ [prf, in mathcomp.solvable.gseries]
maxKn [prf, in mathcomp.boot.ssrnat]
maxminset [prf, in mathcomp.boot.finset]
maxn0 [prf, in mathcomp.boot.ssrnat]
maxn_idPl [prf, in mathcomp.boot.ssrnat]
maxn_idPr [prf, in mathcomp.boot.ssrnat]
maxn_minl [prf, in mathcomp.boot.ssrnat]
maxn_minr [prf, in mathcomp.boot.ssrnat]
maxnA [prf, in mathcomp.boot.ssrnat]
maxnAC [prf, in mathcomp.boot.ssrnat]
maxnACA [prf, in mathcomp.boot.ssrnat]
maxnC [prf, in mathcomp.boot.ssrnat]
maxnCA [prf, in mathcomp.boot.ssrnat]
maxnE [prf, in mathcomp.boot.ssrnat]
maxnK [prf, in mathcomp.boot.ssrnat]
maxnMl [prf, in mathcomp.boot.ssrnat]
maxnMr [prf, in mathcomp.boot.ssrnat]
maxnn [prf, in mathcomp.boot.ssrnat]
maxnormal_charsimple [prf, in mathcomp.solvable.maximal]
maxnormal_minnormal [prf, in mathcomp.solvable.gseries]
maxnormal_normal [prf, in mathcomp.solvable.gseries]
maxnormal_proper [prf, in mathcomp.solvable.gseries]
maxnormal_sub [prf, in mathcomp.solvable.gseries]
maxnormalM [prf, in mathcomp.solvable.gseries]
maxnSS [prf, in mathcomp.boot.ssrnat]
maxr_rat [prf, in mathcomp.algebra.rat]
maxrankfun_inj [prf, in mathcomp.algebra.mxalgebra]
maxrowsub_free [prf, in mathcomp.algebra.mxalgebra]
maxrowsub_full [prf, in mathcomp.algebra.mxalgebra]
maxset_cofix [prf, in mathcomp.boot.finset]
maxset_eq [prf, in mathcomp.boot.finset]
maxset_exists [prf, in mathcomp.boot.finset]
maxset_key [prf, in mathcomp.boot.finset]
maxsetp [prf, in mathcomp.boot.finset]
maxsetP [prf, in mathcomp.boot.finset]
maxsetsup [prf, in mathcomp.boot.finset]
meet_center_nil [prf, in mathcomp.solvable.nilpotent]
meet_Ohm1 [prf, in mathcomp.solvable.abelian]
mem0mx [prf, in mathcomp.algebra.mxalgebra]
mem0v [prf, in mathcomp.algebra.vector]
mem1v [prf, in mathcomp.field.fieldext]
mem2_cat [prf, in mathcomp.boot.path]
mem2_cons [prf, in mathcomp.boot.path]
mem2_last [prf, in mathcomp.boot.path]
mem2_map [prf, in mathcomp.boot.path]
mem2_seq1 [prf, in mathcomp.boot.path]
mem2_sort [prf, in mathcomp.boot.path]
mem2_sort_in [prf, in mathcomp.boot.path]
mem2_splice [prf, in mathcomp.boot.path]
mem2_splice1 [prf, in mathcomp.boot.path]
mem2E [prf, in mathcomp.boot.path]
mem2l [prf, in mathcomp.boot.path]
mem2l_cat [prf, in mathcomp.boot.path]
mem2lf [prf, in mathcomp.boot.path]
mem2lr_splice [prf, in mathcomp.boot.path]
mem2r [prf, in mathcomp.boot.path]
mem2r_cat [prf, in mathcomp.boot.path]
mem2rf [prf, in mathcomp.boot.path]
mem_allpairs [prf, in mathcomp.boot.seq]
mem_allpairs_catr [prf, in mathcomp.boot.seq]
mem_allpairs_consr [prf, in mathcomp.boot.seq]
mem_allpairs_dep [prf, in mathcomp.boot.seq]
mem_allpairs_rconsr [prf, in mathcomp.boot.seq]
mem_aspaceOver [prf, in mathcomp.field.fieldext]
mem_baseVspace [prf, in mathcomp.field.fieldext]
mem_behead [prf, in mathcomp.boot.seq]
mem_belast [prf, in mathcomp.boot.seq]
mem_bigdprod [prf, in mathcomp.finite_group.gproduct]
mem_card1 [prf, in mathcomp.boot.fintype]
mem_cat [prf, in mathcomp.boot.seq]
mem_catC [prf, in mathcomp.boot.seq]
mem_Cint_span [prf, in mathcomp.field.algnum]
mem_class_support [prf, in mathcomp.finite_group.fingroup]
mem_classes [prf, in mathcomp.finite_group.fingroup]
mem_closure [prf, in mathcomp.boot.fingraph]
mem_commg [prf, in mathcomp.finite_group.fingroup]
mem_conjg [prf, in mathcomp.finite_group.fingroup]
mem_conjgV [prf, in mathcomp.finite_group.fingroup]
mem_Crat_span [prf, in mathcomp.field.algnum]
mem_cycle [prf, in mathcomp.finite_group.fingroup]
mem_divgr [prf, in mathcomp.finite_group.gproduct]
mem_dprod [prf, in mathcomp.finite_group.gproduct]
mem_drop [prf, in mathcomp.boot.seq]
mem_enum [prf, in mathcomp.boot.fintype]
mem_fcycle [prf, in mathcomp.boot.path]
mem_filter [prf, in mathcomp.boot.seq]
mem_fixedFieldP [prf, in mathcomp.field.galois]
mem_galNorm [prf, in mathcomp.field.galois]
mem_galTrace [prf, in mathcomp.field.galois]
mem_gen [prf, in mathcomp.finite_group.fingroup]
mem_gring_mx [prf, in mathcomp.group_representation.mxrepresentation]
mem_Hall_pcore [prf, in mathcomp.solvable.pgroup]
mem_head [prf, in mathcomp.boot.seq]
mem_iinv [prf, in mathcomp.boot.fintype]
mem_im_abelem_rV [prf, in mathcomp.group_representation.mxabelem]
mem_image [prf, in mathcomp.boot.fintype]
mem_imset [prf, in mathcomp.boot.finset]
mem_imset2 [prf, in mathcomp.boot.finset]
mem_index_enum [prf, in mathcomp.boot.bigop]
mem_index_iota [prf, in mathcomp.boot.bigop]
mem_infix [prf, in mathcomp.boot.seq]
mem_invg [prf, in mathcomp.finite_group.fingroup]
mem_iota [prf, in mathcomp.boot.seq]
mem_irr [prf, in mathcomp.group_representation.character]
mem_last [prf, in mathcomp.boot.seq]
mem_lcoset [prf, in mathcomp.finite_group.fingroup]
mem_lcosets [prf, in mathcomp.finite_group.fingroup]
mem_map [prf, in mathcomp.boot.seq]
mem_mask [prf, in mathcomp.boot.seq]
mem_mask_cons [prf, in mathcomp.boot.seq]
mem_mask_rot [prf, in mathcomp.boot.seq]
mem_merge [prf, in mathcomp.boot.path]
mem_morphim [prf, in mathcomp.finite_group.morphism]
mem_morphpre [prf, in mathcomp.finite_group.morphism]
mem_mulg [prf, in mathcomp.finite_group.fingroup]
mem_mulsmx [prf, in mathcomp.algebra.mxalgebra]
mem_next [prf, in mathcomp.boot.path]
mem_normal_Hall [prf, in mathcomp.solvable.pgroup]
mem_npoly_enum [prf, in mathcomp.algebra.qpoly]
mem_nseq [prf, in mathcomp.boot.seq]
mem_nth [prf, in mathcomp.boot.seq]
mem_nthE [prf, in mathcomp.boot.seq]
mem_orbit [prf, in mathcomp.finite_group.action]
mem_orbit [prf, in mathcomp.boot.fingraph]
mem_ord_enum [prf, in mathcomp.boot.fintype]
mem_orthov1 [prf, in mathcomp.algebra.sesquilinear]
mem_orthov1_sym [prf, in mathcomp.algebra.sesquilinear]
mem_orthov_sym [prf, in mathcomp.algebra.sesquilinear]
mem_orthovP [prf, in mathcomp.algebra.sesquilinear]
mem_orthovPn [prf, in mathcomp.algebra.sesquilinear]
mem_p_elt [prf, in mathcomp.solvable.pgroup]
mem_pblock [prf, in mathcomp.boot.finset]
mem_permutations [prf, in mathcomp.boot.seq]
mem_pmap [prf, in mathcomp.boot.seq]
mem_pmap_sub [prf, in mathcomp.boot.seq]
mem_porbit [prf, in mathcomp.finite_group.perm]
mem_prev [prf, in mathcomp.boot.path]
mem_prime_decomp [prf, in mathcomp.boot.prime]
mem_primes [prf, in mathcomp.boot.prime]
mem_prodg [prf, in mathcomp.finite_group.fingroup]
mem_quotient [prf, in mathcomp.finite_group.quotient]
mem_rcons [prf, in mathcomp.boot.seq]
mem_rcoset [prf, in mathcomp.finite_group.fingroup]
mem_rcosets [prf, in mathcomp.finite_group.fingroup]
mem_rem [prf, in mathcomp.boot.seq]
mem_rem_uniq [prf, in mathcomp.boot.seq]
mem_rem_uniqF [prf, in mathcomp.boot.seq]
mem_remgr [prf, in mathcomp.finite_group.gproduct]
mem_repr [prf, in mathcomp.finite_group.fingroup]
mem_repr_classes [prf, in mathcomp.finite_group.fingroup]
mem_repr_coset [prf, in mathcomp.finite_group.quotient]
mem_repr_rcoset [prf, in mathcomp.finite_group.fingroup]
mem_rev [prf, in mathcomp.boot.seq]
mem_root [prf, in mathcomp.algebra.poly]
mem_rot [prf, in mathcomp.boot.seq]
mem_rotr [prf, in mathcomp.boot.seq]
mem_rowg [prf, in mathcomp.group_representation.mxabelem]
mem_rVabelem [prf, in mathcomp.group_representation.mxabelem]
mem_sdprod [prf, in mathcomp.finite_group.gproduct]
mem_seq1 [prf, in mathcomp.boot.seq]
mem_seq2 [prf, in mathcomp.boot.seq]
mem_seq3 [prf, in mathcomp.boot.seq]
mem_seq4 [prf, in mathcomp.boot.seq]
mem_seq_sub_enum [prf, in mathcomp.boot.fintype]
mem_setact [prf, in mathcomp.finite_group.action]
mem_sort [prf, in mathcomp.boot.path]
mem_sub_gring [prf, in mathcomp.group_representation.mxrepresentation]
mem_subseq [prf, in mathcomp.boot.seq]
mem_sum_enum [prf, in mathcomp.boot.fintype]
mem_take [prf, in mathcomp.boot.seq]
mem_tnth [prf, in mathcomp.boot.tuple]
mem_undup [prf, in mathcomp.boot.seq]
mem_unity_roots [prf, in mathcomp.algebra.poly]
mem_vspaceOver [prf, in mathcomp.field.fieldext]
mem_zchar [prf, in mathcomp.group_representation.vcharacter]
mem_zchar_on [prf, in mathcomp.group_representation.vcharacter]
mem_Zp [prf, in mathcomp.algebra.zmodp]
membsE [prf, in mathcomp.boot.tuple]
memJ_class [prf, in mathcomp.finite_group.fingroup]
memJ_class_support [prf, in mathcomp.finite_group.fingroup]
memJ_conjg [prf, in mathcomp.finite_group.fingroup]
memJ_norm [prf, in mathcomp.finite_group.fingroup]
memmx0 [prf, in mathcomp.algebra.mxalgebra]
memmx1 [prf, in mathcomp.algebra.mxalgebra]
memmx_addsP [prf, in mathcomp.algebra.mxalgebra]
memmx_cent_envelop [prf, in mathcomp.group_representation.mxrepresentation]
memmx_eqP [prf, in mathcomp.algebra.mxalgebra]
memmx_map [prf, in mathcomp.algebra.mxalgebra]
memmx_subP [prf, in mathcomp.algebra.mxalgebra]
memmx_sumsP [prf, in mathcomp.algebra.mxalgebra]
memNindex [prf, in mathcomp.boot.seq]
memPn [prf, in mathcomp.boot.eqtype]
memPnC [prf, in mathcomp.boot.eqtype]
mempx_Fadjoin [prf, in mathcomp.field.fieldext]
memt_nth [prf, in mathcomp.boot.tuple]
memtE [prf, in mathcomp.boot.tuple]
memv0 [prf, in mathcomp.algebra.vector]
memv_add [prf, in mathcomp.algebra.vector]
memv_addP [prf, in mathcomp.algebra.vector]
memv_adjoin [prf, in mathcomp.field.falgebra]
memv_algid [prf, in mathcomp.field.falgebra]
memv_cap [prf, in mathcomp.algebra.vector]
memv_capP [prf, in mathcomp.algebra.vector]
memv_cosetP [prf, in mathcomp.field.falgebra]
memv_gal [prf, in mathcomp.field.galois]
memv_img [prf, in mathcomp.algebra.vector]
memv_imgP [prf, in mathcomp.algebra.vector]
memV_invg [prf, in mathcomp.finite_group.fingroup]
memv_ker [prf, in mathcomp.algebra.vector]
memV_lcosetV [prf, in mathcomp.finite_group.fingroup]
memv_line [prf, in mathcomp.algebra.vector]
memv_mul [prf, in mathcomp.field.falgebra]
memv_pi [prf, in mathcomp.algebra.vector]
memv_pi1 [prf, in mathcomp.algebra.vector]
memv_pi2 [prf, in mathcomp.algebra.vector]
memv_pick [prf, in mathcomp.algebra.vector]
memv_preim [prf, in mathcomp.algebra.vector]
memv_proj [prf, in mathcomp.algebra.vector]
memv_projC [prf, in mathcomp.algebra.vector]
memV_rcosetV [prf, in mathcomp.finite_group.fingroup]
memv_span [prf, in mathcomp.algebra.vector]
memv_span1 [prf, in mathcomp.algebra.vector]
memv_submod_closed [prf, in mathcomp.algebra.vector]
memv_sum_pi [prf, in mathcomp.algebra.vector]
memv_suml [prf, in mathcomp.algebra.vector]
memv_sumP [prf, in mathcomp.algebra.vector]
memv_sumr [prf, in mathcomp.algebra.vector]
memvB [prf, in mathcomp.algebra.vector]
memvD [prf, in mathcomp.algebra.vector]
memvE [prf, in mathcomp.algebra.vector]
memvf [prf, in mathcomp.algebra.vector]
memvM [prf, in mathcomp.field.falgebra]
memvN [prf, in mathcomp.algebra.vector]
memvV [prf, in mathcomp.field.falgebra]
memvZ [prf, in mathcomp.algebra.vector]
merge_map [prf, in mathcomp.boot.path]
merge_path [prf, in mathcomp.boot.path]
merge_sorted [prf, in mathcomp.boot.path]
merge_stable_path [prf, in mathcomp.boot.path]
merge_stable_sorted [prf, in mathcomp.boot.path]
merge_uniq [prf, in mathcomp.boot.path]
mergeA [prf, in mathcomp.boot.path]
metacyclic1 [prf, in mathcomp.solvable.cyclic]
metacyclic_sol [prf, in mathcomp.solvable.nilpotent]
metacyclicP [prf, in mathcomp.solvable.cyclic]
metacyclicS [prf, in mathcomp.solvable.cyclic]
Mho0 [prf, in mathcomp.solvable.abelian]
Mho1 [prf, in mathcomp.solvable.abelian]
Mho_char [prf, in mathcomp.solvable.abelian]
Mho_cont [prf, in mathcomp.solvable.abelian]
Mho_cprod [prf, in mathcomp.solvable.abelian]
Mho_dprod [prf, in mathcomp.solvable.abelian]
Mho_leq [prf, in mathcomp.solvable.abelian]
Mho_normal [prf, in mathcomp.solvable.abelian]
Mho_p_cycle [prf, in mathcomp.solvable.abelian]
Mho_p_elt [prf, in mathcomp.solvable.abelian]
Mho_sub [prf, in mathcomp.solvable.abelian]
MhoE [prf, in mathcomp.solvable.abelian]
MhoEabelian [prf, in mathcomp.solvable.abelian]
MhoJ [prf, in mathcomp.solvable.abelian]
MhoS [prf, in mathcomp.solvable.abelian]
min0n [prf, in mathcomp.boot.ssrnat]
min_card_extraspecial [prf, in mathcomp.solvable.maximal]
min_subfx_vect [prf, in mathcomp.field.fieldext]
minCpoly_aut [prf, in mathcomp.field.algC]
minCpoly_cyclotomic [prf, in mathcomp.field.cyclotomic]
minCpoly_eq0 [prf, in mathcomp.field.algC]
minCpoly_monic [prf, in mathcomp.field.algC]
minCpolyP [prf, in mathcomp.field.algC]
mingroup_exists [prf, in mathcomp.finite_group.fingroup]
mingroupp [prf, in mathcomp.finite_group.fingroup]
mingroupP [prf, in mathcomp.finite_group.fingroup]
minKn [prf, in mathcomp.boot.ssrnat]
minmaxset [prf, in mathcomp.boot.finset]
minn0 [prf, in mathcomp.boot.ssrnat]
minn_idPl [prf, in mathcomp.boot.ssrnat]
minn_idPr [prf, in mathcomp.boot.ssrnat]
minn_maxl [prf, in mathcomp.boot.ssrnat]
minn_maxr [prf, in mathcomp.boot.ssrnat]
minnA [prf, in mathcomp.boot.ssrnat]
minnAC [prf, in mathcomp.boot.ssrnat]
minnACA [prf, in mathcomp.boot.ssrnat]
minnC [prf, in mathcomp.boot.ssrnat]
minnCA [prf, in mathcomp.boot.ssrnat]
minnE [prf, in mathcomp.boot.ssrnat]
minnK [prf, in mathcomp.boot.ssrnat]
minnMl [prf, in mathcomp.boot.ssrnat]
minnMr [prf, in mathcomp.boot.ssrnat]
minnn [prf, in mathcomp.boot.ssrnat]
minnormal_charsimple [prf, in mathcomp.solvable.maximal]
minnormal_exists [prf, in mathcomp.solvable.gseries]
minnormal_maxnormal [prf, in mathcomp.solvable.gseries]
minnormal_solvable [prf, in mathcomp.solvable.maximal]
minnSS [prf, in mathcomp.boot.ssrnat]
minPoly_decidable_closure [prf, in mathcomp.field.algebraics_fundamentals]
minPoly_dvdp [prf, in mathcomp.field.fieldext]
minPoly_irr [prf, in mathcomp.field.fieldext]
minpoly_mx1 [prf, in mathcomp.algebra.mxpoly]
minpoly_mx_free [prf, in mathcomp.algebra.mxpoly]
minpoly_mx_ring [prf, in mathcomp.algebra.mxpoly]
minpoly_mxM [prf, in mathcomp.algebra.mxpoly]
minPoly_XsubC [prf, in mathcomp.field.fieldext]
minPolyOver [prf, in mathcomp.field.fieldext]
minPolyS [prf, in mathcomp.field.fieldext]
minPolyxx [prf, in mathcomp.field.fieldext]
minr_rat [prf, in mathcomp.algebra.rat]
minset_eq [prf, in mathcomp.boot.finset]
minset_exists [prf, in mathcomp.boot.finset]
minset_fix [prf, in mathcomp.boot.finset]
minsetinf [prf, in mathcomp.boot.finset]
minsetp [prf, in mathcomp.boot.finset]
minsetP [prf, in mathcomp.boot.finset]
minusE [prf, in mathcomp.boot.ssrnat]
misom_isog [prf, in mathcomp.finite_group.morphism]
misomP [prf, in mathcomp.finite_group.morphism]
mk_monic_neq0 [prf, in mathcomp.algebra.qpoly]
mk_monic_X [prf, in mathcomp.algebra.qpoly]
mk_monic_Xn [prf, in mathcomp.algebra.qpoly]
mk_monicE [prf, in mathcomp.field.qfpoly]
mker [prf, in mathcomp.finite_group.morphism]
mkerl [prf, in mathcomp.finite_group.morphism]
mkerr [prf, in mathcomp.finite_group.morphism]
mkseq_nth [prf, in mathcomp.boot.seq]
mkseq_uniq [prf, in mathcomp.boot.seq]
mkseq_uniqP [prf, in mathcomp.boot.seq]
mkseqP [prf, in mathcomp.boot.seq]
mkseqS [prf, in mathcomp.boot.seq]
mod0n [prf, in mathcomp.boot.div]
mod0z [prf, in mathcomp.algebra.intdiv]
mod_Iirr0 [prf, in mathcomp.group_representation.character]
mod_Iirr_bij [prf, in mathcomp.group_representation.character]
mod_Iirr_eq0 [prf, in mathcomp.group_representation.character]
mod_IirrE [prf, in mathcomp.group_representation.character]
mod_IirrK [prf, in mathcomp.group_representation.character]
modact_coset_astab [prf, in mathcomp.finite_group.action]
modact_faithful [prf, in mathcomp.finite_group.action]
modact_is_action [prf, in mathcomp.finite_group.action]
modact_is_groupAction [prf, in mathcomp.finite_group.action]
modactE [prf, in mathcomp.finite_group.action]
modactEcond [prf, in mathcomp.finite_group.action]
modgactE [prf, in mathcomp.finite_group.action]
modn0 [prf, in mathcomp.boot.div]
modn1 [prf, in mathcomp.boot.div]
modn2 [prf, in mathcomp.boot.div]
modn_coprime [prf, in mathcomp.boot.div]
modn_def [prf, in mathcomp.boot.div]
modn_divl [prf, in mathcomp.boot.div]
modn_dvdm [prf, in mathcomp.boot.div]
modn_mod [prf, in mathcomp.boot.div]
modn_partP [prf, in mathcomp.boot.prime]
modn_pred [prf, in mathcomp.boot.div]
modn_small [prf, in mathcomp.boot.div]
modn_sqrB [prf, in mathcomp.boot.div]
modn_summ [prf, in mathcomp.boot.binomial]
modnB [prf, in mathcomp.boot.div]
modnD [prf, in mathcomp.boot.div]
modnDl [prf, in mathcomp.boot.div]
modnDm [prf, in mathcomp.boot.div]
modnDml [prf, in mathcomp.boot.div]
modnDmr [prf, in mathcomp.boot.div]
modnDr [prf, in mathcomp.boot.div]
modnMBXl [prf, in mathcomp.boot.div]
modnMDl [prf, in mathcomp.boot.div]
modnMDXl [prf, in mathcomp.boot.div]
modnMl [prf, in mathcomp.boot.div]
modnMm [prf, in mathcomp.boot.div]
modnMml [prf, in mathcomp.boot.div]
modnMmr [prf, in mathcomp.boot.div]
modnMr [prf, in mathcomp.boot.div]
modnn [prf, in mathcomp.boot.div]
modnS [prf, in mathcomp.boot.div]
modnXm [prf, in mathcomp.boot.div]
modNz_nat [prf, in mathcomp.algebra.intdiv]
modp_polyOver [prf, in mathcomp.field.fieldext]
modular_group_classP [prf, in mathcomp.solvable.extremal]
modular_group_structure [prf, in mathcomp.solvable.extremal]
module_baseAspace [prf, in mathcomp.field.fieldext]
module_baseVspace [prf, in mathcomp.field.fieldext]
modz0 [prf, in mathcomp.algebra.intdiv]
modz1 [prf, in mathcomp.algebra.intdiv]
modz_abs [prf, in mathcomp.algebra.intdiv]
modz_absm [prf, in mathcomp.algebra.intdiv]
modz_ge0 [prf, in mathcomp.algebra.intdiv]
modz_mod [prf, in mathcomp.algebra.intdiv]
modz_nat [prf, in mathcomp.algebra.intdiv]
modz_small [prf, in mathcomp.algebra.intdiv]
modzDl [prf, in mathcomp.algebra.intdiv]
modzDm [prf, in mathcomp.algebra.intdiv]
modzDml [prf, in mathcomp.algebra.intdiv]
modzDmr [prf, in mathcomp.algebra.intdiv]
modzDr [prf, in mathcomp.algebra.intdiv]
modzMDl [prf, in mathcomp.algebra.intdiv]
modzMl [prf, in mathcomp.algebra.intdiv]
modzMm [prf, in mathcomp.algebra.intdiv]
modzMml [prf, in mathcomp.algebra.intdiv]
modzMmr [prf, in mathcomp.algebra.intdiv]
modzMr [prf, in mathcomp.algebra.intdiv]
modzN [prf, in mathcomp.algebra.intdiv]
modzNm [prf, in mathcomp.algebra.intdiv]
modZp [prf, in mathcomp.boot.fintype]
modzXm [prf, in mathcomp.algebra.intdiv]
modzz [prf, in mathcomp.algebra.intdiv]
monic1 [prf, in mathcomp.algebra.poly]
monic_algC_pfactor [prf, in mathcomp.field.algC]
monic_algR_pfactor [prf, in mathcomp.field.algC]
monic_comreg [prf, in mathcomp.algebra.poly]
monic_exp [prf, in mathcomp.algebra.poly]
monic_lreg [prf, in mathcomp.algebra.poly]
monic_map [prf, in mathcomp.algebra.poly]
monic_minPoly [prf, in mathcomp.field.fieldext]
monic_mk_monic [prf, in mathcomp.algebra.qpoly]
monic_mulr_closed [prf, in mathcomp.algebra.poly]
monic_neq0 [prf, in mathcomp.algebra.poly]
monic_prod [prf, in mathcomp.algebra.poly]
monic_prod_XsubC [prf, in mathcomp.algebra.poly]
monic_rreg [prf, in mathcomp.algebra.poly]
monic_Xn_sub_1 [prf, in mathcomp.algebra.poly]
monicE [prf, in mathcomp.algebra.poly]
monicMl [prf, in mathcomp.algebra.poly]
monicMr [prf, in mathcomp.algebra.poly]
monicP [prf, in mathcomp.algebra.poly]
monicX [prf, in mathcomp.algebra.poly]
monicXaddC [prf, in mathcomp.algebra.poly]
monicXn [prf, in mathcomp.algebra.poly]
monicXnaddC [prf, in mathcomp.algebra.poly]
monicXnsubC [prf, in mathcomp.algebra.poly]
monicXsubC [prf, in mathcomp.algebra.poly]
mono_cycle [prf, in mathcomp.boot.path]
mono_cycle_in [prf, in mathcomp.boot.path]
mono_inj [prf, in mathcomp.boot.eqtype]
mono_inj_in [prf, in mathcomp.boot.eqtype]
mono_leqif [prf, in mathcomp.boot.ssrnat]
mono_path [prf, in mathcomp.boot.path]
mono_path_in [prf, in mathcomp.boot.path]
mono_sorted [prf, in mathcomp.boot.path]
mono_sorted_in [prf, in mathcomp.boot.path]
Monoid.Builders_15.opm1 [prf, in mathcomp.boot.bigop]
Monoid.mulC_dist [prf, in mathcomp.boot.bigop]
Monoid.mulC_id [prf, in mathcomp.boot.bigop]
Monoid.mulC_zero [prf, in mathcomp.boot.bigop]
Monoid.Theory.add0m [prf, in mathcomp.boot.bigop]
Monoid.Theory.addm0 [prf, in mathcomp.boot.bigop]
Monoid.Theory.addmA [prf, in mathcomp.boot.bigop]
Monoid.Theory.addmAC [prf, in mathcomp.boot.bigop]
Monoid.Theory.addmC [prf, in mathcomp.boot.bigop]
Monoid.Theory.addmCA [prf, in mathcomp.boot.bigop]
Monoid.Theory.iteropE [prf, in mathcomp.boot.bigop]
Monoid.Theory.mul0m [prf, in mathcomp.boot.bigop]
Monoid.Theory.mul1m [prf, in mathcomp.boot.bigop]
Monoid.Theory.mulm0 [prf, in mathcomp.boot.bigop]
Monoid.Theory.mulm1 [prf, in mathcomp.boot.bigop]
Monoid.Theory.mulmDl [prf, in mathcomp.boot.bigop]
Monoid.Theory.mulmDr [prf, in mathcomp.boot.bigop]
morph1 [prf, in mathcomp.finite_group.morphism]
morph_afix [prf, in mathcomp.finite_group.action]
morph_astab [prf, in mathcomp.finite_group.action]
morph_astabs [prf, in mathcomp.finite_group.action]
morph_constt [prf, in mathcomp.solvable.pgroup]
morph_dom_groupset [prf, in mathcomp.finite_group.morphism]
morph_gacent [prf, in mathcomp.finite_group.action]
morph_gact_irr [prf, in mathcomp.finite_group.action]
morph_gastab [prf, in mathcomp.finite_group.action]
morph_gastabs [prf, in mathcomp.finite_group.action]
morph_generator [prf, in mathcomp.solvable.cyclic]
morph_Iirr0 [prf, in mathcomp.group_representation.character]
morph_Iirr_eq0 [prf, in mathcomp.group_representation.character]
morph_Iirr_inj [prf, in mathcomp.group_representation.character]
morph_IirrE [prf, in mathcomp.group_representation.character]
morph_injm_eq1 [prf, in mathcomp.finite_group.morphism]
morph_order [prf, in mathcomp.solvable.cyclic]
morph_p_elt [prf, in mathcomp.solvable.pgroup]
morph_prod [prf, in mathcomp.finite_group.morphism]
morphic_aut [prf, in mathcomp.finite_group.automorphism]
morphicP [prf, in mathcomp.finite_group.morphism]
morphim0 [prf, in mathcomp.finite_group.morphism]
morphim1 [prf, in mathcomp.finite_group.morphism]
morphim_abelem [prf, in mathcomp.solvable.abelian]
morphim_abelian [prf, in mathcomp.finite_group.morphism]
morphim_actm [prf, in mathcomp.finite_group.action]
morphim_bigcprod [prf, in mathcomp.finite_group.gproduct]
morphim_cent [prf, in mathcomp.finite_group.morphism]
morphim_cent1 [prf, in mathcomp.finite_group.morphism]
morphim_cent1s [prf, in mathcomp.finite_group.morphism]
morphim_center [prf, in mathcomp.solvable.center]
morphim_cents [prf, in mathcomp.finite_group.morphism]
morphim_class [prf, in mathcomp.finite_group.morphism]
morphim_comp [prf, in mathcomp.finite_group.morphism]
morphim_conj [prf, in mathcomp.finite_group.automorphism]
morphim_coprime_bigdprod [prf, in mathcomp.finite_group.gproduct]
morphim_coprime_dprod [prf, in mathcomp.finite_group.gproduct]
morphim_coprime_sdprod [prf, in mathcomp.finite_group.gproduct]
morphim_cprod [prf, in mathcomp.finite_group.gproduct]
morphim_cprodm [prf, in mathcomp.finite_group.gproduct]
morphim_cprodml [prf, in mathcomp.finite_group.gproduct]
morphim_cprodmr [prf, in mathcomp.finite_group.gproduct]
morphim_cycle [prf, in mathcomp.finite_group.morphism]
morphim_cyclic [prf, in mathcomp.solvable.cyclic]
morphim_der [prf, in mathcomp.solvable.commutator]
morphim_dffunXn [prf, in mathcomp.finite_group.gproduct]
morphim_dfung1 [prf, in mathcomp.finite_group.gproduct]
morphim_dprodm [prf, in mathcomp.finite_group.gproduct]
morphim_dprodml [prf, in mathcomp.finite_group.gproduct]
morphim_dprodmr [prf, in mathcomp.finite_group.gproduct]
morphim_eq0 [prf, in mathcomp.finite_group.morphism]
morphim_factm [prf, in mathcomp.finite_group.morphism]
morphim_Fitting [prf, in mathcomp.solvable.maximal]
morphim_fixP [prf, in mathcomp.finite_group.automorphism]
morphim_fstX [prf, in mathcomp.finite_group.gproduct]
morphim_gen [prf, in mathcomp.finite_group.morphism]
morphim_grank [prf, in mathcomp.solvable.abelian]
morphim_groupset [prf, in mathcomp.finite_group.morphism]
morphim_Hall [prf, in mathcomp.solvable.pgroup]
morphim_homg [prf, in mathcomp.finite_group.morphism]
morphim_idm [prf, in mathcomp.finite_group.morphism]
morphim_ifactm [prf, in mathcomp.finite_group.morphism]
morphim_inj [prf, in mathcomp.finite_group.morphism]
morphim_injG [prf, in mathcomp.finite_group.morphism]
morphim_injm_eq1 [prf, in mathcomp.finite_group.morphism]
morphim_invm [prf, in mathcomp.finite_group.morphism]
morphim_invmE [prf, in mathcomp.finite_group.morphism]
morphim_isom [prf, in mathcomp.finite_group.morphism]
morphim_ker [prf, in mathcomp.finite_group.morphism]
morphim_lcn [prf, in mathcomp.solvable.nilpotent]
morphim_Ldiv [prf, in mathcomp.solvable.abelian]
morphim_LdivT [prf, in mathcomp.solvable.abelian]
morphim_Mho [prf, in mathcomp.solvable.abelian]
morphim_mx_abs_irr [prf, in mathcomp.group_representation.mxrepresentation]
morphim_mx_irr [prf, in mathcomp.group_representation.mxrepresentation]
morphim_mx_repr [prf, in mathcomp.group_representation.mxrepresentation]
morphim_mxE [prf, in mathcomp.group_representation.mxrepresentation]
morphim_nil [prf, in mathcomp.solvable.nilpotent]
morphim_norm [prf, in mathcomp.finite_group.morphism]
morphim_normal [prf, in mathcomp.finite_group.morphism]
morphim_normG [prf, in mathcomp.finite_group.morphism]
morphim_norms [prf, in mathcomp.finite_group.morphism]
morphim_odd [prf, in mathcomp.solvable.pgroup]
morphim_Ohm [prf, in mathcomp.solvable.abelian]
morphim_p_group [prf, in mathcomp.solvable.pgroup]
morphim_p_index [prf, in mathcomp.solvable.pgroup]
morphim_p_rank_abelian [prf, in mathcomp.solvable.abelian]
morphim_pair1g [prf, in mathcomp.finite_group.gproduct]
morphim_pairg1 [prf, in mathcomp.finite_group.gproduct]
morphim_pcore [prf, in mathcomp.solvable.pgroup]
morphim_pcore_mod [prf, in mathcomp.solvable.pgroup]
morphim_pElem [prf, in mathcomp.solvable.abelian]
morphim_pgroup [prf, in mathcomp.solvable.pgroup]
morphim_pHall [prf, in mathcomp.solvable.pgroup]
morphim_Phi [prf, in mathcomp.solvable.maximal]
morphim_pnElem [prf, in mathcomp.solvable.abelian]
morphim_pprod [prf, in mathcomp.finite_group.gproduct]
morphim_pprodm [prf, in mathcomp.finite_group.gproduct]
morphim_pprodml [prf, in mathcomp.finite_group.gproduct]
morphim_pprodmr [prf, in mathcomp.finite_group.gproduct]
morphim_pseries [prf, in mathcomp.solvable.pgroup]
morphim_pSylow [prf, in mathcomp.solvable.pgroup]
morphim_qisom [prf, in mathcomp.finite_group.quotient]
morphim_qisom_inj [prf, in mathcomp.finite_group.quotient]
morphim_quotm [prf, in mathcomp.finite_group.quotient]
morphim_rank_abelian [prf, in mathcomp.solvable.abelian]
morphim_restrm [prf, in mathcomp.finite_group.morphism]
morphim_sdprodm [prf, in mathcomp.finite_group.gproduct]
morphim_sdprodml [prf, in mathcomp.finite_group.gproduct]
morphim_sdprodmr [prf, in mathcomp.finite_group.gproduct]
morphim_set1 [prf, in mathcomp.finite_group.morphism]
morphim_setIpre [prf, in mathcomp.finite_group.morphism]
morphim_sndX [prf, in mathcomp.finite_group.gproduct]
morphim_sol [prf, in mathcomp.solvable.nilpotent]
morphim_sub [prf, in mathcomp.finite_group.morphism]
morphim_subcent [prf, in mathcomp.finite_group.morphism]
morphim_subcent1 [prf, in mathcomp.finite_group.morphism]
morphim_subnorm [prf, in mathcomp.finite_group.morphism]
morphim_subnormal [prf, in mathcomp.solvable.gseries]
morphim_subnormG [prf, in mathcomp.finite_group.morphism]
morphim_Sylow [prf, in mathcomp.solvable.pgroup]
morphim_trivm [prf, in mathcomp.finite_group.morphism]
morphim_ucn [prf, in mathcomp.solvable.nilpotent]
morphim_Zgroup [prf, in mathcomp.solvable.sylow]
morphimD [prf, in mathcomp.finite_group.morphism]
morphimD1 [prf, in mathcomp.finite_group.morphism]
morphimDG [prf, in mathcomp.finite_group.morphism]
morphimE [prf, in mathcomp.finite_group.morphism]
morphimEdom [prf, in mathcomp.finite_group.morphism]
morphimEsub [prf, in mathcomp.finite_group.morphism]
morphimF [prf, in mathcomp.solvable.gfunctor]
morphimGI [prf, in mathcomp.finite_group.morphism]
morphimGK [prf, in mathcomp.finite_group.morphism]
morphimI [prf, in mathcomp.finite_group.morphism]
morphimIdom [prf, in mathcomp.finite_group.morphism]
morphimIG [prf, in mathcomp.finite_group.morphism]
morphimIim [prf, in mathcomp.finite_group.morphism]
morphimJ [prf, in mathcomp.finite_group.morphism]
morphimK [prf, in mathcomp.finite_group.morphism]
morphimMl [prf, in mathcomp.finite_group.morphism]
morphimMr [prf, in mathcomp.finite_group.morphism]
morphimP [prf, in mathcomp.finite_group.morphism]
morphimR [prf, in mathcomp.finite_group.morphism]
morphimS [prf, in mathcomp.finite_group.morphism]
morphimSGK [prf, in mathcomp.finite_group.morphism]
morphimSK [prf, in mathcomp.finite_group.morphism]
morphimT [prf, in mathcomp.finite_group.morphism]
morphimU [prf, in mathcomp.finite_group.morphism]
morphimV [prf, in mathcomp.finite_group.morphism]
morphimY [prf, in mathcomp.finite_group.morphism]
morphJ [prf, in mathcomp.finite_group.morphism]
morphM [prf, in mathcomp.finite_group.morphism]
morphmE [prf, in mathcomp.finite_group.morphism]
morphpre0 [prf, in mathcomp.finite_group.morphism]
morphpre_cent [prf, in mathcomp.finite_group.morphism]
morphpre_cent1 [prf, in mathcomp.finite_group.morphism]
morphpre_cent1s [prf, in mathcomp.finite_group.morphism]
morphpre_cents [prf, in mathcomp.finite_group.morphism]
morphpre_comp [prf, in mathcomp.finite_group.morphism]
morphpre_factm [prf, in mathcomp.finite_group.morphism]
morphpre_gen [prf, in mathcomp.finite_group.morphism]
morphpre_groupset [prf, in mathcomp.finite_group.morphism]
morphpre_idm [prf, in mathcomp.finite_group.morphism]
morphpre_ifactm [prf, in mathcomp.finite_group.morphism]
morphpre_inj [prf, in mathcomp.finite_group.morphism]
morphpre_invm [prf, in mathcomp.finite_group.morphism]
morphpre_maximal [prf, in mathcomp.solvable.gseries]
morphpre_maximal_eq [prf, in mathcomp.solvable.gseries]
morphpre_mx_abs_irr [prf, in mathcomp.group_representation.mxrepresentation]
morphpre_mx_irr [prf, in mathcomp.group_representation.mxrepresentation]
morphpre_mx_repr [prf, in mathcomp.group_representation.mxrepresentation]
morphpre_norm [prf, in mathcomp.finite_group.morphism]
morphpre_normal [prf, in mathcomp.finite_group.morphism]
morphpre_norms [prf, in mathcomp.finite_group.morphism]
morphpre_proper [prf, in mathcomp.finite_group.morphism]
morphpre_qisom [prf, in mathcomp.finite_group.quotient]
morphpre_quotm [prf, in mathcomp.finite_group.quotient]
morphpre_restrm [prf, in mathcomp.finite_group.morphism]
morphpre_set1 [prf, in mathcomp.finite_group.morphism]
morphpre_sub [prf, in mathcomp.finite_group.morphism]
morphpre_subcent [prf, in mathcomp.finite_group.morphism]
morphpre_subcent1 [prf, in mathcomp.finite_group.morphism]
morphpre_subnorm [prf, in mathcomp.finite_group.morphism]
morphpreD [prf, in mathcomp.finite_group.morphism]
morphpreE [prf, in mathcomp.finite_group.morphism]
morphpreI [prf, in mathcomp.finite_group.morphism]
morphpreIdom [prf, in mathcomp.finite_group.morphism]
morphpreIim [prf, in mathcomp.finite_group.morphism]
morphpreJ [prf, in mathcomp.finite_group.morphism]
morphpreK [prf, in mathcomp.finite_group.morphism]
morphpreMl [prf, in mathcomp.finite_group.morphism]
morphpreMr [prf, in mathcomp.finite_group.morphism]
morphpreP [prf, in mathcomp.finite_group.morphism]
morphpreS [prf, in mathcomp.finite_group.morphism]
morphpreSK [prf, in mathcomp.finite_group.morphism]
morphpreT [prf, in mathcomp.finite_group.morphism]
morphpreU [prf, in mathcomp.finite_group.morphism]
morphpreV [prf, in mathcomp.finite_group.morphism]
morphR [prf, in mathcomp.finite_group.morphism]
morphV [prf, in mathcomp.finite_group.morphism]
morphX [prf, in mathcomp.finite_group.morphism]
mpiE [prf, in mathcomp.boot.generic_quotient]
mul0g [prf, in mathcomp.finite_group.gproduct]
mul0mx [prf, in mathcomp.algebra.matrix]
mul0n [prf, in mathcomp.boot.ssrnat]
mul0rz [prf, in mathcomp.algebra.ssrint]
mul1fx [prf, in mathcomp.field.fieldext]
mul1mx [prf, in mathcomp.algebra.matrix]
mul1n [prf, in mathcomp.boot.ssrnat]
mul1q [prf, in mathcomp.algebra.rat]
mul2n [prf, in mathcomp.boot.ssrnat]
mul2z [prf, in mathcomp.algebra.ssrint]
mul_0poly [prf, in mathcomp.algebra.poly]
mul_1poly [prf, in mathcomp.algebra.poly]
mul_adj_mx [prf, in mathcomp.algebra.matrix]
mul_bin_diag [prf, in mathcomp.boot.binomial]
mul_bin_down [prf, in mathcomp.boot.binomial]
mul_bin_left [prf, in mathcomp.boot.binomial]
mul_block_col [prf, in mathcomp.algebra.matrix]
mul_card_Ohm_Mho_abelian [prf, in mathcomp.solvable.abelian]
mul_cardG [prf, in mathcomp.finite_group.fingroup]
mul_cfuni [prf, in mathcomp.group_representation.classfun]
mul_cfuni_on [prf, in mathcomp.group_representation.classfun]
mul_char [prf, in mathcomp.group_representation.character]
mul_col_mx [prf, in mathcomp.algebra.matrix]
mul_col_perm [prf, in mathcomp.algebra.matrix]
mul_col_row [prf, in mathcomp.algebra.matrix]
mul_conjC_lin_char [prf, in mathcomp.group_representation.character]
mul_copid_mx_pid [prf, in mathcomp.algebra.matrix]
mul_delta_mx [prf, in mathcomp.algebra.matrix]
mul_delta_mx_0 [prf, in mathcomp.algebra.matrix]
mul_delta_mx_cond [prf, in mathcomp.algebra.matrix]
mul_diag_mx [prf, in mathcomp.algebra.matrix]
mul_dsub_mx [prf, in mathcomp.algebra.matrix]
mul_fun_gmulf1 [prf, in mathcomp.boot.monoid]
mul_lead_coef [prf, in mathcomp.algebra.poly]
mul_lin_irr [prf, in mathcomp.group_representation.character]
mul_mx_adj [prf, in mathcomp.algebra.matrix]
mul_mx_diag [prf, in mathcomp.algebra.matrix]
mul_mx_row [prf, in mathcomp.algebra.matrix]
mul_mx_scalar [prf, in mathcomp.algebra.matrix]
mul_mxblock [prf, in mathcomp.algebra.matrix]
mul_mxblock_mxdiag [prf, in mathcomp.algebra.matrix]
mul_mxblock_mxrow [prf, in mathcomp.algebra.matrix]
mul_mxcol_mxrow [prf, in mathcomp.algebra.matrix]
mul_mxdiag_mxblock [prf, in mathcomp.algebra.matrix]
mul_mxdiag_mxcol [prf, in mathcomp.algebra.matrix]
mul_mxrow [prf, in mathcomp.algebra.matrix]
mul_mxrow_mxblock [prf, in mathcomp.algebra.matrix]
mul_mxrow_mxcol [prf, in mathcomp.algebra.matrix]
mul_mxrow_mxdiag [prf, in mathcomp.algebra.matrix]
mul_pid_mx [prf, in mathcomp.algebra.matrix]
mul_pid_mx_copid [prf, in mathcomp.algebra.matrix]
mul_poly0 [prf, in mathcomp.algebra.poly]
mul_poly1 [prf, in mathcomp.algebra.poly]
mul_poly_key [prf, in mathcomp.algebra.poly]
mul_polyA [prf, in mathcomp.algebra.poly]
mul_polyC [prf, in mathcomp.algebra.poly]
mul_polyDl [prf, in mathcomp.algebra.poly]
mul_polyDr [prf, in mathcomp.algebra.poly]
mul_row_block [prf, in mathcomp.algebra.matrix]
mul_row_col [prf, in mathcomp.algebra.matrix]
mul_row_perm [prf, in mathcomp.algebra.matrix]
mul_rowsub_mx [prf, in mathcomp.algebra.matrix]
mul_rV_lin [prf, in mathcomp.algebra.matrix]
mul_rV_lin1 [prf, in mathcomp.algebra.matrix]
mul_rVP [prf, in mathcomp.algebra.matrix]
mul_scalar_mx [prf, in mathcomp.algebra.matrix]
mul_subdefA [prf, in mathcomp.algebra.rat]
mul_subG [prf, in mathcomp.finite_group.fingroup]
mul_submxrow [prf, in mathcomp.algebra.matrix]
mul_unitarymx [prf, in mathcomp.algebra.spectral]
mul_usub_mx [prf, in mathcomp.algebra.matrix]
mul_vchar [prf, in mathcomp.group_representation.vcharacter]
mul_vec_lin [prf, in mathcomp.algebra.matrix]
mul_vec_lin_row [prf, in mathcomp.algebra.matrix]
mul_xcol [prf, in mathcomp.algebra.matrix]
mulfx_addl [prf, in mathcomp.field.fieldext]
mulfxA [prf, in mathcomp.field.fieldext]
mulfxC [prf, in mathcomp.field.fieldext]
mulg0 [prf, in mathcomp.finite_group.gproduct]
mulg1_eq [prf, in mathcomp.boot.monoid]
mulg_eq1 [prf, in mathcomp.boot.monoid]
mulg_exp_card_rcosets [prf, in mathcomp.solvable.finmodule]
mulg_ffun [prf, in mathcomp.finite_group.gproduct]
mulg_nil [prf, in mathcomp.solvable.nilpotent]
mulg_normal_maximal [prf, in mathcomp.solvable.gseries]
mulg_set1 [prf, in mathcomp.finite_group.fingroup]
mulG_sub [prf, in mathcomp.finite_group.fingroup]
mulG_subG [prf, in mathcomp.finite_group.fingroup]
mulG_subl [prf, in mathcomp.finite_group.fingroup]
mulg_subl [prf, in mathcomp.finite_group.fingroup]
mulG_subr [prf, in mathcomp.finite_group.fingroup]
mulg_subr [prf, in mathcomp.finite_group.fingroup]
mulgI [prf, in mathcomp.boot.monoid]
mulGid [prf, in mathcomp.finite_group.fingroup]
mulGidPl [prf, in mathcomp.finite_group.fingroup]
mulGidPr [prf, in mathcomp.finite_group.fingroup]
mulgK [prf, in mathcomp.boot.monoid]
mulgKA [prf, in mathcomp.boot.monoid]
mulgmP [prf, in mathcomp.finite_group.gproduct]
mulGS [prf, in mathcomp.finite_group.fingroup]
mulgS [prf, in mathcomp.finite_group.fingroup]
mulGSgid [prf, in mathcomp.finite_group.fingroup]
mulGSid [prf, in mathcomp.finite_group.fingroup]
mulgSS [prf, in mathcomp.finite_group.fingroup]
mulGsubP [prf, in mathcomp.finite_group.fingroup]
mulgU [prf, in mathcomp.finite_group.fingroup]
mulgV [prf, in mathcomp.boot.monoid]
mulgVK [prf, in mathcomp.boot.monoid]
mulIg [prf, in mathcomp.boot.monoid]
mulKg [prf, in mathcomp.boot.monoid]
mulKmx [prf, in mathcomp.algebra.matrix]
mulKn [prf, in mathcomp.boot.div]
mulKVmx [prf, in mathcomp.algebra.matrix]
mulKz [prf, in mathcomp.algebra.intdiv]
mulmx0 [prf, in mathcomp.algebra.matrix]
mulmx0_rank_max [prf, in mathcomp.algebra.mxalgebra]
mulmx1 [prf, in mathcomp.algebra.matrix]
mulmx1_min [prf, in mathcomp.algebra.matrix]
mulmx1_min_rank [prf, in mathcomp.algebra.mxalgebra]
mulmx1_unit [prf, in mathcomp.algebra.matrix]
mulmx1C [prf, in mathcomp.algebra.matrix]
mulmx_base [prf, in mathcomp.algebra.mxalgebra]
mulmx_block [prf, in mathcomp.algebra.matrix]
mulmx_coker [prf, in mathcomp.algebra.mxalgebra]
mulmx_colsub [prf, in mathcomp.algebra.matrix]
mulmx_delta_companion [prf, in mathcomp.algebra.mxpoly]
mulmx_diag [prf, in mathcomp.algebra.matrix]
mulmx_ebase [prf, in mathcomp.algebra.mxalgebra]
mulmx_free_eq0 [prf, in mathcomp.algebra.mxalgebra]
mulmx_is_bilinear [prf, in mathcomp.algebra.sesquilinear]
mulmx_is_scalable [prf, in mathcomp.algebra.matrix]
mulmx_ker [prf, in mathcomp.algebra.mxalgebra]
mulmx_key [prf, in mathcomp.algebra.matrix]
mulmx_lsub [prf, in mathcomp.algebra.matrix]
mulmx_max_rank [prf, in mathcomp.algebra.mxalgebra]
mulmx_rsub [prf, in mathcomp.algebra.matrix]
mulmx_sub [prf, in mathcomp.algebra.mxalgebra]
mulmx_sum_row [prf, in mathcomp.algebra.matrix]
mulmx_suml [prf, in mathcomp.algebra.matrix]
mulmx_sumr [prf, in mathcomp.algebra.matrix]
mulmxA [prf, in mathcomp.algebra.matrix]
mulmxBl [prf, in mathcomp.algebra.matrix]
mulmxBr [prf, in mathcomp.algebra.matrix]
mulmxDl [prf, in mathcomp.algebra.matrix]
mulmxDr [prf, in mathcomp.algebra.matrix]
mulmxE [prf, in mathcomp.algebra.matrix]
mulmxK [prf, in mathcomp.algebra.matrix]
mulmxKp [prf, in mathcomp.algebra.mxalgebra]
mulmxKpV [prf, in mathcomp.algebra.mxalgebra]
mulmxKtV [prf, in mathcomp.algebra.spectral]
mulmxKV [prf, in mathcomp.algebra.matrix]
mulmxKV_ker [prf, in mathcomp.algebra.mxalgebra]
mulmxN [prf, in mathcomp.algebra.matrix]
mulmxnE [prf, in mathcomp.algebra.matrix]
mulmxP [prf, in mathcomp.algebra.mxalgebra]
mulmxr_is_linear [prf, in mathcomp.algebra.matrix]
mulmxr_is_semilinear [prf, in mathcomp.algebra.matrix]
mulmxtVK [prf, in mathcomp.algebra.spectral]
mulmxV [prf, in mathcomp.algebra.matrix]
mulmxVp [prf, in mathcomp.algebra.mxalgebra]
muln0 [prf, in mathcomp.boot.ssrnat]
muln1 [prf, in mathcomp.boot.ssrnat]
muln2 [prf, in mathcomp.boot.ssrnat]
muln_cfunE [prf, in mathcomp.group_representation.classfun]
muln_divA [prf, in mathcomp.boot.div]
muln_divCA [prf, in mathcomp.boot.div]
muln_divCA_gcd [prf, in mathcomp.boot.div]
muln_eq0 [prf, in mathcomp.boot.ssrnat]
muln_eq1 [prf, in mathcomp.boot.ssrnat]
muln_gcdl [prf, in mathcomp.boot.div]
muln_gcdr [prf, in mathcomp.boot.div]
muln_gt0 [prf, in mathcomp.boot.ssrnat]
muln_lcm_gcd [prf, in mathcomp.boot.div]
muln_lcml [prf, in mathcomp.boot.div]
muln_lcmr [prf, in mathcomp.boot.div]
muln_modl [prf, in mathcomp.boot.div]
muln_modr [prf, in mathcomp.boot.div]
mulnA [prf, in mathcomp.boot.ssrnat]
mulnAC [prf, in mathcomp.boot.ssrnat]
mulnACA [prf, in mathcomp.boot.ssrnat]
mulnb [prf, in mathcomp.boot.ssrnat]
mulnbl [prf, in mathcomp.boot.ssrnat]
mulnBl [prf, in mathcomp.boot.ssrnat]
mulnbr [prf, in mathcomp.boot.ssrnat]
mulnBr [prf, in mathcomp.boot.ssrnat]
mulnC [prf, in mathcomp.boot.ssrnat]
mulnCA [prf, in mathcomp.boot.ssrnat]
mulnDl [prf, in mathcomp.boot.ssrnat]
mulnDr [prf, in mathcomp.boot.ssrnat]
mulnE [prf, in mathcomp.boot.ssrnat]
mulnK [prf, in mathcomp.boot.div]
mulNmx [prf, in mathcomp.algebra.matrix]
mulnn [prf, in mathcomp.boot.ssrnat]
mulNrNz [prf, in mathcomp.algebra.ssrint]
mulNrz [prf, in mathcomp.algebra.ssrint]
mulnS [prf, in mathcomp.boot.ssrnat]
mulnSr [prf, in mathcomp.boot.ssrnat]
mulpz [prf, in mathcomp.algebra.ssrint]
mulq_addl [prf, in mathcomp.algebra.rat]
mulq_def [prf, in mathcomp.algebra.rat]
mulq_frac [prf, in mathcomp.algebra.rat]
mulq_subdefC [prf, in mathcomp.algebra.rat]
mulq_subdefE [prf, in mathcomp.algebra.rat]
mulqA [prf, in mathcomp.algebra.rat]
mulqC [prf, in mathcomp.algebra.rat]
mulr0z [prf, in mathcomp.algebra.ssrint]
mulr1z [prf, in mathcomp.algebra.ssrint]
mulr2z [prf, in mathcomp.algebra.ssrint]
mulr_absz [prf, in mathcomp.algebra.ssrint]
mulrbz [prf, in mathcomp.algebra.ssrint]
mulrIz [prf, in mathcomp.algebra.ssrint]
mulrN1z [prf, in mathcomp.algebra.ssrint]
mulrNz [prf, in mathcomp.algebra.ssrint]
mulrz_eq0 [prf, in mathcomp.algebra.ssrint]
mulrz_ge0 [prf, in mathcomp.algebra.ssrint]
mulrz_ge0_le0 [prf, in mathcomp.algebra.ssrint]
mulrz_int [prf, in mathcomp.algebra.ssrint]
mulrz_le0 [prf, in mathcomp.algebra.ssrint]
mulrz_le0_ge0 [prf, in mathcomp.algebra.ssrint]
mulrz_nat [prf, in mathcomp.algebra.ssrint]
mulrz_neq0 [prf, in mathcomp.algebra.ssrint]
mulrz_suml [prf, in mathcomp.algebra.ssrint]
mulrz_sumr [prf, in mathcomp.algebra.ssrint]
mulrzA [prf, in mathcomp.algebra.ssrint]
mulrzA_C [prf, in mathcomp.algebra.ssrint]
mulrzAC [prf, in mathcomp.algebra.ssrint]
mulrzAl [prf, in mathcomp.algebra.ssrint]
mulrzAr [prf, in mathcomp.algebra.ssrint]
mulrzBl [prf, in mathcomp.algebra.ssrint]
mulrzBl_nat [prf, in mathcomp.algebra.ssrint]
mulrzBr [prf, in mathcomp.algebra.ssrint]
mulrzDl [prf, in mathcomp.algebra.ssrint]
mulrzDr [prf, in mathcomp.algebra.ssrint]
mulrzl [prf, in mathcomp.algebra.ssrint]
mulrzr [prf, in mathcomp.algebra.ssrint]
mulrzz [prf, in mathcomp.algebra.ssrint]
muls0mx [prf, in mathcomp.algebra.mxalgebra]
muls_eqmx [prf, in mathcomp.algebra.mxalgebra]
mulSG [prf, in mathcomp.finite_group.fingroup]
mulSg [prf, in mathcomp.finite_group.fingroup]
mulSgGid [prf, in mathcomp.finite_group.fingroup]
mulSGid [prf, in mathcomp.finite_group.fingroup]
mulsgP [prf, in mathcomp.finite_group.fingroup]
mulsmx0 [prf, in mathcomp.algebra.mxalgebra]
mulsmx_subP [prf, in mathcomp.algebra.mxalgebra]
mulsmxA [prf, in mathcomp.algebra.mxalgebra]
mulsmxDl [prf, in mathcomp.algebra.mxalgebra]
mulsmxDr [prf, in mathcomp.algebra.mxalgebra]
mulsmxP [prf, in mathcomp.algebra.mxalgebra]
mulsmxS [prf, in mathcomp.algebra.mxalgebra]
mulSn [prf, in mathcomp.boot.ssrnat]
mulSnr [prf, in mathcomp.boot.ssrnat]
multE [prf, in mathcomp.boot.ssrnat]
multiplicity_XsubC [prf, in mathcomp.algebra.poly]
mults0l [prf, in mathcomp.algebra.tensor]
mults0r [prf, in mathcomp.algebra.tensor]
mults_const [prf, in mathcomp.algebra.tensor]
mults_hmul [prf, in mathcomp.algebra.tensor]
mults_hmul_compat [prf, in mathcomp.algebra.tensor]
mults_scale [prf, in mathcomp.algebra.tensor]
multsDl [prf, in mathcomp.algebra.tensor]
multsDr [prf, in mathcomp.algebra.tensor]
multsNl [prf, in mathcomp.algebra.tensor]
multsNr [prf, in mathcomp.algebra.tensor]
mulUg [prf, in mathcomp.finite_group.fingroup]
mulVb [prf, in mathcomp.algebra.algebraic_hierarchy.divalg]
mulVKg [prf, in mathcomp.boot.monoid]
mulVmx [prf, in mathcomp.algebra.matrix]
mulVpmx [prf, in mathcomp.algebra.mxalgebra]
mulVq [prf, in mathcomp.algebra.rat]
mulz2 [prf, in mathcomp.algebra.ssrint]
mulz_divA [prf, in mathcomp.algebra.intdiv]
mulz_divCA [prf, in mathcomp.algebra.intdiv]
mulz_divCA_gcd [prf, in mathcomp.algebra.intdiv]
mulz_gcdl [prf, in mathcomp.algebra.intdiv]
mulz_gcdr [prf, in mathcomp.algebra.intdiv]
mulz_modl [prf, in mathcomp.algebra.intdiv]
mulz_modr [prf, in mathcomp.algebra.intdiv]
mulz_Nsign_abs [prf, in mathcomp.algebra.ssrint]
mulz_sg [prf, in mathcomp.algebra.ssrint]
mulz_sg_eq1 [prf, in mathcomp.algebra.ssrint]
mulz_sg_eqN1 [prf, in mathcomp.algebra.ssrint]
mulz_sign_abs [prf, in mathcomp.algebra.ssrint]
mulzK [prf, in mathcomp.algebra.intdiv]
mx'_cast [prf, in mathcomp.algebra.matrix]
mx0_is_diag [prf, in mathcomp.algebra.matrix]
mx0_is_scalar [prf, in mathcomp.algebra.matrix]
mx0_is_trig [prf, in mathcomp.algebra.matrix]
mx11_is_diag [prf, in mathcomp.algebra.matrix]
mx11_is_trig [prf, in mathcomp.algebra.matrix]
mx11_scalar [prf, in mathcomp.algebra.matrix]
mx1_sum_delta [prf, in mathcomp.algebra.matrix]
mx_abs_irr_cent_scalar [prf, in mathcomp.group_representation.mxrepresentation]
mx_abs_irrP [prf, in mathcomp.group_representation.mxrepresentation]
mx_abs_irrW [prf, in mathcomp.group_representation.mxrepresentation]
mx_butterfly [prf, in mathcomp.group_representation.mxrepresentation]
mx_factmod_sub [prf, in mathcomp.group_representation.mxrepresentation]
mx_faithful_inj [prf, in mathcomp.group_representation.mxrepresentation]
mx_faithful_irr_abelian_cyclic [prf, in mathcomp.group_representation.mxrepresentation]
mx_faithful_irr_center_cyclic [prf, in mathcomp.group_representation.mxrepresentation]
mx_Fp_abelem [prf, in mathcomp.group_representation.mxabelem]
mx_Fp_stable [prf, in mathcomp.group_representation.mxabelem]
mx_group_homocyclic [prf, in mathcomp.group_representation.mxabelem]
mx_ind [prf, in mathcomp.algebra.matrix]
mx_inv_horner0 [prf, in mathcomp.algebra.mxpoly]
mx_inv_hornerK [prf, in mathcomp.algebra.mxpoly]
mx_irr_abelian_linear [prf, in mathcomp.group_representation.mxrepresentation]
mx_irr_gring_op_center_scalar [prf, in mathcomp.group_representation.integral_char]
mx_irr_map [prf, in mathcomp.group_representation.mxrepresentation]
mx_irrP [prf, in mathcomp.group_representation.mxrepresentation]
mx_iso_component [prf, in mathcomp.group_representation.mxrepresentation]
mx_iso_module [prf, in mathcomp.group_representation.mxrepresentation]
mx_iso_refl [prf, in mathcomp.group_representation.mxrepresentation]
mx_iso_simple [prf, in mathcomp.group_representation.mxrepresentation]
mx_iso_sym [prf, in mathcomp.group_representation.mxrepresentation]
mx_iso_trans [prf, in mathcomp.group_representation.mxrepresentation]
mx_Jacobson_density [prf, in mathcomp.group_representation.mxrepresentation]
mx_JordanHolder [prf, in mathcomp.group_representation.mxrepresentation]
mx_JordanHolder_exists [prf, in mathcomp.group_representation.mxrepresentation]
mx_JordanHolder_max [prf, in mathcomp.group_representation.mxrepresentation]
mx_Maschke_pchar [prf, in mathcomp.group_representation.mxrepresentation]
mx_poly_ring_isom [prf, in mathcomp.algebra.mxpoly]
mx_reducible_semisimple [prf, in mathcomp.group_representation.mxrepresentation]
mx_reducibleS [prf, in mathcomp.group_representation.mxrepresentation]
mx_repr0 [prf, in mathcomp.group_representation.character]
mx_repr_actE [prf, in mathcomp.group_representation.mxabelem]
mx_repr_action_faithful [prf, in mathcomp.group_representation.mxabelem]
mx_repr_is_action [prf, in mathcomp.group_representation.mxabelem]
mx_repr_is_groupAction [prf, in mathcomp.group_representation.mxabelem]
mx_root_minpoly [prf, in mathcomp.algebra.mxpoly]
mx_rsim_abs_irr [prf, in mathcomp.group_representation.mxrepresentation]
mx_rsim_dadd [prf, in mathcomp.group_representation.character]
mx_rsim_def [prf, in mathcomp.group_representation.mxrepresentation]
mx_rsim_dsum [prf, in mathcomp.group_representation.character]
mx_rsim_factmod [prf, in mathcomp.group_representation.mxrepresentation]
mx_rsim_faithful [prf, in mathcomp.group_representation.mxrepresentation]
mx_rsim_in_submod [prf, in mathcomp.group_representation.mxrepresentation]
mx_rsim_irr [prf, in mathcomp.group_representation.mxrepresentation]
mx_rsim_iso [prf, in mathcomp.group_representation.mxrepresentation]
mx_rsim_map [prf, in mathcomp.group_representation.mxrepresentation]
mx_rsim_refl [prf, in mathcomp.group_representation.mxrepresentation]
mx_rsim_scalar [prf, in mathcomp.group_representation.mxrepresentation]
mx_rsim_socle [prf, in mathcomp.group_representation.character]
mx_rsim_standard [prf, in mathcomp.group_representation.character]
mx_rsim_sym [prf, in mathcomp.group_representation.mxrepresentation]
mx_rsim_trans [prf, in mathcomp.group_representation.mxrepresentation]
mx_rV_lin [prf, in mathcomp.algebra.matrix]
mx_Schreier [prf, in mathcomp.group_representation.mxrepresentation]
mx_Schur [prf, in mathcomp.group_representation.mxrepresentation]
mx_Schur_inj [prf, in mathcomp.group_representation.mxrepresentation]
mx_Schur_inj_iso [prf, in mathcomp.group_representation.mxrepresentation]
mx_Schur_iso [prf, in mathcomp.group_representation.mxrepresentation]
mx_Schur_onto [prf, in mathcomp.group_representation.mxrepresentation]
mx_second_rsim [prf, in mathcomp.group_representation.mxrepresentation]
mx_series_lt [prf, in mathcomp.group_representation.mxrepresentation]
mx_series_rcons [prf, in mathcomp.group_representation.mxrepresentation]
mx_series_repr_irr [prf, in mathcomp.group_representation.mxrepresentation]
mx_subseries_module [prf, in mathcomp.group_representation.mxrepresentation]
mx_subseries_module' [prf, in mathcomp.group_representation.mxrepresentation]
mx_vec_lin [prf, in mathcomp.algebra.matrix]
mxblock0 [prf, in mathcomp.algebra.matrix]
mxblock_const [prf, in mathcomp.algebra.matrix]
mxblock_recl [prf, in mathcomp.algebra.matrix]
mxblock_recu [prf, in mathcomp.algebra.matrix]
mxblock_recul [prf, in mathcomp.algebra.matrix]
mxblock_sum [prf, in mathcomp.algebra.matrix]
mxblockB [prf, in mathcomp.algebra.matrix]
mxblockD [prf, in mathcomp.algebra.matrix]
mxblockEh [prf, in mathcomp.algebra.matrix]
mxblockEv [prf, in mathcomp.algebra.matrix]
mxblockK [prf, in mathcomp.algebra.matrix]
mxblockN [prf, in mathcomp.algebra.matrix]
mxblockP [prf, in mathcomp.algebra.matrix]
mxcol0 [prf, in mathcomp.algebra.matrix]
mxcol_const [prf, in mathcomp.algebra.matrix]
mxcol_mul [prf, in mathcomp.algebra.matrix]
mxcol_recu [prf, in mathcomp.algebra.matrix]
mxcol_sum [prf, in mathcomp.algebra.matrix]
mxcolB [prf, in mathcomp.algebra.matrix]
mxcolD [prf, in mathcomp.algebra.matrix]
mxcolEblock [prf, in mathcomp.algebra.matrix]
mxcolK [prf, in mathcomp.algebra.matrix]
mxcolN [prf, in mathcomp.algebra.matrix]
mxcolP [prf, in mathcomp.algebra.matrix]
mxdiag0 [prf, in mathcomp.algebra.matrix]
mxdiag_recl [prf, in mathcomp.algebra.matrix]
mxdiag_sum [prf, in mathcomp.algebra.matrix]
mxdiagB [prf, in mathcomp.algebra.matrix]
mxdiagD [prf, in mathcomp.algebra.matrix]
mxdiagN [prf, in mathcomp.algebra.matrix]
mxdiagZ [prf, in mathcomp.algebra.matrix]
mxdirect_adds_center [prf, in mathcomp.algebra.mxalgebra]
mxdirect_addsE [prf, in mathcomp.algebra.mxalgebra]
mxdirect_addsP [prf, in mathcomp.algebra.mxalgebra]
mxdirect_delta [prf, in mathcomp.algebra.mxalgebra]
mxdirect_kermxpoly [prf, in mathcomp.algebra.mxpoly]
mxdirect_sum_eigenspace [prf, in mathcomp.algebra.mxalgebra]
mxdirect_sum_geigenspace [prf, in mathcomp.algebra.mxpoly]
mxdirect_sum_kermx [prf, in mathcomp.algebra.mxpoly]
mxdirect_sums_center [prf, in mathcomp.algebra.mxalgebra]
mxdirect_sumsE [prf, in mathcomp.algebra.mxalgebra]
mxdirect_sumsP [prf, in mathcomp.algebra.mxalgebra]
mxdirect_trivial [prf, in mathcomp.algebra.mxalgebra]
mxdirectE [prf, in mathcomp.algebra.mxalgebra]
mxdirectEgeq [prf, in mathcomp.algebra.mxalgebra]
mxdirectP [prf, in mathcomp.algebra.mxalgebra]
mxE [prf, in mathcomp.algebra.matrix]
mxEmxblock [prf, in mathcomp.algebra.matrix]
mxEmxcol [prf, in mathcomp.algebra.matrix]
mxEmxrow [prf, in mathcomp.algebra.matrix]
mxminpoly_conj [prf, in mathcomp.algebra.mxred]
mxminpoly_conj [prf, in mathcomp.algebra.mxpoly]
mxminpoly_diag [prf, in mathcomp.algebra.mxpoly]
mxminpoly_dvd_char [prf, in mathcomp.algebra.mxpoly]
mxminpoly_linear_is_scalar [prf, in mathcomp.algebra.mxpoly]
mxminpoly_map [prf, in mathcomp.algebra.mxpoly]
mxminpoly_min [prf, in mathcomp.algebra.mxpoly]
mxminpoly_minP [prf, in mathcomp.algebra.mxpoly]
mxminpoly_monic [prf, in mathcomp.algebra.mxpoly]
mxminpoly_nonconstant [prf, in mathcomp.algebra.mxpoly]
mxminpoly_uconj [prf, in mathcomp.algebra.mxred]
mxminpoly_uconj [prf, in mathcomp.algebra.mxpoly]
mxmodule0 [prf, in mathcomp.group_representation.mxrepresentation]
mxmodule1 [prf, in mathcomp.group_representation.mxrepresentation]
mxmodule_abelem [prf, in mathcomp.group_representation.mxabelem]
mxmodule_abelem_subg [prf, in mathcomp.group_representation.mxabelem]
mxmodule_abelemG [prf, in mathcomp.group_representation.mxabelem]
mxmodule_conj [prf, in mathcomp.group_representation.mxrepresentation]
mxmodule_eigenvector [prf, in mathcomp.group_representation.mxrepresentation]
mxmodule_envelop [prf, in mathcomp.group_representation.mxrepresentation]
mxmodule_eqg [prf, in mathcomp.group_representation.mxrepresentation]
mxmodule_form_qf [prf, in mathcomp.group_representation.mxrepresentation]
mxmodule_map [prf, in mathcomp.group_representation.mxrepresentation]
mxmodule_morphim [prf, in mathcomp.group_representation.mxrepresentation]
mxmodule_morphpre [prf, in mathcomp.group_representation.mxrepresentation]
mxmodule_quo [prf, in mathcomp.group_representation.mxrepresentation]
mxmodule_subg [prf, in mathcomp.group_representation.mxrepresentation]
mxmodule_trans [prf, in mathcomp.group_representation.mxrepresentation]
mxmoduleP [prf, in mathcomp.group_representation.mxrepresentation]
mxnonsimpleP [prf, in mathcomp.group_representation.mxrepresentation]
mxOver0 [prf, in mathcomp.algebra.matrix]
mxOver_const [prf, in mathcomp.algebra.matrix]
mxOver_constE [prf, in mathcomp.algebra.matrix]
mxOver_diag [prf, in mathcomp.algebra.matrix]
mxOver_diagE [prf, in mathcomp.algebra.matrix]
mxOver_nmod_closed [prf, in mathcomp.algebra.matrix]
mxOver_scalar [prf, in mathcomp.algebra.matrix]
mxOver_scalarE [prf, in mathcomp.algebra.matrix]
mxOverM [prf, in mathcomp.algebra.matrix]
mxOverP [prf, in mathcomp.algebra.matrix]
mxOverS [prf, in mathcomp.algebra.matrix]
mxOverZ [prf, in mathcomp.algebra.matrix]
mxrank0 [prf, in mathcomp.algebra.mxalgebra]
mxrank1 [prf, in mathcomp.algebra.mxalgebra]
mxrank_add [prf, in mathcomp.algebra.mxalgebra]
mxrank_adds_leqif [prf, in mathcomp.algebra.mxalgebra]
mxrank_cap_compl [prf, in mathcomp.algebra.mxalgebra]
mxrank_coker [prf, in mathcomp.algebra.mxalgebra]
mxrank_compl [prf, in mathcomp.algebra.mxalgebra]
mxrank_delta [prf, in mathcomp.algebra.mxalgebra]
mxrank_disjoint_sum [prf, in mathcomp.algebra.mxalgebra]
mxrank_eq0 [prf, in mathcomp.algebra.mxalgebra]
mxrank_Frobenius [prf, in mathcomp.algebra.mxalgebra]
mxrank_fullrowsub [prf, in mathcomp.algebra.mxalgebra]
mxrank_gen [prf, in mathcomp.algebra.mxalgebra]
mxrank_in_factmod [prf, in mathcomp.group_representation.mxrepresentation]
mxrank_in_submod [prf, in mathcomp.group_representation.mxrepresentation]
mxrank_injP [prf, in mathcomp.algebra.mxalgebra]
mxrank_iso [prf, in mathcomp.group_representation.mxrepresentation]
mxrank_ker [prf, in mathcomp.algebra.mxalgebra]
mxrank_leqif_eq [prf, in mathcomp.algebra.mxalgebra]
mxrank_leqif_sup [prf, in mathcomp.algebra.mxalgebra]
mxrank_map [prf, in mathcomp.algebra.mxalgebra]
mxrank_mul_ker [prf, in mathcomp.algebra.mxalgebra]
mxrank_mul_min [prf, in mathcomp.algebra.mxalgebra]
mxrank_opp [prf, in mathcomp.algebra.mxalgebra]
mxrank_rowg [prf, in mathcomp.group_representation.mxabelem]
mxrank_rsim [prf, in mathcomp.group_representation.mxrepresentation]
mxrank_scale [prf, in mathcomp.algebra.mxalgebra]
mxrank_scale_nz [prf, in mathcomp.algebra.mxalgebra]
mxrank_sum_cap [prf, in mathcomp.algebra.mxalgebra]
mxrank_sum_leqif [prf, in mathcomp.algebra.mxalgebra]
mxrank_tr [prf, in mathcomp.algebra.mxalgebra]
mxrank_unit [prf, in mathcomp.algebra.mxalgebra]
mxrank_unitary [prf, in mathcomp.algebra.spectral]
mxrankE [prf, in mathcomp.algebra.mxalgebra]
mxrankM_maxl [prf, in mathcomp.algebra.mxalgebra]
mxrankM_maxr [prf, in mathcomp.algebra.mxalgebra]
mxrankMfree [prf, in mathcomp.algebra.mxalgebra]
mxrankS [prf, in mathcomp.algebra.mxalgebra]
mxring_id_uniq [prf, in mathcomp.algebra.mxalgebra]
mxring_idP [prf, in mathcomp.algebra.mxalgebra]
mxrow0 [prf, in mathcomp.algebra.matrix]
mxrow_const [prf, in mathcomp.algebra.matrix]
mxrow_recl [prf, in mathcomp.algebra.matrix]
mxrow_sum [prf, in mathcomp.algebra.matrix]
mxrowB [prf, in mathcomp.algebra.matrix]
mxrowD [prf, in mathcomp.algebra.matrix]
mxrowEblock [prf, in mathcomp.algebra.matrix]
mxrowK [prf, in mathcomp.algebra.matrix]
mxrowN [prf, in mathcomp.algebra.matrix]
mxrowP [prf, in mathcomp.algebra.matrix]
mxsemisimple0 [prf, in mathcomp.group_representation.mxrepresentation]
mxsemisimple_module [prf, in mathcomp.group_representation.mxrepresentation]
mxsemisimple_reducible [prf, in mathcomp.group_representation.mxrepresentation]
mxsemisimpleS [prf, in mathcomp.group_representation.mxrepresentation]
mxsimple_abelem_subg [prf, in mathcomp.group_representation.mxabelem]
mxsimple_abelemGP [prf, in mathcomp.group_representation.mxabelem]
mxsimple_abelemP [prf, in mathcomp.group_representation.mxabelem]
mxsimple_abelian_linear [prf, in mathcomp.group_representation.mxrepresentation]
mxsimple_cyclic [prf, in mathcomp.group_representation.mxrepresentation]
mxsimple_eqg [prf, in mathcomp.group_representation.mxrepresentation]
mxsimple_exists [prf, in mathcomp.group_representation.mxrepresentation]
mxsimple_iso_simple [prf, in mathcomp.group_representation.mxrepresentation]
mxsimple_isoP [prf, in mathcomp.group_representation.mxrepresentation]
mxsimple_map [prf, in mathcomp.group_representation.mxrepresentation]
mxsimple_module [prf, in mathcomp.group_representation.mxrepresentation]
mxsimple_morphim [prf, in mathcomp.group_representation.mxrepresentation]
mxsimple_semisimple [prf, in mathcomp.group_representation.mxrepresentation]
mxsimple_subg [prf, in mathcomp.group_representation.mxrepresentation]
mxsimpleP [prf, in mathcomp.group_representation.mxrepresentation]
mxsize_recl [prf, in mathcomp.algebra.matrix]
mxsub_cast [prf, in mathcomp.algebra.matrix]
mxsub_comp [prf, in mathcomp.algebra.matrix]
mxsub_const [prf, in mathcomp.algebra.matrix]
mxsub_eq_colsub [prf, in mathcomp.algebra.matrix]
mxsub_eq_id [prf, in mathcomp.algebra.matrix]
mxsub_eq_rowsub [prf, in mathcomp.algebra.matrix]
mxsub_ffun [prf, in mathcomp.algebra.matrix]
mxsub_ffunl [prf, in mathcomp.algebra.matrix]
mxsub_ffunr [prf, in mathcomp.algebra.matrix]
mxsub_id [prf, in mathcomp.algebra.matrix]
mxsub_ind [prf, in mathcomp.algebra.matrix]
mxsub_mul [prf, in mathcomp.algebra.matrix]
mxsubcr [prf, in mathcomp.algebra.matrix]
mxsubrc [prf, in mathcomp.algebra.matrix]
mxtrace0 [prf, in mathcomp.algebra.matrix]
mxtrace1 [prf, in mathcomp.algebra.matrix]
mxtrace_block [prf, in mathcomp.algebra.matrix]
mxtrace_component [prf, in mathcomp.group_representation.mxrepresentation]
mxtrace_dadd_mod [prf, in mathcomp.group_representation.mxrepresentation]
mxtrace_diag [prf, in mathcomp.algebra.matrix]
mxtrace_dsum_mod [prf, in mathcomp.group_representation.mxrepresentation]
mxtrace_is_nmod_morphism [prf, in mathcomp.algebra.matrix]
mxtrace_is_scalar [prf, in mathcomp.algebra.matrix]
mxtrace_is_zmod_morphism [prf, in mathcomp.algebra.matrix]
mxtrace_mulC [prf, in mathcomp.algebra.matrix]
mxtrace_mxblock [prf, in mathcomp.algebra.matrix]
mxtrace_mxdiag [prf, in mathcomp.algebra.matrix]
mxtrace_prod [prf, in mathcomp.group_representation.character]
mxtrace_regular_pchar [prf, in mathcomp.group_representation.mxrepresentation]
mxtrace_rsim [prf, in mathcomp.group_representation.mxrepresentation]
mxtrace_scalar [prf, in mathcomp.algebra.matrix]
mxtrace_Socle [prf, in mathcomp.group_representation.mxrepresentation]
mxtrace_sub_fact_mod [prf, in mathcomp.group_representation.mxrepresentation]
mxtrace_submod1 [prf, in mathcomp.group_representation.mxrepresentation]
mxtrace_tr [prf, in mathcomp.algebra.matrix]
mxtraceD [prf, in mathcomp.algebra.matrix]
mxtraceZ [prf, in mathcomp.algebra.matrix]
mxvec_cast [prf, in mathcomp.algebra.matrix]
mxvec_delta [prf, in mathcomp.algebra.matrix]
mxvec_dotmul [prf, in mathcomp.algebra.matrix]
mxvec_eq0 [prf, in mathcomp.algebra.matrix]
mxvec_indexP [prf, in mathcomp.algebra.matrix]
mxvecE [prf, in mathcomp.algebra.matrix]
mxvecK [prf, in mathcomp.algebra.matrix]