A (Lemmas)

Files

Definitions

Lemmas

Abbreviations

Global Index

A (Lemmas)

abelem1 [prf, in mathcomp.solvable.abelian]
abelem_abelian [prf, in mathcomp.solvable.abelian]
abelem_charsimple [prf, in mathcomp.solvable.maximal]
abelem_cyclic [prf, in mathcomp.solvable.abelian]
abelem_homocyclic [prf, in mathcomp.solvable.abelian]
abelem_mx_faithful [prf, in mathcomp.group_representation.mxabelem]
abelem_mx_irrP [prf, in mathcomp.group_representation.mxabelem]
abelem_mx_linear_proof [prf, in mathcomp.group_representation.mxabelem]
abelem_mx_repr [prf, in mathcomp.group_representation.mxabelem]
abelem_Ohm1 [prf, in mathcomp.solvable.abelian]
abelem_Ohm1P [prf, in mathcomp.solvable.abelian]
abelem_order_p [prf, in mathcomp.solvable.abelian]
abelem_pgroup [prf, in mathcomp.solvable.abelian]
abelem_pnElem [prf, in mathcomp.solvable.abelian]
abelem_rowgJ [prf, in mathcomp.group_representation.mxabelem]
abelem_rV_1 [prf, in mathcomp.group_representation.mxabelem]
abelem_rV_inj [prf, in mathcomp.group_representation.mxabelem]
abelem_rV_injm [prf, in mathcomp.group_representation.mxabelem]
abelem_rV_isom [prf, in mathcomp.group_representation.mxabelem]
abelem_rV_J [prf, in mathcomp.group_representation.mxabelem]
abelem_rV_K [prf, in mathcomp.group_representation.mxabelem]
abelem_rV_M [prf, in mathcomp.group_representation.mxabelem]
abelem_rV_mK [prf, in mathcomp.group_representation.mxabelem]
abelem_rV_S [prf, in mathcomp.group_representation.mxabelem]
abelem_rV_V [prf, in mathcomp.group_representation.mxabelem]
abelem_rV_X [prf, in mathcomp.group_representation.mxabelem]
abelem_split_dprod [prf, in mathcomp.solvable.maximal]
abelem_splits [prf, in mathcomp.solvable.abelian]
abelemE [prf, in mathcomp.solvable.abelian]
abelemJ [prf, in mathcomp.solvable.abelian]
abelemP [prf, in mathcomp.solvable.abelian]
abelemS [prf, in mathcomp.solvable.abelian]
abelian1 [prf, in mathcomp.finite_group.fingroup]
abelian_abs_irr [prf, in mathcomp.group_representation.mxrepresentation]
abelian_charsimple_special [prf, in mathcomp.solvable.maximal]
abelian_classP [prf, in mathcomp.finite_group.action]
abelian_exponent_gen [prf, in mathcomp.solvable.abelian]
abelian_gen [prf, in mathcomp.finite_group.fingroup]
abelian_nil [prf, in mathcomp.solvable.nilpotent]
abelian_rank1_cyclic [prf, in mathcomp.solvable.abelian]
abelian_sol [prf, in mathcomp.solvable.nilpotent]
abelian_splits [prf, in mathcomp.solvable.abelian]
abelian_structure [prf, in mathcomp.solvable.abelian]
abelian_type_abelem [prf, in mathcomp.solvable.abelian]
abelian_type_dprod_homocyclic [prf, in mathcomp.solvable.abelian]
abelian_type_dvdn_sorted [prf, in mathcomp.solvable.abelian]
abelian_type_gt1 [prf, in mathcomp.solvable.abelian]
abelian_type_homocyclic [prf, in mathcomp.solvable.abelian]
abelian_type_mx_group [prf, in mathcomp.group_representation.mxabelem]
abelian_type_pgroup [prf, in mathcomp.solvable.abelian]
abelian_type_sorted [prf, in mathcomp.solvable.abelian]
abelianE [prf, in mathcomp.finite_group.fingroup]
abelianJ [prf, in mathcomp.finite_group.fingroup]
abelianM [prf, in mathcomp.finite_group.fingroup]
abelianS [prf, in mathcomp.finite_group.fingroup]
abelianY [prf, in mathcomp.finite_group.fingroup]
absz0 [prf, in mathcomp.algebra.ssrint]
absz1 [prf, in mathcomp.algebra.ssrint]
absz_denq [prf, in mathcomp.algebra.rat]
absz_eq0 [prf, in mathcomp.algebra.ssrint]
absz_gt0 [prf, in mathcomp.algebra.ssrint]
absz_id [prf, in mathcomp.algebra.ssrint]
absz_nat [prf, in mathcomp.algebra.ssrint]
absz_sg [prf, in mathcomp.algebra.ssrint]
absz_sign [prf, in mathcomp.algebra.ssrint]
abszE [prf, in mathcomp.algebra.ssrint]
abszEsg [prf, in mathcomp.algebra.ssrint]
abszEsign [prf, in mathcomp.algebra.ssrint]
abszM [prf, in mathcomp.algebra.ssrint]
abszMsign [prf, in mathcomp.algebra.ssrint]
abszN [prf, in mathcomp.algebra.ssrint]
abszN1 [prf, in mathcomp.algebra.ssrint]
abszX [prf, in mathcomp.algebra.ssrint]
AC.cforallP [prf, in mathcomp.boot.ssrAC]
AC.count_memE [prf, in mathcomp.boot.ssrAC]
AC.pos_set_pos [prf, in mathcomp.boot.ssrAC]
AC.proof [prf, in mathcomp.boot.ssrAC]
AC.serial_Op [prf, in mathcomp.boot.ssrAC]
AC.set_pos_trecE [prf, in mathcomp.boot.ssrAC]
acomps_cons [prf, in mathcomp.solvable.jordanholder]
acompsP [prf, in mathcomp.solvable.jordanholder]
act1 [prf, in mathcomp.finite_group.action]
act_f_1 [prf, in mathcomp.solvable.burnside_app]
act_f_morph [prf, in mathcomp.solvable.burnside_app]
act_g_1 [prf, in mathcomp.solvable.burnside_app]
act_g_morph [prf, in mathcomp.solvable.burnside_app]
act_inj [prf, in mathcomp.finite_group.action]
act_reprK [prf, in mathcomp.finite_group.action]
actby_is_action [prf, in mathcomp.finite_group.action]
actby_is_groupAction [prf, in mathcomp.finite_group.action]
actbyE [prf, in mathcomp.finite_group.action]
actCJ [prf, in mathcomp.finite_group.action]
actCJV [prf, in mathcomp.finite_group.action]
actK [prf, in mathcomp.finite_group.action]
actKin [prf, in mathcomp.finite_group.action]
actKV [prf, in mathcomp.finite_group.action]
actKVin [prf, in mathcomp.finite_group.action]
actM [prf, in mathcomp.finite_group.action]
actmE [prf, in mathcomp.finite_group.action]
actmEfun [prf, in mathcomp.finite_group.action]
actMin [prf, in mathcomp.finite_group.action]
actmM [prf, in mathcomp.finite_group.action]
actperm_Aut [prf, in mathcomp.finite_group.action]
actperm_id [prf, in mathcomp.finite_group.action]
actpermE [prf, in mathcomp.finite_group.action]
actpermK [prf, in mathcomp.finite_group.action]
actpermM [prf, in mathcomp.finite_group.action]
acts_act [prf, in mathcomp.finite_group.action]
acts_actby [prf, in mathcomp.finite_group.action]
acts_char [prf, in mathcomp.finite_group.action]
acts_dom [prf, in mathcomp.finite_group.action]
acts_fix_norm [prf, in mathcomp.finite_group.action]
acts_gen [prf, in mathcomp.finite_group.action]
acts_in_orbit [prf, in mathcomp.finite_group.action]
acts_irr_mod [prf, in mathcomp.finite_group.action]
acts_irr_mod_astab [prf, in mathcomp.finite_group.action]
acts_irrQ [prf, in mathcomp.solvable.gseries]
acts_joing [prf, in mathcomp.finite_group.action]
acts_orbit [prf, in mathcomp.finite_group.action]
acts_qact_dom [prf, in mathcomp.finite_group.action]
acts_qact_dom_norm [prf, in mathcomp.finite_group.action]
acts_qact_doms [prf, in mathcomp.solvable.jordanholder]
acts_quotient [prf, in mathcomp.finite_group.action]
acts_ract [prf, in mathcomp.finite_group.action]
acts_rowg [prf, in mathcomp.group_representation.mxabelem]
acts_sub_orbit [prf, in mathcomp.finite_group.action]
acts_subnorm_fix [prf, in mathcomp.finite_group.action]
acts_subnorm_gacent [prf, in mathcomp.finite_group.action]
acts_subnorm_subgacent [prf, in mathcomp.finite_group.action]
acts_sum_card_orbit [prf, in mathcomp.finite_group.action]
actsD [prf, in mathcomp.finite_group.action]
actsEsd [prf, in mathcomp.finite_group.gproduct]
actsI [prf, in mathcomp.finite_group.action]
actsP [prf, in mathcomp.finite_group.action]
actsQ [prf, in mathcomp.finite_group.action]
actsRs_rcosets [prf, in mathcomp.finite_group.action]
actsU [prf, in mathcomp.finite_group.action]
actX [prf, in mathcomp.finite_group.action]
actXin [prf, in mathcomp.finite_group.action]
add0fx [prf, in mathcomp.field.fieldext]
add0n [prf, in mathcomp.boot.ssrnat]
add0q [prf, in mathcomp.algebra.rat]
add0v [prf, in mathcomp.algebra.vector]
add1n [prf, in mathcomp.boot.ssrnat]
add2n [prf, in mathcomp.boot.ssrnat]
add3n [prf, in mathcomp.boot.ssrnat]
add4n [prf, in mathcomp.boot.ssrnat]
add_1_Zp [prf, in mathcomp.algebra.zmodp]
add_block_mx [prf, in mathcomp.algebra.matrix]
add_col_mx [prf, in mathcomp.algebra.matrix]
add_lfunE [prf, in mathcomp.algebra.vector]
add_mx_repr [prf, in mathcomp.group_representation.character]
add_N1_Zp [prf, in mathcomp.algebra.zmodp]
add_poly0 [prf, in mathcomp.algebra.poly]
add_poly_key [prf, in mathcomp.algebra.poly]
add_polyA [prf, in mathcomp.algebra.poly]
add_polyC [prf, in mathcomp.algebra.poly]
add_polyN [prf, in mathcomp.algebra.poly]
add_proj_mx [prf, in mathcomp.algebra.mxalgebra]
add_proj_ortho [prf, in mathcomp.algebra.spectral]
add_rank_ortho [prf, in mathcomp.algebra.spectral]
add_row_mx [prf, in mathcomp.algebra.matrix]
add_sub_fact_mod [prf, in mathcomp.group_representation.mxrepresentation]
add_Zp_1 [prf, in mathcomp.algebra.zmodp]
addBnA [prf, in mathcomp.boot.ssrnat]
addBnAC [prf, in mathcomp.boot.ssrnat]
addBnCAC [prf, in mathcomp.boot.ssrnat]
addfxA [prf, in mathcomp.field.fieldext]
addfxC [prf, in mathcomp.field.fieldext]
addfxN [prf, in mathcomp.field.fieldext]
addIn [prf, in mathcomp.boot.ssrnat]
addKn [prf, in mathcomp.boot.ssrnat]
addmx_key [prf, in mathcomp.algebra.matrix]
addmx_sub [prf, in mathcomp.algebra.mxalgebra]
addmx_sub_adds [prf, in mathcomp.algebra.mxalgebra]
addn0 [prf, in mathcomp.boot.ssrnat]
addn1 [prf, in mathcomp.boot.ssrnat]
addn2 [prf, in mathcomp.boot.ssrnat]
addn3 [prf, in mathcomp.boot.ssrnat]
addn4 [prf, in mathcomp.boot.ssrnat]
addn_eq0 [prf, in mathcomp.boot.ssrnat]
addn_eq1 [prf, in mathcomp.boot.ssrnat]
addn_gt0 [prf, in mathcomp.boot.ssrnat]
addn_maxl [prf, in mathcomp.boot.ssrnat]
addn_maxr [prf, in mathcomp.boot.ssrnat]
addn_min_max [prf, in mathcomp.boot.ssrnat]
addn_minl [prf, in mathcomp.boot.ssrnat]
addn_minr [prf, in mathcomp.boot.ssrnat]
addn_negb [prf, in mathcomp.boot.ssrnat]
addnA [prf, in mathcomp.boot.ssrnat]
addnABC [prf, in mathcomp.boot.ssrnat]
addnAC [prf, in mathcomp.boot.ssrnat]
addnACA [prf, in mathcomp.boot.ssrnat]
addnACl [prf, in mathcomp.boot.ssrnat]
addnBA [prf, in mathcomp.boot.ssrnat]
addnBAC [prf, in mathcomp.boot.ssrnat]
addnBC [prf, in mathcomp.boot.ssrnat]
addnBCA [prf, in mathcomp.boot.ssrnat]
addnBl_leq [prf, in mathcomp.boot.ssrnat]
addnBn [prf, in mathcomp.boot.ssrnat]
addnBr_leq [prf, in mathcomp.boot.ssrnat]
addnC [prf, in mathcomp.boot.ssrnat]
addnCA [prf, in mathcomp.boot.ssrnat]
addnCAC [prf, in mathcomp.boot.ssrnat]
addnCB [prf, in mathcomp.boot.ssrnat]
addnCBA [prf, in mathcomp.boot.ssrnat]
addnE [prf, in mathcomp.boot.ssrnat]
addnI [prf, in mathcomp.boot.ssrnat]
addnK [prf, in mathcomp.boot.ssrnat]
addNmx [prf, in mathcomp.algebra.matrix]
addnn [prf, in mathcomp.boot.ssrnat]
addNq [prf, in mathcomp.algebra.rat]
addnS [prf, in mathcomp.boot.ssrnat]
addq_def [prf, in mathcomp.algebra.rat]
addq_frac [prf, in mathcomp.algebra.rat]
addq_subdefA [prf, in mathcomp.algebra.rat]
addq_subdefC [prf, in mathcomp.algebra.rat]
addq_subdefE [prf, in mathcomp.algebra.rat]
addqA [prf, in mathcomp.algebra.rat]
addqC [prf, in mathcomp.algebra.rat]
adds0mx [prf, in mathcomp.algebra.mxalgebra]
adds0mx_id [prf, in mathcomp.algebra.mxalgebra]
adds_eqmx [prf, in mathcomp.algebra.mxalgebra]
addsmx0 [prf, in mathcomp.algebra.mxalgebra]
addsmx0_id [prf, in mathcomp.algebra.mxalgebra]
addsmx_addKl [prf, in mathcomp.algebra.mxalgebra]
addsmx_addKr [prf, in mathcomp.algebra.mxalgebra]
addsmx_compl_full [prf, in mathcomp.algebra.mxalgebra]
addsmx_diff_cap_eq [prf, in mathcomp.algebra.mxalgebra]
addsmx_idPl [prf, in mathcomp.algebra.mxalgebra]
addsmx_idPr [prf, in mathcomp.algebra.mxalgebra]
addsmx_module [prf, in mathcomp.group_representation.mxrepresentation]
addsmx_ortho [prf, in mathcomp.algebra.spectral]
addsmx_semisimple [prf, in mathcomp.group_representation.mxrepresentation]
addsmx_sub [prf, in mathcomp.algebra.mxalgebra]
addsmxA [prf, in mathcomp.algebra.mxalgebra]
addsmxC [prf, in mathcomp.algebra.mxalgebra]
addsmxE [prf, in mathcomp.algebra.mxalgebra]
addsmxMr [prf, in mathcomp.algebra.mxalgebra]
addsmxS [prf, in mathcomp.algebra.mxalgebra]
addsmxSl [prf, in mathcomp.algebra.mxalgebra]
addsmxSr [prf, in mathcomp.algebra.mxalgebra]
addSn [prf, in mathcomp.boot.ssrnat]
addSnnS [prf, in mathcomp.boot.ssrnat]
addv0 [prf, in mathcomp.algebra.vector]
addv_complf [prf, in mathcomp.algebra.vector]
addv_diff [prf, in mathcomp.algebra.vector]
addv_diff_cap [prf, in mathcomp.algebra.vector]
addv_idPl [prf, in mathcomp.algebra.vector]
addv_idPr [prf, in mathcomp.algebra.vector]
addv_pi1_pi2 [prf, in mathcomp.algebra.vector]
addv_pi1_proj [prf, in mathcomp.algebra.vector]
addv_pi2_id [prf, in mathcomp.algebra.vector]
addv_pi2_proj [prf, in mathcomp.algebra.vector]
addvA [prf, in mathcomp.algebra.vector]
addvC [prf, in mathcomp.algebra.vector]
addvf [prf, in mathcomp.algebra.vector]
addvS [prf, in mathcomp.algebra.vector]
addvSl [prf, in mathcomp.algebra.vector]
addvSr [prf, in mathcomp.algebra.vector]
addvv [prf, in mathcomp.algebra.vector]
adim1P [prf, in mathcomp.field.falgebra]
adim_gt0 [prf, in mathcomp.field.falgebra]
adj1 [prf, in mathcomp.algebra.matrix]
adjoin0_deg [prf, in mathcomp.field.fieldext]
adjoin_cons [prf, in mathcomp.field.falgebra]
adjoin_deg_eq1 [prf, in mathcomp.field.fieldext]
adjoin_degree_aimg [prf, in mathcomp.field.fieldext]
adjoin_degreeE [prf, in mathcomp.field.fieldext]
adjoin_nil [prf, in mathcomp.field.falgebra]
adjoin_rcons [prf, in mathcomp.field.falgebra]
adjoin_separable [prf, in mathcomp.field.separable]
adjoin_separable_eq [prf, in mathcomp.field.separable]
adjoin_separableP [prf, in mathcomp.field.separable]
adjoin_seq1 [prf, in mathcomp.field.falgebra]
adjoin_seqSl [prf, in mathcomp.field.falgebra]
adjoin_seqSr [prf, in mathcomp.field.falgebra]
adjoinC [prf, in mathcomp.field.falgebra]
adjoinSl [prf, in mathcomp.field.falgebra]
adjugate_key [prf, in mathcomp.algebra.matrix]
adjunction_closed [prf, in mathcomp.boot.fingraph]
adjunction_n_comp [prf, in mathcomp.boot.fingraph]
adjZ [prf, in mathcomp.algebra.matrix]
AEnd_FinGroup.aut_mem_eqP [prf, in mathcomp.field.galois]
AEnd_FinGroup.comp_AEnd1l [prf, in mathcomp.field.galois]
AEnd_FinGroup.comp_AEndA [prf, in mathcomp.field.galois]
AEnd_FinGroup.comp_AEndK [prf, in mathcomp.field.galois]
AEnd_FinGroup.inAEndK [prf, in mathcomp.field.galois]
AEnd_FinGroup.kAEnd_group_set [prf, in mathcomp.field.galois]
AEnd_FinGroup.kAEnd_norm [prf, in mathcomp.field.galois]
AEnd_FinGroup.mem_kAut_coset [prf, in mathcomp.field.galois]
AEnd_lker0 [prf, in mathcomp.field.fieldext]
afix1 [prf, in mathcomp.finite_group.action]
afix1P [prf, in mathcomp.finite_group.action]
afix_actby [prf, in mathcomp.finite_group.action]
afix_comp [prf, in mathcomp.finite_group.action]
afix_cycle [prf, in mathcomp.finite_group.action]
afix_cycle_in [prf, in mathcomp.finite_group.action]
afix_gen [prf, in mathcomp.finite_group.action]
afix_gen_in [prf, in mathcomp.finite_group.action]
afix_mod [prf, in mathcomp.finite_group.action]
afix_ract [prf, in mathcomp.finite_group.action]
afix_repr [prf, in mathcomp.group_representation.mxabelem]
afix_subact [prf, in mathcomp.finite_group.action]
afixD1 [prf, in mathcomp.finite_group.action]
afixJ [prf, in mathcomp.finite_group.action]
afixJG [prf, in mathcomp.finite_group.action]
afixM [prf, in mathcomp.finite_group.action]
afixMin [prf, in mathcomp.finite_group.action]
afixP [prf, in mathcomp.finite_group.action]
afixRs_rcosets [prf, in mathcomp.finite_group.action]
afixS [prf, in mathcomp.finite_group.action]
afixU [prf, in mathcomp.finite_group.action]
afixYin [prf, in mathcomp.finite_group.action]
agenv_add_id [prf, in mathcomp.field.falgebra]
agenv_id [prf, in mathcomp.field.falgebra]
agenv_is_aspace [prf, in mathcomp.field.falgebra]
agenv_modl [prf, in mathcomp.field.falgebra]
agenv_modr [prf, in mathcomp.field.falgebra]
agenv_sub_modl [prf, in mathcomp.field.falgebra]
agenv_sub_modr [prf, in mathcomp.field.falgebra]
agenvE [prf, in mathcomp.field.falgebra]
agenvEl [prf, in mathcomp.field.falgebra]
agenvEr [prf, in mathcomp.field.falgebra]
agenvM [prf, in mathcomp.field.falgebra]
agenvS [prf, in mathcomp.field.falgebra]
agenvX [prf, in mathcomp.field.falgebra]
ahom_inP [prf, in mathcomp.field.falgebra]
ahom_is_monoid_morphism [prf, in mathcomp.field.falgebra]
AHom_lker0 [prf, in mathcomp.field.fieldext]
ahomP [prf, in mathcomp.field.falgebra]
ahomP_tmp [prf, in mathcomp.field.falgebra]
ahomWin [prf, in mathcomp.field.falgebra]
aimg1 [prf, in mathcomp.field.falgebra]
aimg_adjoin [prf, in mathcomp.field.falgebra]
aimg_adjoin_seq [prf, in mathcomp.field.falgebra]
aimg_agen [prf, in mathcomp.field.falgebra]
aimg_is_aspace [prf, in mathcomp.field.fieldext]
aimgM [prf, in mathcomp.field.falgebra]
aimgX [prf, in mathcomp.field.falgebra]
Aint0 [prf, in mathcomp.field.algnum]
Aint1 [prf, in mathcomp.field.algnum]
Aint_aut [prf, in mathcomp.field.algnum]
Aint_char [prf, in mathcomp.group_representation.integral_char]
Aint_Cint [prf, in mathcomp.field.algnum]
Aint_class_div_irr1 [prf, in mathcomp.group_representation.integral_char]
Aint_Cnat [prf, in mathcomp.field.algnum]
Aint_gring_mode_class_sum [prf, in mathcomp.group_representation.integral_char]
Aint_int [prf, in mathcomp.field.algnum]
Aint_irr [prf, in mathcomp.group_representation.integral_char]
Aint_prim_root [prf, in mathcomp.field.algnum]
Aint_subring [prf, in mathcomp.field.algnum]
Aint_subring_exists [prf, in mathcomp.field.algnum]
Aint_unity_root [prf, in mathcomp.field.algnum]
Aint_vchar [prf, in mathcomp.group_representation.vcharacter]
alg_integral [prf, in mathcomp.field.algebraics_fundamentals]
alg_num_field [prf, in mathcomp.field.algnum]
alg_polyC [prf, in mathcomp.algebra.poly]
alg_polyOver [prf, in mathcomp.field.fieldext]
algC'G_pchar [prf, in mathcomp.group_representation.classfun]
algC_autK [prf, in mathcomp.field.algC]
algC_invaut_is_monoid_morphism [prf, in mathcomp.field.algC]
algC_invaut_is_zmod_morphism [prf, in mathcomp.field.algC]
algC_invautK [prf, in mathcomp.field.algC]
algC_PET [prf, in mathcomp.field.algnum]
algC_pfactor_eq0 [prf, in mathcomp.field.algC]
algC_pfactorCE [prf, in mathcomp.field.algC]
algC_pfactorCgt0 [prf, in mathcomp.field.algC]
algC_pfactorE [prf, in mathcomp.field.algC]
algC_pfactorRE [prf, in mathcomp.field.algC]
algCreal_Im [prf, in mathcomp.field.algC]
algCreal_Re [prf, in mathcomp.field.algC]
algCrect [prf, in mathcomp.field.algC]
Algebra.add_fun_nmod_morphism [prf, in mathcomp.boot.nmodule]
Algebra.addIr [prf, in mathcomp.boot.nmodule]
Algebra.addKr [prf, in mathcomp.boot.nmodule]
Algebra.addNKr [prf, in mathcomp.boot.nmodule]
Algebra.addr0 [prf, in mathcomp.boot.nmodule]
Algebra.addr0_eq [prf, in mathcomp.boot.nmodule]
Algebra.addr_eq0 [prf, in mathcomp.boot.nmodule]
Algebra.addrAC [prf, in mathcomp.boot.nmodule]
Algebra.addrACA [prf, in mathcomp.boot.nmodule]
Algebra.addrCA [prf, in mathcomp.boot.nmodule]
Algebra.addrI [prf, in mathcomp.boot.nmodule]
Algebra.addrK [prf, in mathcomp.boot.nmodule]
Algebra.addrKA [prf, in mathcomp.boot.nmodule]
Algebra.addrN [prf, in mathcomp.boot.nmodule]
Algebra.addrNK [prf, in mathcomp.boot.nmodule]
Algebra.Builders_102.raddf0 [prf, in mathcomp.boot.nmodule]
Algebra.Builders_102.raddfD [prf, in mathcomp.boot.nmodule]
Algebra.Builders_155.add0r [prf, in mathcomp.boot.nmodule]
Algebra.Builders_155.addrC [prf, in mathcomp.boot.nmodule]
Algebra.Builders_155.valD0 [prf, in mathcomp.boot.nmodule]
Algebra.Builders_167.addrA [prf, in mathcomp.boot.nmodule]
Algebra.Builders_178.valD0 [prf, in mathcomp.boot.nmodule]
Algebra.Builders_183.addNr [prf, in mathcomp.boot.nmodule]
Algebra.can2_nmod_morphism [prf, in mathcomp.boot.nmodule]
Algebra.can2_zmod_morphism [prf, in mathcomp.boot.nmodule]
Algebra.commuteT [prf, in mathcomp.boot.nmodule]
Algebra.comp_is_nmod_morphism [prf, in mathcomp.boot.nmodule]
Algebra.eqr_opp [prf, in mathcomp.boot.nmodule]
Algebra.eqr_oppLR [prf, in mathcomp.boot.nmodule]
Algebra.idfun_is_nmod_morphism [prf, in mathcomp.boot.nmodule]
Algebra.iter_addr [prf, in mathcomp.boot.nmodule]
Algebra.iter_addr_0 [prf, in mathcomp.boot.nmodule]
Algebra.mul0rn [prf, in mathcomp.boot.nmodule]
Algebra.mulNrn [prf, in mathcomp.boot.nmodule]
Algebra.mulr0n [prf, in mathcomp.boot.nmodule]
Algebra.mulr1n [prf, in mathcomp.boot.nmodule]
Algebra.mulr2n [prf, in mathcomp.boot.nmodule]
Algebra.mulrb [prf, in mathcomp.boot.nmodule]
Algebra.mulrnA [prf, in mathcomp.boot.nmodule]
Algebra.mulrnAC [prf, in mathcomp.boot.nmodule]
Algebra.mulrnBl [prf, in mathcomp.boot.nmodule]
Algebra.mulrnBr [prf, in mathcomp.boot.nmodule]
Algebra.mulrnDl [prf, in mathcomp.boot.nmodule]
Algebra.mulrnDr [prf, in mathcomp.boot.nmodule]
Algebra.mulrS [prf, in mathcomp.boot.nmodule]
Algebra.mulrSr [prf, in mathcomp.boot.nmodule]
Algebra.mulrSS [prf, in mathcomp.boot.nmodule]
Algebra.null_fun_is_nmod_morphism [prf, in mathcomp.boot.nmodule]
Algebra.opp_is_zmod_morphism [prf, in mathcomp.boot.nmodule]
Algebra.oppr0 [prf, in mathcomp.boot.nmodule]
Algebra.oppr_eq0 [prf, in mathcomp.boot.nmodule]
Algebra.oppr_inj [prf, in mathcomp.boot.nmodule]
Algebra.opprB [prf, in mathcomp.boot.nmodule]
Algebra.opprD [prf, in mathcomp.boot.nmodule]
Algebra.opprK [prf, in mathcomp.boot.nmodule]
Algebra.raddf0 [prf, in mathcomp.boot.nmodule]
Algebra.raddf_eq0 [prf, in mathcomp.boot.nmodule]
Algebra.raddf_inj [prf, in mathcomp.boot.nmodule]
Algebra.raddf_sum [prf, in mathcomp.boot.nmodule]
Algebra.raddfB [prf, in mathcomp.boot.nmodule]
Algebra.raddfD [prf, in mathcomp.boot.nmodule]
Algebra.raddfMn [prf, in mathcomp.boot.nmodule]
Algebra.raddfMNn [prf, in mathcomp.boot.nmodule]
Algebra.raddfN [prf, in mathcomp.boot.nmodule]
Algebra.rpred0 [prf, in mathcomp.boot.nmodule]
Algebra.rpred0D [prf, in mathcomp.boot.nmodule]
Algebra.rpred_sum [prf, in mathcomp.boot.nmodule]
Algebra.rpredB [prf, in mathcomp.boot.nmodule]
Algebra.rpredBC [prf, in mathcomp.boot.nmodule]
Algebra.rpredBl [prf, in mathcomp.boot.nmodule]
Algebra.rpredBr [prf, in mathcomp.boot.nmodule]
Algebra.rpredD [prf, in mathcomp.boot.nmodule]
Algebra.rpredDl [prf, in mathcomp.boot.nmodule]
Algebra.rpredDr [prf, in mathcomp.boot.nmodule]
Algebra.rpredMn [prf, in mathcomp.boot.nmodule]
Algebra.rpredMNn [prf, in mathcomp.boot.nmodule]
Algebra.rpredN [prf, in mathcomp.boot.nmodule]
Algebra.rpredNr [prf, in mathcomp.boot.nmodule]
Algebra.sub0r [prf, in mathcomp.boot.nmodule]
Algebra.subIr [prf, in mathcomp.boot.nmodule]
Algebra.subKr [prf, in mathcomp.boot.nmodule]
Algebra.subr0 [prf, in mathcomp.boot.nmodule]
Algebra.subr0_eq [prf, in mathcomp.boot.nmodule]
Algebra.subr_eq [prf, in mathcomp.boot.nmodule]
Algebra.subr_eq0 [prf, in mathcomp.boot.nmodule]
Algebra.subrI [prf, in mathcomp.boot.nmodule]
Algebra.subrKA [prf, in mathcomp.boot.nmodule]
Algebra.subrKC [prf, in mathcomp.boot.nmodule]
Algebra.sumr_const [prf, in mathcomp.boot.nmodule]
Algebra.sumr_const_nat [prf, in mathcomp.boot.nmodule]
Algebra.sumrB [prf, in mathcomp.boot.nmodule]
Algebra.sumrMnl [prf, in mathcomp.boot.nmodule]
Algebra.sumrMnr [prf, in mathcomp.boot.nmodule]
Algebra.sumrN [prf, in mathcomp.boot.nmodule]
Algebra.telescope_sumr [prf, in mathcomp.boot.nmodule]
Algebra.telescope_sumr_eq [prf, in mathcomp.boot.nmodule]
Algebra.val0 [prf, in mathcomp.boot.nmodule]
Algebra.valB [prf, in mathcomp.boot.nmodule]
Algebra.valD [prf, in mathcomp.boot.nmodule]
Algebra.valN [prf, in mathcomp.boot.nmodule]
Algebra.zmod_closed0D [prf, in mathcomp.boot.nmodule]
Algebra.zmod_closedD [prf, in mathcomp.boot.nmodule]
Algebra.zmod_closedN [prf, in mathcomp.boot.nmodule]
Algebra.zmodClosedP [prf, in mathcomp.boot.nmodule]
algebraic0 [prf, in mathcomp.algebra.mxpoly]
algebraic1 [prf, in mathcomp.algebra.mxpoly]
algebraic_add [prf, in mathcomp.algebra.mxpoly]
algebraic_div [prf, in mathcomp.algebra.mxpoly]
algebraic_id [prf, in mathcomp.algebra.mxpoly]
algebraic_inv [prf, in mathcomp.algebra.mxpoly]
algebraic_mul [prf, in mathcomp.algebra.mxpoly]
algebraic_opp [prf, in mathcomp.algebra.mxpoly]
algebraic_root_polyXY [prf, in mathcomp.algebra.polyXY]
algebraic_sub [prf, in mathcomp.algebra.mxpoly]
Algebraics.Exports.nCdivE [prf, in mathcomp.field.algC]
Algebraics.Exports.zCdivE [prf, in mathcomp.field.algC]
Algebraics.Implementation.add0 [prf, in mathcomp.field.algC]
Algebraics.Implementation.addA [prf, in mathcomp.field.algC]
Algebraics.Implementation.addC [prf, in mathcomp.field.algC]
Algebraics.Implementation.addN [prf, in mathcomp.field.algC]
Algebraics.Implementation.algebraic [prf, in mathcomp.field.algC]
Algebraics.Implementation.archimedean [prf, in mathcomp.field.algC]
Algebraics.Implementation.closedFieldAxiom [prf, in mathcomp.field.algC]
Algebraics.Implementation.conj_is_monoid_morphism [prf, in mathcomp.field.algC]
Algebraics.Implementation.conj_is_nmod_morphism [prf, in mathcomp.field.algC]
Algebraics.Implementation.conj_is_zmod_morphism [prf, in mathcomp.field.algC]
Algebraics.Implementation.conj_nt [prf, in mathcomp.field.algC]
Algebraics.Implementation.conjK [prf, in mathcomp.field.algC]
Algebraics.Implementation.conjL_K [prf, in mathcomp.field.algC]
Algebraics.Implementation.conjL_nt [prf, in mathcomp.field.algC]
Algebraics.Implementation.CtoL_inj [prf, in mathcomp.field.algC]
Algebraics.Implementation.CtoL_is_monoid_morphism [prf, in mathcomp.field.algC]
Algebraics.Implementation.CtoL_is_zmod_morphism [prf, in mathcomp.field.algC]
Algebraics.Implementation.CtoL_K [prf, in mathcomp.field.algC]
Algebraics.Implementation.CtoL_P [prf, in mathcomp.field.algC]
Algebraics.Implementation.eq_root_is_equiv [prf, in mathcomp.field.algC]
Algebraics.Implementation.inv0 [prf, in mathcomp.field.algC]
Algebraics.Implementation.LtoC_K [prf, in mathcomp.field.algC]
Algebraics.Implementation.mul1 [prf, in mathcomp.field.algC]
Algebraics.Implementation.mulA [prf, in mathcomp.field.algC]
Algebraics.Implementation.mulC [prf, in mathcomp.field.algC]
Algebraics.Implementation.mulD [prf, in mathcomp.field.algC]
Algebraics.Implementation.mulVf [prf, in mathcomp.field.algC]
Algebraics.Implementation.one_nz [prf, in mathcomp.field.algC]
algid1 [prf, in mathcomp.field.fieldext]
algid_center [prf, in mathcomp.field.falgebra]
algid_decidable [prf, in mathcomp.field.falgebra]
algid_eq1 [prf, in mathcomp.field.falgebra]
algid_neq0 [prf, in mathcomp.field.falgebra]
algidl [prf, in mathcomp.field.falgebra]
algidr [prf, in mathcomp.field.falgebra]
algR_addr_gt0 [prf, in mathcomp.field.algC]
algR_ger_leVge [prf, in mathcomp.field.algC]
algR_ler_def [prf, in mathcomp.field.algC]
algR_ler_normD [prf, in mathcomp.field.algC]
algR_normr0_eq0 [prf, in mathcomp.field.algC]
algR_normrM [prf, in mathcomp.field.algC]
algR_normrMn [prf, in mathcomp.field.algC]
algR_normrN [prf, in mathcomp.field.algC]
algR_pfactor_eq0 [prf, in mathcomp.field.algC]
algR_pfactorCE [prf, in mathcomp.field.algC]
algR_pfactorR_mul_gt0 [prf, in mathcomp.field.algC]
algR_pfactorRE [prf, in mathcomp.field.algC]
algRval_is_monoid_morphism [prf, in mathcomp.field.algC]
algRval_is_zmod_morphism [prf, in mathcomp.field.algC]
all2E [prf, in mathcomp.boot.seq]
all2rel1 [prf, in mathcomp.boot.seq]
all2rel2 [prf, in mathcomp.boot.seq]
all2rel_cons [prf, in mathcomp.boot.seq]
all_allpairsP [prf, in mathcomp.boot.seq]
all_cat [prf, in mathcomp.boot.seq]
all_comm_mx1 [prf, in mathcomp.algebra.matrix]
all_comm_mx2P [prf, in mathcomp.algebra.matrix]
all_comm_mx_cons [prf, in mathcomp.algebra.matrix]
all_comm_mxP [prf, in mathcomp.algebra.matrix]
all_count [prf, in mathcomp.boot.seq]
all_filter [prf, in mathcomp.boot.seq]
all_filterP [prf, in mathcomp.boot.seq]
all_iffLR [prf, in mathcomp.boot.seq]
all_iffP [prf, in mathcomp.boot.seq]
all_map [prf, in mathcomp.boot.seq]
all_mapT [prf, in mathcomp.boot.seq]
all_mask [prf, in mathcomp.boot.seq]
all_merge [prf, in mathcomp.boot.path]
all_nil [prf, in mathcomp.boot.seq]
all_nseq [prf, in mathcomp.boot.seq]
all_nseqb [prf, in mathcomp.boot.seq]
all_nthP [prf, in mathcomp.boot.seq]
all_pmap [prf, in mathcomp.boot.seq]
all_pred0 [prf, in mathcomp.boot.seq]
all_pred1_constant [prf, in mathcomp.boot.seq]
all_pred1_nseq [prf, in mathcomp.boot.seq]
all_pred1P [prf, in mathcomp.boot.seq]
all_predC [prf, in mathcomp.boot.seq]
all_predI [prf, in mathcomp.boot.seq]
all_predT [prf, in mathcomp.boot.seq]
all_prime_primes [prf, in mathcomp.boot.prime]
all_rcons [prf, in mathcomp.boot.seq]
all_rev [prf, in mathcomp.boot.seq]
all_roots_prod_XsubC [prf, in mathcomp.algebra.poly]
all_seq1 [prf, in mathcomp.boot.seq]
all_set1 [prf, in mathcomp.boot.finset]
all_setU [prf, in mathcomp.boot.finset]
all_sigP [prf, in mathcomp.boot.seq]
all_sort [prf, in mathcomp.boot.path]
all_tnthP [prf, in mathcomp.boot.tuple]
all_undup [prf, in mathcomp.boot.seq]
allP [prf, in mathcomp.boot.seq]
allpairs0l [prf, in mathcomp.boot.seq]
allpairs0r [prf, in mathcomp.boot.seq]
allpairs1l [prf, in mathcomp.boot.seq]
allpairs1r [prf, in mathcomp.boot.seq]
allpairs_bseqP [prf, in mathcomp.boot.tuple]
allpairs_cat [prf, in mathcomp.boot.seq]
allpairs_cons [prf, in mathcomp.boot.seq]
allpairs_f [prf, in mathcomp.boot.seq]
allpairs_f_dep [prf, in mathcomp.boot.seq]
allpairs_mapl [prf, in mathcomp.boot.seq]
allpairs_mapr [prf, in mathcomp.boot.seq]
allpairs_rcons [prf, in mathcomp.boot.seq]
allpairs_rconsr [prf, in mathcomp.boot.seq]
allpairs_tupleP [prf, in mathcomp.boot.tuple]
allpairs_uniq [prf, in mathcomp.boot.seq]
allpairs_uniq_dep [prf, in mathcomp.boot.seq]
allpairsP [prf, in mathcomp.boot.seq]
allpairsPdep [prf, in mathcomp.boot.seq]
allPn [prf, in mathcomp.boot.seq]
allPP [prf, in mathcomp.boot.seq]
allrel0l [prf, in mathcomp.boot.seq]
allrel0r [prf, in mathcomp.boot.seq]
allrel1l [prf, in mathcomp.boot.seq]
allrel1r [prf, in mathcomp.boot.seq]
allrel_allpairsE [prf, in mathcomp.boot.seq]
allrel_catl [prf, in mathcomp.boot.seq]
allrel_catr [prf, in mathcomp.boot.seq]
allrel_cons2 [prf, in mathcomp.boot.seq]
allrel_consl [prf, in mathcomp.boot.seq]
allrel_consr [prf, in mathcomp.boot.seq]
allrel_filterl [prf, in mathcomp.boot.seq]
allrel_filterr [prf, in mathcomp.boot.seq]
allrel_mapl [prf, in mathcomp.boot.seq]
allrel_mapr [prf, in mathcomp.boot.seq]
allrel_maskl [prf, in mathcomp.boot.seq]
allrel_maskr [prf, in mathcomp.boot.seq]
allrel_merge [prf, in mathcomp.boot.path]
allrel_relI [prf, in mathcomp.boot.seq]
allrel_rev2 [prf, in mathcomp.boot.seq]
allrel_revl [prf, in mathcomp.boot.seq]
allrel_revr [prf, in mathcomp.boot.seq]
allrelC [prf, in mathcomp.boot.seq]
allrelP [prf, in mathcomp.boot.seq]
allrelT [prf, in mathcomp.boot.seq]
allss [prf, in mathcomp.boot.seq]
allT [prf, in mathcomp.boot.seq]
Alt_even [prf, in mathcomp.solvable.alt]
Alt_index [prf, in mathcomp.solvable.alt]
Alt_norm [prf, in mathcomp.solvable.alt]
Alt_normal [prf, in mathcomp.solvable.alt]
Alt_subset [prf, in mathcomp.solvable.alt]
Alt_trans [prf, in mathcomp.solvable.alt]
amove_act [prf, in mathcomp.finite_group.action]
amove_orbit [prf, in mathcomp.finite_group.action]
amoveK [prf, in mathcomp.finite_group.action]
amull1 [prf, in mathcomp.field.falgebra]
amull_inj [prf, in mathcomp.field.falgebra]
amull_is_linear [prf, in mathcomp.field.falgebra]
amullM [prf, in mathcomp.field.falgebra]
amulr_inj [prf, in mathcomp.field.falgebra]
amulr_is_linear [prf, in mathcomp.field.falgebra]
amulr_is_monoid_morphism [prf, in mathcomp.field.falgebra]
annihilator_mxP [prf, in mathcomp.group_representation.mxrepresentation]
anti_leq [prf, in mathcomp.boot.ssrnat]
anti_mono [prf, in mathcomp.boot.eqtype]
anti_mono_in [prf, in mathcomp.boot.eqtype]
aperm_faithful [prf, in mathcomp.solvable.alt]
aperm_is_action [prf, in mathcomp.finite_group.action]
apermE [prf, in mathcomp.finite_group.perm]
applyrE [prf, in mathcomp.algebra.sesquilinear]
arc_rot [prf, in mathcomp.boot.path]
arg_maxnP [prf, in mathcomp.boot.fintype]
arg_minnP [prf, in mathcomp.boot.fintype]
asimple_acompsP [prf, in mathcomp.solvable.jordanholder]
asimple_quo_maxainv [prf, in mathcomp.solvable.jordanholder]
asimpleI [prf, in mathcomp.solvable.jordanholder]
asimpleP [prf, in mathcomp.solvable.jordanholder]
aspace_divr_closed [prf, in mathcomp.field.fieldext]
aspaceOver_suproof [prf, in mathcomp.field.fieldext]
aspaceOverP [prf, in mathcomp.field.fieldext]
astab1 [prf, in mathcomp.finite_group.action]
astab1_act [prf, in mathcomp.finite_group.action]
astab1_act_in [prf, in mathcomp.finite_group.action]
astab1_scale_act [prf, in mathcomp.group_representation.mxabelem]
astab1_set [prf, in mathcomp.finite_group.action]
astab1J [prf, in mathcomp.finite_group.action]
astab1JG [prf, in mathcomp.finite_group.action]
astab1Js [prf, in mathcomp.finite_group.action]
astab1P [prf, in mathcomp.finite_group.action]
astab1R [prf, in mathcomp.finite_group.action]
astab1Rs [prf, in mathcomp.finite_group.action]
astab_act [prf, in mathcomp.finite_group.action]
astab_actby [prf, in mathcomp.finite_group.action]
astab_comp [prf, in mathcomp.finite_group.action]
astab_dom [prf, in mathcomp.finite_group.action]
astab_gen [prf, in mathcomp.finite_group.action]
astab_mod [prf, in mathcomp.finite_group.action]
astab_norm [prf, in mathcomp.finite_group.action]
astab_normal [prf, in mathcomp.finite_group.action]
astab_ract [prf, in mathcomp.finite_group.action]
astab_range [prf, in mathcomp.finite_group.action]
astab_rowg_repr [prf, in mathcomp.group_representation.mxabelem]
astab_setact [prf, in mathcomp.finite_group.action]
astab_setact_in [prf, in mathcomp.finite_group.action]
astab_setT_repr [prf, in mathcomp.group_representation.mxabelem]
astab_sub [prf, in mathcomp.finite_group.action]
astab_subact [prf, in mathcomp.finite_group.action]
astab_trans_gcore [prf, in mathcomp.finite_group.action]
astabC [prf, in mathcomp.finite_group.action]
astabCin [prf, in mathcomp.finite_group.action]
astabEsd [prf, in mathcomp.finite_group.gproduct]
astabIdom [prf, in mathcomp.finite_group.action]
astabJ [prf, in mathcomp.finite_group.action]
astabM [prf, in mathcomp.finite_group.action]
astabP [prf, in mathcomp.finite_group.action]
astabQ [prf, in mathcomp.finite_group.action]
astabQR [prf, in mathcomp.finite_group.action]
astabR [prf, in mathcomp.finite_group.action]
astabRs_rcosets [prf, in mathcomp.finite_group.action]
astabS [prf, in mathcomp.finite_group.action]
astabs1 [prf, in mathcomp.finite_group.action]
astabs_act [prf, in mathcomp.finite_group.action]
astabs_actby [prf, in mathcomp.finite_group.action]
astabs_Aut_isom [prf, in mathcomp.finite_group.action]
astabs_comp [prf, in mathcomp.finite_group.action]
astabs_dom [prf, in mathcomp.finite_group.action]
astabs_mod [prf, in mathcomp.finite_group.action]
astabs_quotient [prf, in mathcomp.finite_group.action]
astabs_ract [prf, in mathcomp.finite_group.action]
astabs_range [prf, in mathcomp.finite_group.action]
astabs_rowg_repr [prf, in mathcomp.group_representation.mxabelem]
astabs_set1 [prf, in mathcomp.finite_group.action]
astabs_setact [prf, in mathcomp.finite_group.action]
astabs_subact [prf, in mathcomp.finite_group.action]
astabsC [prf, in mathcomp.finite_group.action]
astabsD [prf, in mathcomp.finite_group.action]
astabsD1 [prf, in mathcomp.finite_group.action]
astabsEsd [prf, in mathcomp.finite_group.gproduct]
astabsI [prf, in mathcomp.finite_group.action]
astabsIdom [prf, in mathcomp.finite_group.action]
astabsJ [prf, in mathcomp.finite_group.action]
astabsP [prf, in mathcomp.finite_group.action]
astabsQ [prf, in mathcomp.finite_group.action]
astabsR [prf, in mathcomp.finite_group.action]
astabsU [prf, in mathcomp.finite_group.action]
astabU [prf, in mathcomp.finite_group.action]
asubv [prf, in mathcomp.field.falgebra]
atrans_acts [prf, in mathcomp.finite_group.action]
atrans_acts_card [prf, in mathcomp.finite_group.action]
atrans_acts_in [prf, in mathcomp.finite_group.action]
atrans_dvd [prf, in mathcomp.finite_group.action]
atrans_dvd_in [prf, in mathcomp.finite_group.action]
atrans_dvd_index_in [prf, in mathcomp.finite_group.action]
atrans_orbit [prf, in mathcomp.finite_group.action]
atrans_supgroup [prf, in mathcomp.finite_group.action]
atransP [prf, in mathcomp.finite_group.action]
atransP2 [prf, in mathcomp.finite_group.action]
atransP2in [prf, in mathcomp.finite_group.action]
atransPin [prf, in mathcomp.finite_group.action]
atransR [prf, in mathcomp.finite_group.action]
Aut1 [prf, in mathcomp.finite_group.automorphism]
Aut_aut [prf, in mathcomp.finite_group.automorphism]
Aut_Aut_isom [prf, in mathcomp.finite_group.automorphism]
aut_closed [prf, in mathcomp.finite_group.automorphism]
Aut_closed [prf, in mathcomp.finite_group.automorphism]
Aut_conj_aut [prf, in mathcomp.finite_group.automorphism]
Aut_cprod_by_full [prf, in mathcomp.solvable.center]
Aut_cprod_full [prf, in mathcomp.solvable.center]
aut_Crat [prf, in mathcomp.field.algC]
Aut_cycle_abelian [prf, in mathcomp.solvable.cyclic]
Aut_cyclic_abelian [prf, in mathcomp.solvable.cyclic]
Aut_extraspecial_full [prf, in mathcomp.solvable.maximal]
Aut_group_set [prf, in mathcomp.finite_group.automorphism]
aut_Iirr0 [prf, in mathcomp.group_representation.character]
aut_Iirr_eq0 [prf, in mathcomp.group_representation.character]
aut_Iirr_inj [prf, in mathcomp.group_representation.character]
aut_IirrE [prf, in mathcomp.group_representation.character]
Aut_in_isog [prf, in mathcomp.finite_group.action]
Aut_isomE [prf, in mathcomp.finite_group.automorphism]
Aut_isomM [prf, in mathcomp.finite_group.automorphism]
Aut_isomP [prf, in mathcomp.finite_group.automorphism]
Aut_morphic [prf, in mathcomp.finite_group.automorphism]
Aut_ncprod_full [prf, in mathcomp.solvable.center]
aut_prim_rootP [prf, in mathcomp.algebra.poly]
Aut_prime_cycle_cyclic [prf, in mathcomp.solvable.cyclic]
Aut_prime_cyclic [prf, in mathcomp.solvable.cyclic]
Aut_restr_perm [prf, in mathcomp.finite_group.action]
Aut_sub_fullP [prf, in mathcomp.finite_group.action]
aut_unity_rootC [prf, in mathcomp.algebra.poly]
aut_unity_rootP [prf, in mathcomp.algebra.poly]
autact_is_groupAction [prf, in mathcomp.finite_group.action]
autactK [prf, in mathcomp.finite_group.action]
autE [prf, in mathcomp.finite_group.automorphism]
autmE [prf, in mathcomp.finite_group.automorphism]