mathcomp.ssreflect.tuple

Global Index

Y

_

(54001 entries)

Notation Index

J

T

W

X

Y

_

(1931 entries)

Module Index

J

K

W

X

Y

_

other

(1658 entries)

Variable Index

J

W

X

Y

_

other

(7199 entries)

Library Index

K

L

U

W

X

Y

_

other

(97 entries)

Lemma Index

Y

_

other

(15214 entries)

Axiom Index

H

J

K

L

N

O

T

U

V

W

X

Y

Z

_

other

(75 entries)

Constructor Index

J

K

W

Y

_

other

(224 entries)

Inductive Index

J

K

Q

W

Y

Z

_

other

(132 entries)

Projection Index

J

K

W

X

Y

_

other

(2371 entries)

Section Index

J

W

X

Y

_

other

(2266 entries)

Abbreviation Index

Y

_

other

(732 entries)

Definition Index

Y

_

other

(21455 entries)

Record Index

J

K

W

X

Y

_

other

(647 entries)

A (lemma)

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

Global Index

Y

_

(54001 entries)

Notation Index

J

T

W

X

Y

_

(1931 entries)

Module Index

J

K

W

X

Y

_

other

(1658 entries)

Variable Index

J

W

X

Y

_

other

(7199 entries)

Library Index

K

L

U

W

X

Y

_

other

(97 entries)

Lemma Index

Y

_

other

(15214 entries)

Axiom Index

H

J

K

L

N

O

T

U

V

W

X

Y

Z

_

other

(75 entries)

Constructor Index

J

K

W

Y

_

other

(224 entries)

Inductive Index

J

K

Q

W

Y

Z

_

other

(132 entries)

Projection Index

J

K

W

X

Y

_

other

(2371 entries)

Section Index

J

W

X

Y

_

other

(2266 entries)

Abbreviation Index

Y

_

other

(732 entries)

Definition Index

Y

_

other

(21455 entries)

Record Index

J

K

W

X

Y

_

other

(647 entries)