| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (80254 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1852 entries) |
| Binder Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (48996 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (383 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4219 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (93 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (14738 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (223 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (45 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (132 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (452 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1431 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1169 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (6273 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (248 entries) |
S (lemma)
same_pblock [in mathcomp.ssreflect.finset]same_fconnect1_r [in mathcomp.ssreflect.fingraph]
same_fconnect1 [in mathcomp.ssreflect.fingraph]
same_fconnect_finv [in mathcomp.ssreflect.fingraph]
same_connect_rev [in mathcomp.ssreflect.fingraph]
same_connect1r [in mathcomp.ssreflect.fingraph]
same_connect1 [in mathcomp.ssreflect.fingraph]
same_connect_r [in mathcomp.ssreflect.fingraph]
same_connect [in mathcomp.ssreflect.fingraph]
scalar_mxC [in mathcomp.algebra.matrix]
scalar_mx_is_multiplicative [in mathcomp.algebra.matrix]
scalar_mxM [in mathcomp.algebra.matrix]
scalar_mx_sum_delta [in mathcomp.algebra.matrix]
scalar_mx_block [in mathcomp.algebra.matrix]
scalar_mx_is_trig [in mathcomp.algebra.matrix]
scalar_mx_is_diag [in mathcomp.algebra.matrix]
scalar_mx_is_scalar [in mathcomp.algebra.matrix]
scalar_mx_is_additive [in mathcomp.algebra.matrix]
scalar_mx_key [in mathcomp.algebra.matrix]
scalar_mx_hom [in mathcomp.character.mxrepresentation]
scalar_mx_cent [in mathcomp.algebra.mxalgebra]
scalemxA [in mathcomp.algebra.matrix]
scalemxAl [in mathcomp.algebra.matrix]
scalemxAr [in mathcomp.algebra.matrix]
scalemxDl [in mathcomp.algebra.matrix]
scalemxDr [in mathcomp.algebra.matrix]
scalemx_inj [in mathcomp.algebra.matrix]
scalemx_eq0 [in mathcomp.algebra.matrix]
scalemx_const [in mathcomp.algebra.matrix]
scalemx_key [in mathcomp.algebra.matrix]
scalemx_sub [in mathcomp.algebra.mxalgebra]
scalemx1 [in mathcomp.algebra.matrix]
scalerMzl [in mathcomp.algebra.ssrint]
scalerMzr [in mathcomp.algebra.ssrint]
scaler_int [in mathcomp.algebra.ssrint]
scalezrE [in mathcomp.algebra.ssrint]
scale_zchar [in mathcomp.character.vcharacter]
scale_scalar_mx [in mathcomp.algebra.matrix]
scale_block_mx [in mathcomp.algebra.matrix]
scale_col_mx [in mathcomp.algebra.matrix]
scale_row_mx [in mathcomp.algebra.matrix]
scale_is_groupAction [in mathcomp.character.mxabelem]
scale_is_action [in mathcomp.character.mxabelem]
scale_actE [in mathcomp.character.mxabelem]
scale_lfunE [in mathcomp.algebra.vector]
scale_poly_eq0 [in mathcomp.algebra.poly]
scale_polyC [in mathcomp.algebra.poly]
scale_polyAl [in mathcomp.algebra.poly]
scale_polyDl [in mathcomp.algebra.poly]
scale_polyDr [in mathcomp.algebra.poly]
scale_1poly [in mathcomp.algebra.poly]
scale_polyA [in mathcomp.algebra.poly]
scale_polyE [in mathcomp.algebra.poly]
scale_poly_key [in mathcomp.algebra.poly]
scale1mx [in mathcomp.algebra.matrix]
scalqE [in mathcomp.algebra.rat]
scalq_eq0 [in mathcomp.algebra.rat]
scalq_def [in mathcomp.algebra.rat]
scanlK [in mathcomp.ssreflect.seq]
scanl_bseqP [in mathcomp.ssreflect.tuple]
scanl_tupleP [in mathcomp.ssreflect.tuple]
scanl_rcons [in mathcomp.ssreflect.seq]
scanl_cat [in mathcomp.ssreflect.seq]
SchurZassenhaus_trans_actsol [in mathcomp.solvable.hall]
SchurZassenhaus_trans_sol [in mathcomp.solvable.hall]
SchurZassenhaus_split [in mathcomp.solvable.hall]
SCN_max [in mathcomp.solvable.maximal]
SCN_abelian [in mathcomp.solvable.maximal]
SCN_P [in mathcomp.solvable.maximal]
sdpairE [in mathcomp.fingroup.gproduct]
sdpair_setact [in mathcomp.fingroup.gproduct]
sdpair_act [in mathcomp.fingroup.gproduct]
sdpair1_morphM [in mathcomp.fingroup.gproduct]
sdpair2_morphM [in mathcomp.fingroup.gproduct]
sdprodE [in mathcomp.fingroup.gproduct]
sdprodEY [in mathcomp.fingroup.gproduct]
sdprodg1 [in mathcomp.fingroup.gproduct]
sdprodJ [in mathcomp.fingroup.gproduct]
sdprodmE [in mathcomp.fingroup.gproduct]
sdprodmEl [in mathcomp.fingroup.gproduct]
sdprodmEr [in mathcomp.fingroup.gproduct]
sdprodm_eqf [in mathcomp.fingroup.gproduct]
sdprodm_sub [in mathcomp.fingroup.gproduct]
sdprodm_norm [in mathcomp.fingroup.gproduct]
sdprodP [in mathcomp.fingroup.gproduct]
sdprodW [in mathcomp.fingroup.gproduct]
sdprodWC [in mathcomp.fingroup.gproduct]
sdprodWpp [in mathcomp.fingroup.gproduct]
sdprodWY [in mathcomp.fingroup.gproduct]
sdprod_cfker [in mathcomp.character.classfun]
sdprod_p'core_HallP [in mathcomp.solvable.pgroup]
sdprod_Hall_p'coreP [in mathcomp.solvable.pgroup]
sdprod_pcore_HallP [in mathcomp.solvable.pgroup]
sdprod_Hall_pcoreP [in mathcomp.solvable.pgroup]
sdprod_normal_pHallP [in mathcomp.solvable.pgroup]
sdprod_normal_p'HallP [in mathcomp.solvable.pgroup]
sdprod_Hall [in mathcomp.solvable.pgroup]
sdprod_sdpair [in mathcomp.fingroup.gproduct]
sdprod_mulgA [in mathcomp.fingroup.gproduct]
sdprod_mulVg [in mathcomp.fingroup.gproduct]
sdprod_mul1g [in mathcomp.fingroup.gproduct]
sdprod_mul_proof [in mathcomp.fingroup.gproduct]
sdprod_inv_proof [in mathcomp.fingroup.gproduct]
sdprod_recr [in mathcomp.fingroup.gproduct]
sdprod_recl [in mathcomp.fingroup.gproduct]
sdprod_modr [in mathcomp.fingroup.gproduct]
sdprod_modl [in mathcomp.fingroup.gproduct]
sdprod_subr [in mathcomp.fingroup.gproduct]
sdprod_isog [in mathcomp.fingroup.gproduct]
sdprod_isom [in mathcomp.fingroup.gproduct]
sdprod_card [in mathcomp.fingroup.gproduct]
sdprod_normal_complP [in mathcomp.fingroup.gproduct]
sdprod_compl [in mathcomp.fingroup.gproduct]
sdprod_context [in mathcomp.fingroup.gproduct]
sdprod_Res_IirrK [in mathcomp.character.character]
sdprod_Res_IirrE [in mathcomp.character.character]
sdprod_Iirr0 [in mathcomp.character.character]
sdprod_Iirr_eq0 [in mathcomp.character.character]
sdprod_Iirr_inj [in mathcomp.character.character]
sdprod_IirrK [in mathcomp.character.character]
sdprod_IirrE [in mathcomp.character.character]
sdprod1g [in mathcomp.fingroup.gproduct]
sd1_inv [in mathcomp.solvable.burnside_app]
Sd1_inj [in mathcomp.solvable.burnside_app]
sd2_inv [in mathcomp.solvable.burnside_app]
Sd2_inj [in mathcomp.solvable.burnside_app]
second_isog [in mathcomp.fingroup.quotient]
second_isom [in mathcomp.fingroup.quotient]
second_orthogonality_relation [in mathcomp.character.character]
section_repr_isog [in mathcomp.solvable.jordanholder]
section_reprP [in mathcomp.solvable.jordanholder]
section_eqmx [in mathcomp.character.mxrepresentation]
section_eqmx_add [in mathcomp.character.mxrepresentation]
section_module [in mathcomp.character.mxrepresentation]
semidihedral_classP [in mathcomp.solvable.extremal]
semidihedral_structure [in mathcomp.solvable.extremal]
semiprimeJ [in mathcomp.solvable.frobenius]
semiprimeS [in mathcomp.solvable.frobenius]
semiprime_regular [in mathcomp.solvable.frobenius]
semiregularJ [in mathcomp.solvable.frobenius]
semiregularS [in mathcomp.solvable.frobenius]
semiregular_prime [in mathcomp.solvable.frobenius]
semiregular_sym [in mathcomp.solvable.frobenius]
semiregular1l [in mathcomp.solvable.frobenius]
semiregular1r [in mathcomp.solvable.frobenius]
semisimple_Socle [in mathcomp.character.mxrepresentation]
separableP [in mathcomp.field.separable]
separablePn [in mathcomp.field.separable]
separableS [in mathcomp.field.separable]
separableSl [in mathcomp.field.separable]
separableSr [in mathcomp.field.separable]
separable_Xn_sub_1 [in mathcomp.field.cyclotomic]
separable_Fadjoin_seq [in mathcomp.field.separable]
separable_trans [in mathcomp.field.separable]
separable_refl [in mathcomp.field.separable]
separable_generator_maximal [in mathcomp.field.separable]
separable_generatorP [in mathcomp.field.separable]
separable_generator_mem [in mathcomp.field.separable]
separable_inseparable_decomposition [in mathcomp.field.separable]
separable_sum [in mathcomp.field.separable]
separable_add [in mathcomp.field.separable]
separable_inseparable_element [in mathcomp.field.separable]
separable_exponent [in mathcomp.field.separable]
separable_elementS [in mathcomp.field.separable]
separable_root_der [in mathcomp.field.separable]
separable_nz_der [in mathcomp.field.separable]
separable_elementP [in mathcomp.field.separable]
separable_map [in mathcomp.field.separable]
separable_prod_XsubC [in mathcomp.field.separable]
separable_root [in mathcomp.field.separable]
separable_mul [in mathcomp.field.separable]
separable_deriv_eq0 [in mathcomp.field.separable]
separable_nosquare [in mathcomp.field.separable]
separable_coprime [in mathcomp.field.separable]
separable_polyP [in mathcomp.field.separable]
separable_poly_neq0 [in mathcomp.field.separable]
seqs1 [in mathcomp.solvable.burnside_app]
seqv_sub_adjoin [in mathcomp.field.falgebra]
seq_tnthP [in mathcomp.ssreflect.tuple]
seq_ind2 [in mathcomp.ssreflect.seq]
seq_choiceMixin [in mathcomp.ssreflect.choice]
seq_of_optK [in mathcomp.ssreflect.choice]
seq_subE [in mathcomp.ssreflect.fintype]
seq_sub_default [in mathcomp.ssreflect.fintype]
seq_sub_axiom [in mathcomp.ssreflect.fintype]
seq_sub_pickleK [in mathcomp.ssreflect.fintype]
seq1_basis [in mathcomp.algebra.vector]
seq1_free [in mathcomp.algebra.vector]
series_sol [in mathcomp.solvable.nilpotent]
setactE [in mathcomp.fingroup.action]
setactJ [in mathcomp.fingroup.action]
setactVin [in mathcomp.fingroup.action]
setact_orbit [in mathcomp.fingroup.action]
setact_is_action [in mathcomp.fingroup.action]
setCD [in mathcomp.ssreflect.finset]
setCI [in mathcomp.ssreflect.finset]
setCK [in mathcomp.ssreflect.finset]
setCP [in mathcomp.ssreflect.finset]
setCS [in mathcomp.ssreflect.finset]
setCT [in mathcomp.ssreflect.finset]
setCU [in mathcomp.ssreflect.finset]
setC_bigcap [in mathcomp.ssreflect.finset]
setC_bigcup [in mathcomp.ssreflect.finset]
setC_inj [in mathcomp.ssreflect.finset]
setC0 [in mathcomp.ssreflect.finset]
setC11 [in mathcomp.ssreflect.finset]
setDDl [in mathcomp.ssreflect.finset]
setDDr [in mathcomp.ssreflect.finset]
setDE [in mathcomp.ssreflect.finset]
SetDef.finsetE [in mathcomp.ssreflect.finset]
SetDef.pred_of_setE [in mathcomp.ssreflect.finset]
setDidPl [in mathcomp.ssreflect.finset]
setDIl [in mathcomp.ssreflect.finset]
setDIr [in mathcomp.ssreflect.finset]
setDP [in mathcomp.ssreflect.finset]
setDS [in mathcomp.ssreflect.finset]
setDSS [in mathcomp.ssreflect.finset]
setDT [in mathcomp.ssreflect.finset]
setDUl [in mathcomp.ssreflect.finset]
setDUr [in mathcomp.ssreflect.finset]
setDv [in mathcomp.ssreflect.finset]
setD_eq0 [in mathcomp.ssreflect.finset]
setD0 [in mathcomp.ssreflect.finset]
setD1K [in mathcomp.ssreflect.finset]
setD1P [in mathcomp.ssreflect.finset]
setD11 [in mathcomp.ssreflect.finset]
setIA [in mathcomp.ssreflect.finset]
setIAC [in mathcomp.ssreflect.finset]
setIACA [in mathcomp.ssreflect.finset]
setIC [in mathcomp.ssreflect.finset]
setICA [in mathcomp.ssreflect.finset]
setICr [in mathcomp.ssreflect.finset]
setID [in mathcomp.ssreflect.finset]
setIDA [in mathcomp.ssreflect.finset]
setIDAC [in mathcomp.ssreflect.finset]
setIdE [in mathcomp.ssreflect.finset]
setIdP [in mathcomp.ssreflect.finset]
setId2P [in mathcomp.ssreflect.finset]
setIg1 [in mathcomp.fingroup.fingroup]
setIid [in mathcomp.ssreflect.finset]
setIidPl [in mathcomp.ssreflect.finset]
setIidPr [in mathcomp.ssreflect.finset]
setIIl [in mathcomp.ssreflect.finset]
setIIr [in mathcomp.ssreflect.finset]
setIK [in mathcomp.ssreflect.finset]
setIP [in mathcomp.ssreflect.finset]
setIS [in mathcomp.ssreflect.finset]
setISS [in mathcomp.ssreflect.finset]
setIT [in mathcomp.ssreflect.finset]
setIUl [in mathcomp.ssreflect.finset]
setIUr [in mathcomp.ssreflect.finset]
setI_transversal_pblock [in mathcomp.ssreflect.finset]
setI_eq0 [in mathcomp.ssreflect.finset]
setI_powerset [in mathcomp.ssreflect.finset]
setI_normal_Hall [in mathcomp.solvable.pgroup]
setI_subnormal [in mathcomp.solvable.gseries]
setI_im_cpair [in mathcomp.solvable.center]
setI0 [in mathcomp.ssreflect.finset]
setI1g [in mathcomp.fingroup.fingroup]
setKI [in mathcomp.ssreflect.finset]
setKU [in mathcomp.ssreflect.finset]
setP [in mathcomp.ssreflect.finset]
setSD [in mathcomp.ssreflect.finset]
setSI [in mathcomp.ssreflect.finset]
setSU [in mathcomp.ssreflect.finset]
setTD [in mathcomp.ssreflect.finset]
setTI [in mathcomp.ssreflect.finset]
setTU [in mathcomp.ssreflect.finset]
setUA [in mathcomp.ssreflect.finset]
setUAC [in mathcomp.ssreflect.finset]
setUACA [in mathcomp.ssreflect.finset]
setUC [in mathcomp.ssreflect.finset]
setUCA [in mathcomp.ssreflect.finset]
setUCr [in mathcomp.ssreflect.finset]
setUid [in mathcomp.ssreflect.finset]
setUidPl [in mathcomp.ssreflect.finset]
setUidPr [in mathcomp.ssreflect.finset]
setUIl [in mathcomp.ssreflect.finset]
setUIr [in mathcomp.ssreflect.finset]
setUK [in mathcomp.ssreflect.finset]
setUP [in mathcomp.ssreflect.finset]
setUS [in mathcomp.ssreflect.finset]
setUSS [in mathcomp.ssreflect.finset]
setUT [in mathcomp.ssreflect.finset]
setUUl [in mathcomp.ssreflect.finset]
setUUr [in mathcomp.ssreflect.finset]
setU_eq0 [in mathcomp.ssreflect.finset]
setU0 [in mathcomp.ssreflect.finset]
setU1K [in mathcomp.ssreflect.finset]
setU1P [in mathcomp.ssreflect.finset]
setU1r [in mathcomp.ssreflect.finset]
setU11 [in mathcomp.ssreflect.finset]
setXP [in mathcomp.ssreflect.finset]
setXS [in mathcomp.ssreflect.finset]
setX_gen [in mathcomp.fingroup.gproduct]
setX_dprod [in mathcomp.fingroup.gproduct]
setX_prod [in mathcomp.fingroup.gproduct]
set_gring_classM_coef [in mathcomp.character.integral_char]
set_nth_default [in mathcomp.ssreflect.seq]
set_nthE [in mathcomp.ssreflect.seq]
set_set_nth [in mathcomp.ssreflect.seq]
set_nth_nil [in mathcomp.ssreflect.seq]
set_partition_big [in mathcomp.ssreflect.finset]
set_partition_big_cond [in mathcomp.ssreflect.finset]
set_cons [in mathcomp.ssreflect.finset]
set_seq1 [in mathcomp.ssreflect.finset]
set_nil [in mathcomp.ssreflect.finset]
set_enum [in mathcomp.ssreflect.finset]
set_0Vmem [in mathcomp.ssreflect.finset]
set_invgM [in mathcomp.fingroup.fingroup]
set_invgK [in mathcomp.fingroup.fingroup]
set_mulgA [in mathcomp.fingroup.fingroup]
set_mul1g [in mathcomp.fingroup.fingroup]
set_Frobenius_compl [in mathcomp.solvable.frobenius]
set0D [in mathcomp.ssreflect.finset]
set0I [in mathcomp.ssreflect.finset]
set0Pn [in mathcomp.ssreflect.finset]
set0U [in mathcomp.ssreflect.finset]
set1gE [in mathcomp.fingroup.fingroup]
set1gP [in mathcomp.fingroup.fingroup]
set1P [in mathcomp.ssreflect.finset]
set1Ul [in mathcomp.ssreflect.finset]
set1Ur [in mathcomp.ssreflect.finset]
set1_inj [in mathcomp.ssreflect.finset]
set11 [in mathcomp.ssreflect.finset]
set2P [in mathcomp.ssreflect.finset]
set21 [in mathcomp.ssreflect.finset]
set22 [in mathcomp.ssreflect.finset]
sgrEz [in mathcomp.algebra.ssrint]
sgrMz [in mathcomp.algebra.ssrint]
sgrz [in mathcomp.algebra.ssrint]
sgr_numq [in mathcomp.algebra.rat]
sgr_numq_div [in mathcomp.algebra.rat]
sgr_denq [in mathcomp.algebra.rat]
sgr_scalq [in mathcomp.algebra.rat]
sgvalK [in mathcomp.fingroup.fingroup]
sgvalM [in mathcomp.fingroup.fingroup]
sgvalmK [in mathcomp.fingroup.morphism]
sgval_sub [in mathcomp.fingroup.morphism]
sgzM [in mathcomp.algebra.ssrint]
sgzN [in mathcomp.algebra.ssrint]
sgzN1 [in mathcomp.algebra.ssrint]
sgzP [in mathcomp.algebra.ssrint]
sgzX [in mathcomp.algebra.ssrint]
sgz_lead_primitive [in mathcomp.algebra.intdiv]
sgz_contents [in mathcomp.algebra.intdiv]
sgz_eq [in mathcomp.algebra.ssrint]
sgz_smul [in mathcomp.algebra.ssrint]
sgz_le0 [in mathcomp.algebra.ssrint]
sgz_ge0 [in mathcomp.algebra.ssrint]
sgz_lt0 [in mathcomp.algebra.ssrint]
sgz_gt0 [in mathcomp.algebra.ssrint]
sgz_odd [in mathcomp.algebra.ssrint]
sgz_eq0 [in mathcomp.algebra.ssrint]
sgz_cp0 [in mathcomp.algebra.ssrint]
sgz_id [in mathcomp.algebra.ssrint]
sgz_int [in mathcomp.algebra.ssrint]
sgz_sgr [in mathcomp.algebra.ssrint]
sgz_def [in mathcomp.algebra.ssrint]
sgz0 [in mathcomp.algebra.ssrint]
sgz1 [in mathcomp.algebra.ssrint]
shape_rev [in mathcomp.ssreflect.seq]
shortenP [in mathcomp.ssreflect.path]
sh_inv [in mathcomp.solvable.burnside_app]
Sh_inj [in mathcomp.solvable.burnside_app]
signr_scalq [in mathcomp.algebra.rat]
sigW [in mathcomp.ssreflect.choice]
sig_eqW [in mathcomp.ssreflect.choice]
sig_big_dep [in mathcomp.ssreflect.bigop]
sig_big_dep_idem [in mathcomp.ssreflect.bigop]
sig2W [in mathcomp.ssreflect.choice]
sig2_eqW [in mathcomp.ssreflect.choice]
simmxLR [in mathcomp.algebra.mxpoly]
simmxP [in mathcomp.algebra.mxpoly]
simmxPp [in mathcomp.algebra.mxpoly]
simmxRL [in mathcomp.algebra.mxpoly]
simmxW [in mathcomp.algebra.mxpoly]
simmx_minpoly [in mathcomp.algebra.mxpoly]
simpleP [in mathcomp.solvable.gseries]
simple_Alt5 [in mathcomp.solvable.alt]
simple_Alt5_base [in mathcomp.solvable.alt]
simple_Alt_3 [in mathcomp.solvable.alt]
simple_compsP [in mathcomp.solvable.jordanholder]
simple_Socle [in mathcomp.character.mxrepresentation]
simple_maxnormal [in mathcomp.solvable.gseries]
simple_sol_prime [in mathcomp.solvable.maximal]
sizeYE [in mathcomp.algebra.polyXY]
sizeY_mulX [in mathcomp.algebra.polyXY]
sizeY_eq0 [in mathcomp.algebra.polyXY]
size_rat_int_poly [in mathcomp.algebra.intdiv]
size_zprimitive [in mathcomp.algebra.intdiv]
size_widen_bseq [in mathcomp.ssreflect.tuple]
size_cast_bseq [in mathcomp.ssreflect.tuple]
size_insub_bseq [in mathcomp.ssreflect.tuple]
size_bseq [in mathcomp.ssreflect.tuple]
size_tuple [in mathcomp.ssreflect.tuple]
size_Cyclotomic [in mathcomp.field.cyclotomic]
size_cyclotomic [in mathcomp.field.cyclotomic]
size_permutations [in mathcomp.ssreflect.seq]
size_tally_seq [in mathcomp.ssreflect.seq]
size_allpairs [in mathcomp.ssreflect.seq]
size_allpairs_dep [in mathcomp.ssreflect.seq]
size_suffix [in mathcomp.ssreflect.seq]
size_prefix [in mathcomp.ssreflect.seq]
size_infix [in mathcomp.ssreflect.seq]
size_reshape [in mathcomp.ssreflect.seq]
size_flatten [in mathcomp.ssreflect.seq]
size_zip [in mathcomp.ssreflect.seq]
size_scanl [in mathcomp.ssreflect.seq]
size_pairmap [in mathcomp.ssreflect.seq]
size_mkseq [in mathcomp.ssreflect.seq]
size_iota [in mathcomp.ssreflect.seq]
size_pmap_sub [in mathcomp.ssreflect.seq]
size_pmap [in mathcomp.ssreflect.seq]
size_map [in mathcomp.ssreflect.seq]
size_rem [in mathcomp.ssreflect.seq]
size_subseq_leqif [in mathcomp.ssreflect.seq]
size_subseq [in mathcomp.ssreflect.seq]
size_mask [in mathcomp.ssreflect.seq]
size_rotr [in mathcomp.ssreflect.seq]
size_incr_nth [in mathcomp.ssreflect.seq]
size_undup [in mathcomp.ssreflect.seq]
size_eq0 [in mathcomp.ssreflect.seq]
size_rev [in mathcomp.ssreflect.seq]
size_rot [in mathcomp.ssreflect.seq]
size_take_min [in mathcomp.ssreflect.seq]
size_take [in mathcomp.ssreflect.seq]
size_takel [in mathcomp.ssreflect.seq]
size_drop [in mathcomp.ssreflect.seq]
size_filter [in mathcomp.ssreflect.seq]
size_set_nth [in mathcomp.ssreflect.seq]
size_belast [in mathcomp.ssreflect.seq]
size_rcons [in mathcomp.ssreflect.seq]
size_cat [in mathcomp.ssreflect.seq]
size_nseq [in mathcomp.ssreflect.seq]
size_ncons [in mathcomp.ssreflect.seq]
size_behead [in mathcomp.ssreflect.seq]
size_minCpoly [in mathcomp.field.algC]
size_minPoly [in mathcomp.field.fieldext]
size_Fadjoin_poly [in mathcomp.field.fieldext]
size_mod_mxminpoly [in mathcomp.algebra.mxpoly]
size_mxminpoly [in mathcomp.algebra.mxpoly]
size_char_poly [in mathcomp.algebra.mxpoly]
size_cfclass [in mathcomp.character.inertia]
size_traject [in mathcomp.ssreflect.path]
size_sort [in mathcomp.ssreflect.path]
size_merge_sort_push [in mathcomp.ssreflect.path]
size_merge [in mathcomp.ssreflect.path]
size_poly_XmY [in mathcomp.algebra.polyXY]
size_poly_XaY [in mathcomp.algebra.polyXY]
size_abelian_type [in mathcomp.solvable.abelian]
size_orbit [in mathcomp.ssreflect.fingraph]
size_basis [in mathcomp.algebra.vector]
size_enum_ord [in mathcomp.ssreflect.fintype]
size_codom [in mathcomp.ssreflect.fintype]
size_image [in mathcomp.ssreflect.fintype]
size_map_poly [in mathcomp.algebra.poly]
size_comp_poly2 [in mathcomp.algebra.poly]
size_comp_poly [in mathcomp.algebra.poly]
size_exp [in mathcomp.algebra.poly]
size_prod_eq1 [in mathcomp.algebra.poly]
size_prod_seq_eq1 [in mathcomp.algebra.poly]
size_mul_eq1 [in mathcomp.algebra.poly]
size_prod_seq [in mathcomp.algebra.poly]
size_prod [in mathcomp.algebra.poly]
size_Cmul [in mathcomp.algebra.poly]
size_scale [in mathcomp.algebra.poly]
size_mul [in mathcomp.algebra.poly]
size_drop_poly [in mathcomp.algebra.poly]
size_take_poly [in mathcomp.algebra.poly]
size_odd_poly_eq [in mathcomp.algebra.poly]
size_odd_poly [in mathcomp.algebra.poly]
size_even_poly_eq [in mathcomp.algebra.poly]
size_even_poly [in mathcomp.algebra.poly]
size_comp_poly_leq [in mathcomp.algebra.poly]
size_map_polyC [in mathcomp.algebra.poly]
size_map_inj_poly [in mathcomp.algebra.poly]
size_map_poly_id0 [in mathcomp.algebra.poly]
size_Xn_sub_1 [in mathcomp.algebra.poly]
size_exp_XsubC [in mathcomp.algebra.poly]
size_prod_XsubC [in mathcomp.algebra.poly]
size_Mmonic [in mathcomp.algebra.poly]
size_monicM [in mathcomp.algebra.poly]
size_mulXn [in mathcomp.algebra.poly]
size_polyXn [in mathcomp.algebra.poly]
size_XmulC [in mathcomp.algebra.poly]
size_mulX [in mathcomp.algebra.poly]
size_MXaddC [in mathcomp.algebra.poly]
size_XaddC [in mathcomp.algebra.poly]
size_XsubC [in mathcomp.algebra.poly]
size_polyX [in mathcomp.algebra.poly]
size_scale_leq [in mathcomp.algebra.poly]
size_Msign [in mathcomp.algebra.poly]
size_exp_leq [in mathcomp.algebra.poly]
size_prod_leq [in mathcomp.algebra.poly]
size_proper_mul [in mathcomp.algebra.poly]
size_mul_leq [in mathcomp.algebra.poly]
size_poly1 [in mathcomp.algebra.poly]
size_sum [in mathcomp.algebra.poly]
size_addl [in mathcomp.algebra.poly]
size_add [in mathcomp.algebra.poly]
size_opp [in mathcomp.algebra.poly]
size_polyC_leq1 [in mathcomp.algebra.poly]
size_poly1P [in mathcomp.algebra.poly]
size_poly_gt0 [in mathcomp.algebra.poly]
size_poly_leq0P [in mathcomp.algebra.poly]
size_poly_leq0 [in mathcomp.algebra.poly]
size_poly_eq0 [in mathcomp.algebra.poly]
size_poly0 [in mathcomp.algebra.poly]
size_poly_eq [in mathcomp.algebra.poly]
size_poly [in mathcomp.algebra.poly]
size_Poly [in mathcomp.algebra.poly]
size_cons_poly [in mathcomp.algebra.poly]
size_polyC [in mathcomp.algebra.poly]
size_mk_monic [in mathcomp.algebra.qpoly]
size_mk_monic_gt0 [in mathcomp.algebra.qpoly]
size_mk_monic_gt1 [in mathcomp.algebra.qpoly]
size_lagrange [in mathcomp.algebra.qpoly]
size_lagrange_ [in mathcomp.algebra.qpoly]
size_npoly0 [in mathcomp.algebra.qpoly]
size_npoly [in mathcomp.algebra.qpoly]
size0nil [in mathcomp.ssreflect.seq]
size1_zip [in mathcomp.ssreflect.seq]
size1_polyC [in mathcomp.algebra.poly]
size2_zip [in mathcomp.ssreflect.seq]
skew_field_dimS [in mathcomp.field.falgebra]
skew_field_module_dimS [in mathcomp.field.falgebra]
skew_field_module_semisimple [in mathcomp.field.falgebra]
skew_field_algid1 [in mathcomp.field.falgebra]
small_nil_class [in mathcomp.solvable.sylow]
snd_morphM [in mathcomp.fingroup.gproduct]
snd_is_scalable [in mathcomp.algebra.ssralg]
snd_is_multiplicative [in mathcomp.algebra.ssralg]
snd_is_additive [in mathcomp.algebra.ssralg]
socleP [in mathcomp.character.mxrepresentation]
socle_rsimP [in mathcomp.character.mxrepresentation]
socle_irr [in mathcomp.character.mxrepresentation]
Socle_iso [in mathcomp.character.mxrepresentation]
Socle_direct [in mathcomp.character.mxrepresentation]
Socle_semisimple [in mathcomp.character.mxrepresentation]
Socle_module [in mathcomp.character.mxrepresentation]
socle_finType_subproof [in mathcomp.character.mxrepresentation]
socle_mem [in mathcomp.character.mxrepresentation]
socle_simple [in mathcomp.character.mxrepresentation]
socle_exists [in mathcomp.character.mxrepresentation]
socle_of_Iirr_bij [in mathcomp.character.character]
socle_of_IirrK [in mathcomp.character.character]
socle_Iirr0 [in mathcomp.character.character]
solvableS [in mathcomp.solvable.nilpotent]
solvable_irr_extendible_from_det [in mathcomp.character.inertia]
solvable_has_lin_char [in mathcomp.character.character]
solvable_norm_abelem [in mathcomp.solvable.maximal]
solvable1 [in mathcomp.solvable.nilpotent]
sol_coprime_Sylow_subset [in mathcomp.solvable.hall]
sol_coprime_Sylow_trans [in mathcomp.solvable.hall]
sol_coprime_Sylow_exists [in mathcomp.solvable.hall]
sol_prime_factor_exists [in mathcomp.solvable.maximal]
sol_der1_proper [in mathcomp.solvable.nilpotent]
some_big_AC_mk_monoid [in mathcomp.ssreflect.bigop]
sop_morph [in mathcomp.solvable.burnside_app]
sop_spec [in mathcomp.solvable.burnside_app]
sop_inj [in mathcomp.solvable.burnside_app]
sortE [in mathcomp.ssreflect.path]
sortedP [in mathcomp.ssreflect.path]
sorted_subseq_sort_in [in mathcomp.ssreflect.path]
sorted_subseq_sort [in mathcomp.ssreflect.path]
sorted_mask_sort_in [in mathcomp.ssreflect.path]
sorted_mask_sort [in mathcomp.ssreflect.path]
sorted_sort_in [in mathcomp.ssreflect.path]
sorted_sort [in mathcomp.ssreflect.path]
sorted_merge [in mathcomp.ssreflect.path]
sorted_eq_in [in mathcomp.ssreflect.path]
sorted_uniq_in [in mathcomp.ssreflect.path]
sorted_leq_index [in mathcomp.ssreflect.path]
sorted_ltn_index [in mathcomp.ssreflect.path]
sorted_eq [in mathcomp.ssreflect.path]
sorted_uniq [in mathcomp.ssreflect.path]
sorted_leq_index_in [in mathcomp.ssreflect.path]
sorted_ltn_index_in [in mathcomp.ssreflect.path]
sorted_map [in mathcomp.ssreflect.path]
sorted_leq_nth [in mathcomp.ssreflect.path]
sorted_ltn_nth [in mathcomp.ssreflect.path]
sorted_filter [in mathcomp.ssreflect.path]
sorted_mask [in mathcomp.ssreflect.path]
sorted_pairwise [in mathcomp.ssreflect.path]
sorted_leq_nth_in [in mathcomp.ssreflect.path]
sorted_ltn_nth_in [in mathcomp.ssreflect.path]
sorted_filter_in [in mathcomp.ssreflect.path]
sorted_mask_in [in mathcomp.ssreflect.path]
sorted_pairwise_in [in mathcomp.ssreflect.path]
sorted_relI [in mathcomp.ssreflect.path]
sorted_divisors_ltn [in mathcomp.ssreflect.prime]
sorted_divisors [in mathcomp.ssreflect.prime]
sorted_primes [in mathcomp.ssreflect.prime]
sort_bseqP [in mathcomp.ssreflect.tuple]
sort_tupleP [in mathcomp.ssreflect.tuple]
sort_sorted_in [in mathcomp.ssreflect.path]
sort_sorted [in mathcomp.ssreflect.path]
sort_stable_in [in mathcomp.ssreflect.path]
sort_stable [in mathcomp.ssreflect.path]
sort_pairwise_stable [in mathcomp.ssreflect.path]
sort_iota_stable [in mathcomp.ssreflect.path]
sort_uniq [in mathcomp.ssreflect.path]
sort_map [in mathcomp.ssreflect.path]
span_orthogonal [in mathcomp.character.classfun]
span_bigcat [in mathcomp.algebra.vector]
span_basis [in mathcomp.algebra.vector]
span_cat [in mathcomp.algebra.vector]
span_cons [in mathcomp.algebra.vector]
span_seq1 [in mathcomp.algebra.vector]
span_nil [in mathcomp.algebra.vector]
span_def [in mathcomp.algebra.vector]
span_subvP [in mathcomp.algebra.vector]
span_key [in mathcomp.algebra.vector]
splitK [in mathcomp.ssreflect.fintype]
splitP [in mathcomp.ssreflect.path]
splitP [in mathcomp.ssreflect.fintype]
splitPl [in mathcomp.ssreflect.path]
splitPr [in mathcomp.ssreflect.path]
splitP2r [in mathcomp.ssreflect.path]
splitsP [in mathcomp.fingroup.gproduct]
splittingFieldForS [in mathcomp.field.galois]
splittingFieldP [in mathcomp.field.galois]
splittingPoly [in mathcomp.field.galois]
splitting_galoisField [in mathcomp.field.galois]
splitting_normalField [in mathcomp.field.galois]
splitting_field_normal [in mathcomp.field.galois]
splitting_cyclic_primitive_root [in mathcomp.character.mxrepresentation]
split_find [in mathcomp.ssreflect.seq]
split_find_nth [in mathcomp.ssreflect.seq]
split_ordP [in mathcomp.ssreflect.fintype]
split_subproof [in mathcomp.ssreflect.fintype]
split1 [in mathcomp.algebra.zmodp]
split1_extraspecial [in mathcomp.solvable.maximal]
sqmx_ind [in mathcomp.algebra.matrix]
sqrnB [in mathcomp.ssreflect.ssrnat]
sqrnD [in mathcomp.ssreflect.ssrnat]
sqrnD_sub [in mathcomp.ssreflect.ssrnat]
sqrn_inj [in mathcomp.ssreflect.ssrnat]
sqrn_gt0 [in mathcomp.ssreflect.ssrnat]
sqrt_cfnorm_gt0 [in mathcomp.character.classfun]
sqrt_cfnorm_eq0 [in mathcomp.character.classfun]
sqrt_cfnorm_ge0 [in mathcomp.character.classfun]
sqr_Cint_ge1 [in mathcomp.field.algC]
stable [in mathcomp.solvable.burnside_app]
stableCmx [in mathcomp.algebra.mxalgebra]
stableDmx [in mathcomp.algebra.mxalgebra]
stablemxC [in mathcomp.algebra.mxalgebra]
stablemxD [in mathcomp.algebra.mxalgebra]
stablemxM [in mathcomp.algebra.mxalgebra]
stablemxN [in mathcomp.algebra.mxalgebra]
stablemx_restrict [in mathcomp.algebra.mxpoly]
stablemx_comp [in mathcomp.algebra.mxpoly]
stablemx_unit [in mathcomp.algebra.mxalgebra]
stablemx_sums [in mathcomp.algebra.mxalgebra]
stablemx_full [in mathcomp.algebra.mxalgebra]
stablemx_row_base [in mathcomp.algebra.mxalgebra]
stablemx0 [in mathcomp.algebra.mxalgebra]
stableNmx [in mathcomp.algebra.mxalgebra]
stable_rowg_mxK [in mathcomp.character.mxabelem]
stable0mx [in mathcomp.algebra.mxalgebra]
stab_ntransitiveI [in mathcomp.solvable.primitive_action]
stab_ntransitive [in mathcomp.solvable.primitive_action]
stab_semiprime [in mathcomp.solvable.frobenius]
strict_adjunction [in mathcomp.ssreflect.fingraph]
strongest_coprime_quotient_cent [in mathcomp.solvable.hall]
StrongJordanHolderUniqueness [in mathcomp.solvable.jordanholder]
strong_Primitive_Element_Theorem [in mathcomp.field.separable]
subact_is_action [in mathcomp.fingroup.action]
subBnAC [in mathcomp.ssreflect.ssrnat]
subcentP [in mathcomp.solvable.center]
subcent_dprod [in mathcomp.fingroup.gproduct]
subcent_sdprod [in mathcomp.fingroup.gproduct]
subcent_TImulg [in mathcomp.fingroup.gproduct]
subcent_char [in mathcomp.solvable.center]
subcent_normal [in mathcomp.solvable.center]
subcent_norm [in mathcomp.solvable.center]
subcent_sub [in mathcomp.solvable.center]
subcent1C [in mathcomp.solvable.center]
subcent1P [in mathcomp.solvable.center]
subcent1_cycle_normal [in mathcomp.solvable.center]
subcent1_cycle_norm [in mathcomp.solvable.center]
subcent1_cycle_sub [in mathcomp.solvable.center]
subcent1_sub [in mathcomp.solvable.center]
subcent1_id [in mathcomp.solvable.center]
subcent1_extraspecial_maximal [in mathcomp.solvable.maximal]
subCset [in mathcomp.ssreflect.finset]
subDnAC [in mathcomp.ssreflect.ssrnat]
subDnCA [in mathcomp.ssreflect.ssrnat]
subDnCAC [in mathcomp.ssreflect.ssrnat]
subDset [in mathcomp.ssreflect.finset]
subD1set [in mathcomp.ssreflect.finset]
subEproper [in mathcomp.ssreflect.finset]
subfield_closed [in mathcomp.field.fieldext]
subfxE [in mathcomp.field.fieldext]
subfxEroot [in mathcomp.field.fieldext]
subfx_irreducibleP [in mathcomp.field.fieldext]
subfx_inj_base [in mathcomp.field.fieldext]
subfx_injZ [in mathcomp.field.fieldext]
subfx_inj_root [in mathcomp.field.fieldext]
subfx_inj_eval [in mathcomp.field.fieldext]
subfx_evalZ [in mathcomp.field.fieldext]
subfx_scaleAr [in mathcomp.field.fieldext]
subfx_scaleAl [in mathcomp.field.fieldext]
subfx_scalerDl [in mathcomp.field.fieldext]
subfx_scalerDr [in mathcomp.field.fieldext]
subfx_scaler1r [in mathcomp.field.fieldext]
subfx_scalerA [in mathcomp.field.fieldext]
subfx_eval_is_rmorphism [in mathcomp.field.fieldext]
subfx_inj_is_rmorphism [in mathcomp.field.fieldext]
subfx_inv0 [in mathcomp.field.fieldext]
subfx_fieldAxiom [in mathcomp.field.fieldext]
subgacentE [in mathcomp.fingroup.action]
subgacent1E [in mathcomp.fingroup.action]
subGcfker [in mathcomp.character.character]
subgK [in mathcomp.fingroup.fingroup]
subgM [in mathcomp.fingroup.fingroup]
subgmK [in mathcomp.fingroup.morphism]
subgP [in mathcomp.fingroup.fingroup]
subgroup_transitiveP [in mathcomp.fingroup.action]
subgroup_transitivePin [in mathcomp.fingroup.action]
subg_default [in mathcomp.fingroup.fingroup]
subg_mulP [in mathcomp.fingroup.fingroup]
subg_invP [in mathcomp.fingroup.fingroup]
subg_oneP [in mathcomp.fingroup.fingroup]
subg_inj [in mathcomp.fingroup.fingroup]
subg_mx_abs_irr [in mathcomp.character.mxrepresentation]
subg_mx_irr [in mathcomp.character.mxrepresentation]
subg_mx_faithful [in mathcomp.character.mxrepresentation]
subg_mx_repr [in mathcomp.character.mxrepresentation]
subG1 [in mathcomp.fingroup.fingroup]
subG1_contra [in mathcomp.fingroup.fingroup]
subHall_Sylow [in mathcomp.solvable.pgroup]
subHall_Hall [in mathcomp.solvable.pgroup]
subIset [in mathcomp.ssreflect.finset]
subitvE [in mathcomp.algebra.interval]
subitvP [in mathcomp.algebra.interval]
subitvPl [in mathcomp.algebra.interval]
subitvPr [in mathcomp.algebra.interval]
subitv_trans [in mathcomp.algebra.interval]
subitv_anti [in mathcomp.algebra.interval]
subitv_refl [in mathcomp.algebra.interval]
SubK [in mathcomp.ssreflect.eqtype]
subKn [in mathcomp.ssreflect.ssrnat]
submod_mx_irr [in mathcomp.character.mxrepresentation]
submod_mx_faithful [in mathcomp.character.mxrepresentation]
submod_mx_repr [in mathcomp.character.mxrepresentation]
submxblockB [in mathcomp.algebra.matrix]
submxblockD [in mathcomp.algebra.matrix]
submxblockEh [in mathcomp.algebra.matrix]
submxblockEv [in mathcomp.algebra.matrix]
submxblockK [in mathcomp.algebra.matrix]
submxblockN [in mathcomp.algebra.matrix]
submxblock_diag [in mathcomp.algebra.matrix]
submxblock_sum [in mathcomp.algebra.matrix]
submxblock0 [in mathcomp.algebra.matrix]
submxcolB [in mathcomp.algebra.matrix]
submxcolD [in mathcomp.algebra.matrix]
submxcolK [in mathcomp.algebra.matrix]
submxcolN [in mathcomp.algebra.matrix]
submxcol_mul [in mathcomp.algebra.matrix]
submxcol_sum [in mathcomp.algebra.matrix]
submxcol_matrix [in mathcomp.algebra.matrix]
submxcol0 [in mathcomp.algebra.matrix]
submxE [in mathcomp.algebra.mxalgebra]
submxElt [in mathcomp.algebra.mxalgebra]
submxK [in mathcomp.algebra.matrix]
submxMfree [in mathcomp.algebra.mxalgebra]
submxMl [in mathcomp.algebra.mxalgebra]
submxMr [in mathcomp.algebra.mxalgebra]
submxP [in mathcomp.algebra.mxalgebra]
submxrowB [in mathcomp.algebra.matrix]
submxrowD [in mathcomp.algebra.matrix]
submxrowK [in mathcomp.algebra.matrix]
submxrowN [in mathcomp.algebra.matrix]
submxrow_sum [in mathcomp.algebra.matrix]
submxrow_matrix [in mathcomp.algebra.matrix]
submxrow0 [in mathcomp.algebra.matrix]
submx_rowsub [in mathcomp.algebra.mxalgebra]
submx_full [in mathcomp.algebra.mxalgebra]
submx_trans [in mathcomp.algebra.mxalgebra]
submx_refl [in mathcomp.algebra.mxalgebra]
submx_key [in mathcomp.algebra.mxalgebra]
submx0 [in mathcomp.algebra.mxalgebra]
submx0null [in mathcomp.algebra.mxalgebra]
submx1 [in mathcomp.algebra.mxalgebra]
subnA [in mathcomp.ssreflect.ssrnat]
subnAC [in mathcomp.ssreflect.ssrnat]
subnBA [in mathcomp.ssreflect.ssrnat]
subnBAC [in mathcomp.ssreflect.ssrnat]
subnBl_leq [in mathcomp.ssreflect.ssrnat]
subnBr_leq [in mathcomp.ssreflect.ssrnat]
subnCBA [in mathcomp.ssreflect.ssrnat]
subnDA [in mathcomp.ssreflect.ssrnat]
subnDAC [in mathcomp.ssreflect.ssrnat]
subnDl [in mathcomp.ssreflect.ssrnat]
subnDr [in mathcomp.ssreflect.ssrnat]
subnE [in mathcomp.ssreflect.ssrnat]
subnK [in mathcomp.ssreflect.ssrnat]
subnKC [in mathcomp.ssreflect.ssrnat]
subnn [in mathcomp.ssreflect.ssrnat]
subnormalEl [in mathcomp.solvable.gseries]
subnormalEr [in mathcomp.solvable.gseries]
subnormalEsupport [in mathcomp.solvable.gseries]
subnormalP [in mathcomp.solvable.gseries]
subnormal_sub [in mathcomp.solvable.gseries]
subnormal_trans [in mathcomp.solvable.gseries]
subnormal_refl [in mathcomp.solvable.gseries]
subnS [in mathcomp.ssreflect.ssrnat]
subnSK [in mathcomp.ssreflect.ssrnat]
subn_exp [in mathcomp.ssreflect.binomial]
subn_sqr [in mathcomp.ssreflect.ssrnat]
subn_if_gt [in mathcomp.ssreflect.ssrnat]
subn_minl [in mathcomp.ssreflect.ssrnat]
subn_maxl [in mathcomp.ssreflect.ssrnat]
subn_eq0 [in mathcomp.ssreflect.ssrnat]
subn_gt0 [in mathcomp.ssreflect.ssrnat]
subn0 [in mathcomp.ssreflect.ssrnat]
subn1 [in mathcomp.ssreflect.ssrnat]
subn2 [in mathcomp.ssreflect.ssrnat]
SubP [in mathcomp.ssreflect.eqtype]
subq_ge0 [in mathcomp.algebra.rat]
subseqP [in mathcomp.ssreflect.seq]
subseq_pairwise [in mathcomp.ssreflect.seq]
subseq_rem [in mathcomp.ssreflect.seq]
subseq_uniqP [in mathcomp.ssreflect.seq]
subseq_filter [in mathcomp.ssreflect.seq]
subseq_rot [in mathcomp.ssreflect.seq]
subseq_cat2r [in mathcomp.ssreflect.seq]
subseq_cat2l [in mathcomp.ssreflect.seq]
subseq_rev [in mathcomp.ssreflect.seq]
subseq_uniq [in mathcomp.ssreflect.seq]
subseq_rcons [in mathcomp.ssreflect.seq]
subseq_cons [in mathcomp.ssreflect.seq]
subseq_anti [in mathcomp.ssreflect.seq]
subseq_trans [in mathcomp.ssreflect.seq]
subseq_refl [in mathcomp.ssreflect.seq]
subseq_sort_in [in mathcomp.ssreflect.path]
subseq_sort [in mathcomp.ssreflect.path]
subseq_sorted [in mathcomp.ssreflect.path]
subseq_path [in mathcomp.ssreflect.path]
subseq_sorted_in [in mathcomp.ssreflect.path]
subseq_path_in [in mathcomp.ssreflect.path]
subseq0 [in mathcomp.ssreflect.seq]
subsetC [in mathcomp.ssreflect.finset]
subsetD [in mathcomp.ssreflect.finset]
subsetDl [in mathcomp.ssreflect.finset]
subsetDP [in mathcomp.ssreflect.finset]
subsetDr [in mathcomp.ssreflect.finset]
subsetD1 [in mathcomp.ssreflect.finset]
subsetD1P [in mathcomp.ssreflect.finset]
subsetE [in mathcomp.ssreflect.fintype]
subsetI [in mathcomp.ssreflect.finset]
subsetIidl [in mathcomp.ssreflect.finset]
subsetIidr [in mathcomp.ssreflect.finset]
subsetIl [in mathcomp.ssreflect.finset]
subsetIP [in mathcomp.ssreflect.finset]
subsetIr [in mathcomp.ssreflect.finset]
subsetP [in mathcomp.ssreflect.fintype]
subsetPn [in mathcomp.ssreflect.fintype]
subsets_disjoint [in mathcomp.ssreflect.finset]
subsetT [in mathcomp.ssreflect.finset]
subsetT_hint [in mathcomp.ssreflect.finset]
subsetU [in mathcomp.ssreflect.finset]
subsetUl [in mathcomp.ssreflect.finset]
subsetUr [in mathcomp.ssreflect.finset]
subsetU1 [in mathcomp.ssreflect.finset]
subset_itv_co_cc [in mathcomp.algebra.interval]
subset_itv_oc_cc [in mathcomp.algebra.interval]
subset_itv_oo_co [in mathcomp.algebra.interval]
subset_itv_oo_oc [in mathcomp.algebra.interval]
subset_itv_oo_cc [in mathcomp.algebra.interval]
subset_itv [in mathcomp.algebra.interval]
subset_mapP [in mathcomp.ssreflect.seq]
subset_iter [in mathcomp.ssreflect.finset]
subset_iterS [in mathcomp.ssreflect.finset]
subset_le_big_cond [in mathcomp.ssreflect.finset]
subset_neq0 [in mathcomp.ssreflect.finset]
subset_leqif_cards [in mathcomp.ssreflect.finset]
subset_faithful [in mathcomp.fingroup.action]
subset_gen [in mathcomp.fingroup.fingroup]
subset_closure [in mathcomp.ssreflect.fingraph]
subset_dfs [in mathcomp.ssreflect.fingraph]
subset_disjoint [in mathcomp.ssreflect.fintype]
subset_filter [in mathcomp.ssreflect.fintype]
subset_cat2 [in mathcomp.ssreflect.fintype]
subset_catr [in mathcomp.ssreflect.fintype]
subset_catl [in mathcomp.ssreflect.fintype]
subset_cons2 [in mathcomp.ssreflect.fintype]
subset_cons [in mathcomp.ssreflect.fintype]
subset_all [in mathcomp.ssreflect.fintype]
subset_trans [in mathcomp.ssreflect.fintype]
subset_leqif_card [in mathcomp.ssreflect.fintype]
subset_cardP [in mathcomp.ssreflect.fintype]
subset_eqP [in mathcomp.ssreflect.fintype]
subset_pred1 [in mathcomp.ssreflect.fintype]
subset_predT [in mathcomp.ssreflect.fintype]
subset_leq_card [in mathcomp.ssreflect.fintype]
subset_le_big [in mathcomp.ssreflect.bigop]
subset0 [in mathcomp.ssreflect.finset]
subset1 [in mathcomp.ssreflect.finset]
subSKn [in mathcomp.ssreflect.ssrnat]
subSn [in mathcomp.ssreflect.ssrnat]
subSnn [in mathcomp.ssreflect.ssrnat]
subSocle_direct [in mathcomp.character.mxrepresentation]
subSocle_iso [in mathcomp.character.mxrepresentation]
subSocle_semisimple [in mathcomp.character.mxrepresentation]
subSocle_module [in mathcomp.character.mxrepresentation]
subSS [in mathcomp.ssreflect.ssrnat]
subTset [in mathcomp.ssreflect.finset]
subUset [in mathcomp.ssreflect.finset]
subUsetP [in mathcomp.ssreflect.finset]
subvf [in mathcomp.algebra.vector]
subvP [in mathcomp.algebra.vector]
subvPn [in mathcomp.algebra.vector]
subvP_adjoin [in mathcomp.field.falgebra]
subvsP [in mathcomp.algebra.vector]
subvs_fieldMixin [in mathcomp.field.fieldext]
subvs_vect_iso [in mathcomp.algebra.vector]
subvs_inj [in mathcomp.algebra.vector]
subvs_scaleAr [in mathcomp.field.falgebra]
subvs_scaleAl [in mathcomp.field.falgebra]
subvs_mulDr [in mathcomp.field.falgebra]
subvs_mulDl [in mathcomp.field.falgebra]
subvs_mul1 [in mathcomp.field.falgebra]
subvs_mu1l [in mathcomp.field.falgebra]
subvs_mulA [in mathcomp.field.falgebra]
subvv [in mathcomp.algebra.vector]
subv_bigcapP [in mathcomp.algebra.vector]
subv_cap [in mathcomp.algebra.vector]
subv_sumP [in mathcomp.algebra.vector]
subv_add [in mathcomp.algebra.vector]
subv_anti [in mathcomp.algebra.vector]
subv_trans [in mathcomp.algebra.vector]
subv_adjoin_seq [in mathcomp.field.falgebra]
subv_adjoin [in mathcomp.field.falgebra]
subv_cent1 [in mathcomp.field.falgebra]
subv0 [in mathcomp.algebra.vector]
subxx [in mathcomp.ssreflect.fintype]
subxx_hint [in mathcomp.ssreflect.fintype]
subX_agenv [in mathcomp.field.falgebra]
subzn [in mathcomp.algebra.ssrint]
subzSS [in mathcomp.algebra.ssrint]
sub_cosetpre_quo [in mathcomp.fingroup.quotient]
sub_quotient_pre [in mathcomp.fingroup.quotient]
sub_cosetpre [in mathcomp.fingroup.quotient]
sub_im_coset [in mathcomp.fingroup.quotient]
sub_conjC_vchar [in mathcomp.character.vcharacter]
sub_aut_zchar [in mathcomp.character.vcharacter]
sub_pairwise [in mathcomp.ssreflect.seq]
sub_in_pairwise [in mathcomp.ssreflect.seq]
sub_allrel [in mathcomp.ssreflect.seq]
sub_in_allrel [in mathcomp.ssreflect.seq]
sub_map [in mathcomp.ssreflect.seq]
sub_all [in mathcomp.ssreflect.seq]
sub_count [in mathcomp.ssreflect.seq]
sub_has [in mathcomp.ssreflect.seq]
sub_find [in mathcomp.ssreflect.seq]
sub_der1_abelian [in mathcomp.solvable.commutator]
sub_der1_normal [in mathcomp.solvable.commutator]
sub_der1_norm [in mathcomp.solvable.commutator]
sub_Zp_1 [in mathcomp.algebra.zmodp]
sub_imset_pre [in mathcomp.ssreflect.finset]
sub_baseField [in mathcomp.field.fieldext]
sub_adjoin1v [in mathcomp.field.fieldext]
sub_adjoin_separable_generator [in mathcomp.field.separable]
sub_inseparable [in mathcomp.field.separable]
sub_eigenspace_conjmx [in mathcomp.algebra.mxpoly]
sub_kermxpoly_conjmx [in mathcomp.algebra.mxpoly]
sub_inertia_Ind [in mathcomp.character.inertia]
sub_inertia_Res [in mathcomp.character.inertia]
sub_Inertia [in mathcomp.character.inertia]
sub_inertia [in mathcomp.character.inertia]
sub_astabQR [in mathcomp.fingroup.action]
sub_astabQ [in mathcomp.fingroup.action]
sub_afixRs_norm [in mathcomp.fingroup.action]
sub_afixRs_norms [in mathcomp.fingroup.action]
sub_act_proof [in mathcomp.fingroup.action]
sub_astab1 [in mathcomp.fingroup.action]
sub_astab1_in [in mathcomp.fingroup.action]
sub_cfker_mod [in mathcomp.character.classfun]
sub_morphim_cfker [in mathcomp.character.classfun]
sub_cfker_morph [in mathcomp.character.classfun]
sub_cfker_Res [in mathcomp.character.classfun]
sub_iso_to [in mathcomp.character.classfun]
sub_orthonormal [in mathcomp.character.classfun]
sub_pairwise_orthogonal [in mathcomp.character.classfun]
sub_abelem_rV_im [in mathcomp.character.mxabelem]
sub_rVabelem_im [in mathcomp.character.mxabelem]
sub_rVabelem [in mathcomp.character.mxabelem]
sub_im_abelem_rV [in mathcomp.character.mxabelem]
sub_rowg_mx [in mathcomp.character.mxabelem]
sub_abelian_normal [in mathcomp.fingroup.fingroup]
sub_abelian_norm [in mathcomp.fingroup.fingroup]
sub_abelian_cent2 [in mathcomp.fingroup.fingroup]
sub_abelian_cent [in mathcomp.fingroup.fingroup]
sub_cent1 [in mathcomp.fingroup.fingroup]
sub_gcore [in mathcomp.fingroup.fingroup]
sub_gen [in mathcomp.fingroup.fingroup]
sub_class_support [in mathcomp.fingroup.fingroup]
sub_conjgV [in mathcomp.fingroup.fingroup]
sub_conjg [in mathcomp.fingroup.fingroup]
sub_rcosetV [in mathcomp.fingroup.fingroup]
sub_rcoset [in mathcomp.fingroup.fingroup]
sub_lcosetV [in mathcomp.fingroup.fingroup]
sub_lcoset [in mathcomp.fingroup.fingroup]
sub_nilpotent_cent2 [in mathcomp.solvable.sylow]
sub_pcore [in mathcomp.solvable.pgroup]
sub_in_pcore [in mathcomp.solvable.pgroup]
sub_Hall_pcore [in mathcomp.solvable.pgroup]
sub_normal_Hall [in mathcomp.solvable.pgroup]
sub_pHall [in mathcomp.solvable.pgroup]
sub_in_constt [in mathcomp.solvable.pgroup]
sub_p_elt [in mathcomp.solvable.pgroup]
sub_pgroup [in mathcomp.solvable.pgroup]
sub_sorted [in mathcomp.ssreflect.path]
sub_cycle [in mathcomp.ssreflect.path]
sub_path [in mathcomp.ssreflect.path]
sub_in_sorted [in mathcomp.ssreflect.path]
sub_in_cycle [in mathcomp.ssreflect.path]
sub_in_path [in mathcomp.ssreflect.path]
sub_pnat_coprime [in mathcomp.ssreflect.prime]
sub_in_pnat [in mathcomp.ssreflect.prime]
sub_in_partn [in mathcomp.ssreflect.prime]
sub_annihilant_neq0 [in mathcomp.algebra.polyXY]
sub_annihilantP [in mathcomp.algebra.polyXY]
sub_annihilant_in_ideal [in mathcomp.algebra.polyXY]
sub_Ldiv [in mathcomp.solvable.abelian]
sub_LdivT [in mathcomp.solvable.abelian]
sub_isog [in mathcomp.fingroup.morphism]
sub_isom [in mathcomp.fingroup.morphism]
sub_morphpre_injm [in mathcomp.fingroup.morphism]
sub_morphpre_im [in mathcomp.fingroup.morphism]
sub_morphim_pre [in mathcomp.fingroup.morphism]
sub_center_normal [in mathcomp.solvable.center]
sub_cyclic_char [in mathcomp.solvable.cyclic]
sub_span [in mathcomp.algebra.vector]
sub_ordK [in mathcomp.ssreflect.fintype]
sub_ord_proof [in mathcomp.ssreflect.fintype]
sub_enum_uniq [in mathcomp.ssreflect.fintype]
sub_proper_trans [in mathcomp.ssreflect.fintype]
sub_in_le_big [in mathcomp.ssreflect.bigop]
sub_le_big_seq_cond [in mathcomp.ssreflect.bigop]
sub_le_big_seq [in mathcomp.ssreflect.bigop]
sub_le_big [in mathcomp.ssreflect.bigop]
sub_agenv [in mathcomp.field.falgebra]
sub_dsumsmx [in mathcomp.algebra.mxalgebra]
sub_daddsmx [in mathcomp.algebra.mxalgebra]
sub_bigcapmxP [in mathcomp.algebra.mxalgebra]
sub_capmx [in mathcomp.algebra.mxalgebra]
sub_capmx_gen [in mathcomp.algebra.mxalgebra]
sub_kermx [in mathcomp.algebra.mxalgebra]
sub_kermxP [in mathcomp.algebra.mxalgebra]
sub_sumsmxP [in mathcomp.algebra.mxalgebra]
sub_sums_genmxP [in mathcomp.algebra.mxalgebra]
sub_addsmxP [in mathcomp.algebra.mxalgebra]
sub_rVP [in mathcomp.algebra.mxalgebra]
sub_ltmx_trans [in mathcomp.algebra.mxalgebra]
sub0mx [in mathcomp.algebra.mxalgebra]
sub0n [in mathcomp.ssreflect.ssrnat]
sub0seq [in mathcomp.ssreflect.seq]
sub0set [in mathcomp.ssreflect.finset]
sub0v [in mathcomp.algebra.vector]
sub1b [in mathcomp.ssreflect.ssrnat]
sub1G [in mathcomp.fingroup.fingroup]
sub1mx [in mathcomp.algebra.mxalgebra]
sub1seq [in mathcomp.ssreflect.seq]
sub1set [in mathcomp.ssreflect.finset]
sub1v [in mathcomp.field.fieldext]
sub1_agenv [in mathcomp.field.falgebra]
succnK [in mathcomp.ssreflect.ssrnat]
succn_inj [in mathcomp.ssreflect.ssrnat]
suffixE [in mathcomp.ssreflect.seq]
suffixP [in mathcomp.ssreflect.seq]
suffixs0 [in mathcomp.ssreflect.seq]
suffixW [in mathcomp.ssreflect.seq]
suffix_drop [in mathcomp.ssreflect.seq]
suffix_uniq [in mathcomp.ssreflect.seq]
suffix_prefix_trans [in mathcomp.ssreflect.seq]
suffix_infix_trans [in mathcomp.ssreflect.seq]
suffix_infix [in mathcomp.ssreflect.seq]
suffix_cons [in mathcomp.ssreflect.seq]
suffix_catr [in mathcomp.ssreflect.seq]
suffix_catl [in mathcomp.ssreflect.seq]
suffix_rcons [in mathcomp.ssreflect.seq]
suffix_trans [in mathcomp.ssreflect.seq]
suffix_suffix [in mathcomp.ssreflect.seq]
suffix_revLR [in mathcomp.ssreflect.seq]
suffix_rev [in mathcomp.ssreflect.seq]
suffix_refl [in mathcomp.ssreflect.seq]
suffix_subseq [in mathcomp.ssreflect.seq]
suffix_sorted [in mathcomp.ssreflect.path]
suffix0s [in mathcomp.ssreflect.seq]
suffix1s [in mathcomp.ssreflect.seq]
sumfv [in mathcomp.algebra.vector]
summxE [in mathcomp.algebra.matrix]
summx_sub_sums [in mathcomp.algebra.mxalgebra]
summx_sub [in mathcomp.algebra.mxalgebra]
sumMz [in mathcomp.algebra.ssrint]
sumnB [in mathcomp.ssreflect.bigop]
sumnE [in mathcomp.ssreflect.bigop]
sumn_flatten [in mathcomp.ssreflect.seq]
sumn_set_nth0 [in mathcomp.ssreflect.seq]
sumn_set_nth_ltn [in mathcomp.ssreflect.seq]
sumn_set_nth [in mathcomp.ssreflect.seq]
sumn_rev [in mathcomp.ssreflect.seq]
sumn_rot [in mathcomp.ssreflect.seq]
sumn_rcons [in mathcomp.ssreflect.seq]
sumn_count [in mathcomp.ssreflect.seq]
sumn_cat [in mathcomp.ssreflect.seq]
sumn_nseq [in mathcomp.ssreflect.seq]
sumn_ncons [in mathcomp.ssreflect.seq]
sumsmxMr [in mathcomp.algebra.mxalgebra]
sumsmxMr_gen [in mathcomp.algebra.mxalgebra]
sumsmxS [in mathcomp.algebra.mxalgebra]
sumsmx_semisimple [in mathcomp.character.mxrepresentation]
sumsmx_module [in mathcomp.character.mxrepresentation]
sumsmx_subP [in mathcomp.algebra.mxalgebra]
sumsmx_sup [in mathcomp.algebra.mxalgebra]
sumv_pi_nat_sum [in mathcomp.algebra.vector]
sumv_pi_sum [in mathcomp.algebra.vector]
sumv_pi_uniq_sum [in mathcomp.algebra.vector]
sumv_sup [in mathcomp.algebra.vector]
sum_norm2_char_generators [in mathcomp.character.integral_char]
sum_index_rcosets_cycle [in mathcomp.solvable.finmodule]
sum_nat_cond_const [in mathcomp.ssreflect.finset]
sum_card_class [in mathcomp.fingroup.action]
sum_by_classes [in mathcomp.character.classfun]
sum_cfunE [in mathcomp.character.classfun]
sum_irr_degree [in mathcomp.character.mxrepresentation]
sum_mxsimple_direct_sub [in mathcomp.character.mxrepresentation]
sum_mxsimple_direct_compl [in mathcomp.character.mxrepresentation]
sum_totient_dvd [in mathcomp.solvable.cyclic]
sum_ncycle_totient [in mathcomp.solvable.cyclic]
sum_ffun [in mathcomp.algebra.ssralg]
sum_ffunE [in mathcomp.algebra.ssralg]
sum_lfunE [in mathcomp.algebra.vector]
sum_norm_irr_quo [in mathcomp.character.character]
sum_enum_uniq [in mathcomp.ssreflect.fintype]
sum_drop_poly [in mathcomp.algebra.poly]
sum_odd_poly [in mathcomp.algebra.poly]
sum_even_poly [in mathcomp.algebra.poly]
sum_nat_seq_eq1 [in mathcomp.ssreflect.bigop]
sum_nat_eq1 [in mathcomp.ssreflect.bigop]
sum_nat_seq_neq0 [in mathcomp.ssreflect.bigop]
sum_nat_seq_eq0 [in mathcomp.ssreflect.bigop]
sum_nat_eq0 [in mathcomp.ssreflect.bigop]
sum_nat_const_nat [in mathcomp.ssreflect.bigop]
sum_nat_const [in mathcomp.ssreflect.bigop]
sum_eqE [in mathcomp.ssreflect.eqtype]
sum_eqP [in mathcomp.ssreflect.eqtype]
sum1dep_card [in mathcomp.ssreflect.finset]
sum1_size [in mathcomp.ssreflect.bigop]
sum1_count [in mathcomp.ssreflect.bigop]
sum1_card [in mathcomp.ssreflect.bigop]
supportE [in mathcomp.ssreflect.finfun]
supportP [in mathcomp.ssreflect.finfun]
support_zchar [in mathcomp.character.vcharacter]
support_cfAut [in mathcomp.character.classfun]
support_cfuni [in mathcomp.character.classfun]
support_cfun [in mathcomp.character.classfun]
sup_field_module [in mathcomp.field.fieldext]
sv_inv [in mathcomp.solvable.burnside_app]
Sv_inj [in mathcomp.solvable.burnside_app]
swapXYK [in mathcomp.algebra.polyXY]
swapXY_map [in mathcomp.algebra.polyXY]
swapXY_poly_XmY [in mathcomp.algebra.polyXY]
swapXY_poly_XaY [in mathcomp.algebra.polyXY]
swapXY_comp_poly [in mathcomp.algebra.polyXY]
swapXY_is_scalable [in mathcomp.algebra.polyXY]
swapXY_is_multiplicative [in mathcomp.algebra.polyXY]
swapXY_eq0 [in mathcomp.algebra.polyXY]
swapXY_map_polyC [in mathcomp.algebra.polyXY]
swapXY_is_additive [in mathcomp.algebra.polyXY]
swapXY_Y [in mathcomp.algebra.polyXY]
swapXY_X [in mathcomp.algebra.polyXY]
swapXY_polyC [in mathcomp.algebra.polyXY]
swapXY_key [in mathcomp.algebra.polyXY]
swizzle_mx_is_scalable [in mathcomp.algebra.matrix]
swizzle_mx_is_additive [in mathcomp.algebra.matrix]
SylowJ [in mathcomp.solvable.pgroup]
SylowP [in mathcomp.solvable.pgroup]
Sylow_subnorm [in mathcomp.solvable.sylow]
Sylow_gen [in mathcomp.solvable.sylow]
Sylow_transversal_gen [in mathcomp.solvable.sylow]
Sylow_setI_normal [in mathcomp.solvable.sylow]
Sylow_Jsub [in mathcomp.solvable.sylow]
Sylow_subJ [in mathcomp.solvable.sylow]
Sylow_trans [in mathcomp.solvable.sylow]
Sylow_exists [in mathcomp.solvable.sylow]
Sylow_superset [in mathcomp.solvable.sylow]
Sylow's_theorem [in mathcomp.solvable.sylow]
Sylow1 [in mathcomp.solvable.pgroup]
Sylvester_mxE [in mathcomp.algebra.mxpoly]
Syl_trans [in mathcomp.solvable.sylow]
SymE [in mathcomp.fingroup.action]
symplectic_type_group_structure [in mathcomp.solvable.extremal]
Sym_trans [in mathcomp.solvable.alt]
Sym_group_set [in mathcomp.fingroup.perm]
sym_connect_sym [in mathcomp.ssreflect.fingraph]
S0_inv [in mathcomp.solvable.burnside_app]
S05_inj [in mathcomp.solvable.burnside_app]
S1_inv [in mathcomp.solvable.burnside_app]
S14_inj [in mathcomp.solvable.burnside_app]
S2_inv [in mathcomp.solvable.burnside_app]
s23_inv [in mathcomp.solvable.burnside_app]
S23_inv [in mathcomp.solvable.burnside_app]
S3_inv [in mathcomp.solvable.burnside_app]
S4_inv [in mathcomp.solvable.burnside_app]
S5_inv [in mathcomp.solvable.burnside_app]
S6_inv [in mathcomp.solvable.burnside_app]
| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (80254 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1852 entries) |
| Binder Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (48996 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (383 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (4219 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (93 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (14738 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (223 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (45 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (132 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (452 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1431 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1169 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (6273 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (248 entries) |