| Global Index | +A | +B | +C | +D | +E | +F | +G | +H | +I | +J | +K | +L | +M | +N | +O | +P | +Q | +R | +S | +T | +U | +V | +W | +X | +Y | +Z | +_ | +other | +(23233 entries) | +
| Notation Index | +A | +B | +C | +D | +E | +F | +G | +H | +I | +J | +K | +L | +M | +N | +O | +P | +Q | +R | +S | +T | +U | +V | +W | +X | +Y | +Z | +_ | +other | +(1373 entries) | +
| Module Index | +A | +B | +C | +D | +E | +F | +G | +H | +I | +J | +K | +L | +M | +N | +O | +P | +Q | +R | +S | +T | +U | +V | +W | +X | +Y | +Z | +_ | +other | +(213 entries) | +
| Variable Index | +A | +B | +C | +D | +E | +F | +G | +H | +I | +J | +K | +L | +M | +N | +O | +P | +Q | +R | +S | +T | +U | +V | +W | +X | +Y | +Z | +_ | +other | +(3475 entries) | +
| Library Index | +A | +B | +C | +D | +E | +F | +G | +H | +I | +J | +K | +L | +M | +N | +O | +P | +Q | +R | +S | +T | +U | +V | +W | +X | +Y | +Z | +_ | +other | +(89 entries) | +
| Lemma Index | +A | +B | +C | +D | +E | +F | +G | +H | +I | +J | +K | +L | +M | +N | +O | +P | +Q | +R | +S | +T | +U | +V | +W | +X | +Y | +Z | +_ | +other | +(11853 entries) | +
| Constructor Index | +A | +B | +C | +D | +E | +F | +G | +H | +I | +J | +K | +L | +M | +N | +O | +P | +Q | +R | +S | +T | +U | +V | +W | +X | +Y | +Z | +_ | +other | +(359 entries) | +
| Axiom Index | +A | +B | +C | +D | +E | +F | +G | +H | +I | +J | +K | +L | +M | +N | +O | +P | +Q | +R | +S | +T | +U | +V | +W | +X | +Y | +Z | +_ | +other | +(47 entries) | +
| Inductive Index | +A | +B | +C | +D | +E | +F | +G | +H | +I | +J | +K | +L | +M | +N | +O | +P | +Q | +R | +S | +T | +U | +V | +W | +X | +Y | +Z | +_ | +other | +(103 entries) | +
| Projection Index | +A | +B | +C | +D | +E | +F | +G | +H | +I | +J | +K | +L | +M | +N | +O | +P | +Q | +R | +S | +T | +U | +V | +W | +X | +Y | +Z | +_ | +other | +(266 entries) | +
| Section Index | +A | +B | +C | +D | +E | +F | +G | +H | +I | +J | +K | +L | +M | +N | +O | +P | +Q | +R | +S | +T | +U | +V | +W | +X | +Y | +Z | +_ | +other | +(1118 entries) | +
| Abbreviation Index | +A | +B | +C | +D | +E | +F | +G | +H | +I | +J | +K | +L | +M | +N | +O | +P | +Q | +R | +S | +T | +U | +V | +W | +X | +Y | +Z | +_ | +other | +(691 entries) | +
| Definition Index | +A | +B | +C | +D | +E | +F | +G | +H | +I | +J | +K | +L | +M | +N | +O | +P | +Q | +R | +S | +T | +U | +V | +W | +X | +Y | +Z | +_ | +other | +(3461 entries) | +
| Record Index | +A | +B | +C | +D | +E | +F | +G | +H | +I | +J | +K | +L | +M | +N | +O | +P | +Q | +R | +S | +T | +U | +V | +W | +X | +Y | +Z | +_ | +other | +(185 entries) | +
S (lemma)
+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]
+same_pblock [in mathcomp.ssreflect.finset]
+scalar_mx_hom [in mathcomp.character.mxrepresentation]
+scalar_mx_comm [in mathcomp.algebra.matrix]
+scalar_mxC [in mathcomp.algebra.matrix]
+scalar_mx_is_multiplicative [in mathcomp.algebra.matrix]
+scalar_mxM [in mathcomp.algebra.matrix]
+scalar_mx_block [in mathcomp.algebra.matrix]
+scalar_mx_is_scalar [in mathcomp.algebra.matrix]
+scalar_mx_sum_delta [in mathcomp.algebra.matrix]
+scalar_mx_is_additive [in mathcomp.algebra.matrix]
+scalar_mx_key [in mathcomp.algebra.matrix]
+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_lfunE [in mathcomp.algebra.vector]
+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_poly_eq0 [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]
+scale_is_groupAction [in mathcomp.character.mxabelem]
+scale_is_action [in mathcomp.character.mxabelem]
+scale_actE [in mathcomp.character.mxabelem]
+scale1mx [in mathcomp.algebra.matrix]
+scalqE [in mathcomp.algebra.rat]
+scalq_eq0 [in mathcomp.algebra.rat]
+scalq_key [in mathcomp.algebra.rat]
+scanlK [in mathcomp.ssreflect.seq]
+scanl_tupleP [in mathcomp.ssreflect.tuple]
+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_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]
+sdprod_cfker [in mathcomp.character.classfun]
+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_eqmx [in mathcomp.character.mxrepresentation]
+section_eqmx_add [in mathcomp.character.mxrepresentation]
+section_module [in mathcomp.character.mxrepresentation]
+section_repr_isog [in mathcomp.solvable.jordanholder]
+section_reprP [in mathcomp.solvable.jordanholder]
+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_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]
+separable_Xn_sub_1 [in mathcomp.field.cyclotomic]
+seqs1 [in mathcomp.solvable.burnside_app]
+seqv_sub_adjoin [in mathcomp.field.falgebra]
+seq_tnthP [in mathcomp.ssreflect.tuple]
+seq_choiceMixin [in mathcomp.ssreflect.choice]
+seq_of_optK [in mathcomp.ssreflect.choice]
+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]
+seq2_ind [in mathcomp.ssreflect.seq]
+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_normal_Hall [in mathcomp.solvable.pgroup]
+setI_subnormal [in mathcomp.solvable.gseries]
+setI_im_cpair [in mathcomp.solvable.center]
+setI_transversal_pblock [in mathcomp.ssreflect.finset]
+setI_eq0 [in mathcomp.ssreflect.finset]
+setI_powerset [in mathcomp.ssreflect.finset]
+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_Frobenius_compl [in mathcomp.solvable.frobenius]
+set_nth_default [in mathcomp.ssreflect.seq]
+set_set_nth [in mathcomp.ssreflect.seq]
+set_nth_nil [in mathcomp.ssreflect.seq]
+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_partition_big [in mathcomp.ssreflect.finset]
+set_partition_big_cond [in mathcomp.ssreflect.finset]
+set_cons [in mathcomp.ssreflect.finset]
+set_0Vmem [in mathcomp.ssreflect.finset]
+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]
+sig2W [in mathcomp.ssreflect.choice]
+sig2_eqW [in mathcomp.ssreflect.choice]
+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_Socle [in mathcomp.character.mxrepresentation]
+simple_compsP [in mathcomp.solvable.jordanholder]
+simple_maxnormal [in mathcomp.solvable.gseries]
+simple_sol_prime [in mathcomp.solvable.maximal]
+sizeTP [in mathcomp.field.closed_field]
+sizeT_qf [in mathcomp.field.closed_field]
+sizeYE [in mathcomp.algebra.polyXY]
+sizeY_mulX [in mathcomp.algebra.polyXY]
+sizeY_eq0 [in mathcomp.algebra.polyXY]
+size_minCpoly [in mathcomp.field.algC]
+size_traject [in mathcomp.ssreflect.path]
+size_sort [in mathcomp.ssreflect.path]
+size_merge [in mathcomp.ssreflect.path]
+size_minPoly [in mathcomp.field.fieldext]
+size_Fadjoin_poly [in mathcomp.field.fieldext]
+size_basis [in mathcomp.algebra.vector]
+size_rat_int_poly [in mathcomp.algebra.intdiv]
+size_zprimitive [in mathcomp.algebra.intdiv]
+size_tuple [in mathcomp.ssreflect.tuple]
+size_mod_mxminpoly [in mathcomp.algebra.mxpoly]
+size_mxminpoly [in mathcomp.algebra.mxpoly]
+size_char_poly [in mathcomp.algebra.mxpoly]
+size_poly_XmY [in mathcomp.algebra.polyXY]
+size_poly_XaY [in mathcomp.algebra.polyXY]
+size_Cyclotomic [in mathcomp.field.cyclotomic]
+size_cyclotomic [in mathcomp.field.cyclotomic]
+size_allpairs [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 [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_cfclass [in mathcomp.character.inertia]
+size_abelian_type [in mathcomp.solvable.abelian]
+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 [in mathcomp.algebra.poly]
+size_Cmul [in mathcomp.algebra.poly]
+size_scale [in mathcomp.algebra.poly]
+size_mul [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_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_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_orbit [in mathcomp.ssreflect.fingraph]
+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]
+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_has_lin_char [in mathcomp.character.character]
+solvable_irr_extendible_from_det [in mathcomp.character.inertia]
+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]
+sop_morph [in mathcomp.solvable.burnside_app]
+sop_spec [in mathcomp.solvable.burnside_app]
+sop_inj [in mathcomp.solvable.burnside_app]
+sorted_uniq [in mathcomp.ssreflect.path]
+sorted_filter [in mathcomp.ssreflect.path]
+sorted_divisors_ltn [in mathcomp.ssreflect.prime]
+sorted_divisors [in mathcomp.ssreflect.prime]
+sorted_primes [in mathcomp.ssreflect.prime]
+sort_uniq [in mathcomp.ssreflect.path]
+sort_sorted [in mathcomp.ssreflect.path]
+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]
+span_orthogonal [in mathcomp.character.classfun]
+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_subproof [in mathcomp.ssreflect.fintype]
+split1 [in mathcomp.algebra.zmodp]
+split1_extraspecial [in mathcomp.solvable.maximal]
+sqrnD [in mathcomp.ssreflect.ssrnat]
+sqrnD_sub [in mathcomp.ssreflect.ssrnat]
+sqrn_inj [in mathcomp.ssreflect.ssrnat]
+sqrn_gt0 [in mathcomp.ssreflect.ssrnat]
+sqrn_sub [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]
+stable_rowg_mxK [in mathcomp.character.mxabelem]
+stab_semiprime [in mathcomp.solvable.frobenius]
+stab_ntransitiveI [in mathcomp.solvable.primitive_action]
+stab_ntransitive [in mathcomp.solvable.primitive_action]
+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]
+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_extraspecial_maximal [in mathcomp.solvable.maximal]
+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]
+subCset [in mathcomp.ssreflect.finset]
+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_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]
+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]
+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]
+subitvP [in mathcomp.algebra.interval]
+subitvPl [in mathcomp.algebra.interval]
+subitvPr [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]
+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]
+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]
+subnAC [in mathcomp.ssreflect.ssrnat]
+subnBA [in mathcomp.ssreflect.ssrnat]
+subnDA [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_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_sorted [in mathcomp.ssreflect.path]
+subseq_order_path [in mathcomp.ssreflect.path]
+subseq_uniqP [in mathcomp.ssreflect.seq]
+subseq_filter [in mathcomp.ssreflect.seq]
+subseq_uniq [in mathcomp.ssreflect.seq]
+subseq_rcons [in mathcomp.ssreflect.seq]
+subseq_cons [in mathcomp.ssreflect.seq]
+subseq_refl [in mathcomp.ssreflect.seq]
+subseq_trans [in mathcomp.ssreflect.seq]
+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_disjoint [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_faithful [in mathcomp.fingroup.action]
+subset_gen [in mathcomp.fingroup.fingroup]
+subset_closure [in mathcomp.ssreflect.fingraph]
+subset_dfs [in mathcomp.ssreflect.fingraph]
+subset_neq0 [in mathcomp.ssreflect.finset]
+subset_leqif_cards [in mathcomp.ssreflect.finset]
+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_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_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_path [in mathcomp.ssreflect.path]
+sub_conjC_vchar [in mathcomp.character.vcharacter]
+sub_aut_zchar [in mathcomp.character.vcharacter]
+sub_baseField [in mathcomp.field.fieldext]
+sub_adjoin1v [in mathcomp.field.fieldext]
+sub_pnat_coprime [in mathcomp.ssreflect.prime]
+sub_in_pnat [in mathcomp.ssreflect.prime]
+sub_in_partn [in mathcomp.ssreflect.prime]
+sub_adjoin_separable_generator [in mathcomp.field.separable]
+sub_inseparable [in mathcomp.field.separable]
+sub_span [in mathcomp.algebra.vector]
+sub_annihilant_neq0 [in mathcomp.algebra.polyXY]
+sub_annihilantP [in mathcomp.algebra.polyXY]
+sub_annihilant_in_ideal [in mathcomp.algebra.polyXY]
+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_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_Ldiv [in mathcomp.solvable.abelian]
+sub_LdivT [in mathcomp.solvable.abelian]
+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_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_der1_abelian [in mathcomp.solvable.commutator]
+sub_der1_normal [in mathcomp.solvable.commutator]
+sub_der1_norm [in mathcomp.solvable.commutator]
+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_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_center_normal [in mathcomp.solvable.center]
+sub_agenv [in mathcomp.field.falgebra]
+sub_cyclic_char [in mathcomp.solvable.cyclic]
+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_kermxP [in mathcomp.algebra.mxalgebra]
+sub_sumsmxP [in mathcomp.algebra.mxalgebra]
+sub_addsmxP [in mathcomp.algebra.mxalgebra]
+sub_rVP [in mathcomp.algebra.mxalgebra]
+sub_ltmx_trans [in mathcomp.algebra.mxalgebra]
+sub_imset_pre [in mathcomp.ssreflect.finset]
+sub_nilpotent_cent2 [in mathcomp.solvable.sylow]
+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]
+suffix_subseq [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]
+sumn_flatten [in mathcomp.ssreflect.seq]
+sumn_rev [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]
+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_ffun [in mathcomp.algebra.ssralg]
+sum_ffunE [in mathcomp.algebra.ssralg]
+sum_irr_degree [in mathcomp.character.mxrepresentation]
+sum_mxsimple_direct_sub [in mathcomp.character.mxrepresentation]
+sum_mxsimple_direct_compl [in mathcomp.character.mxrepresentation]
+sum_lfunE [in mathcomp.algebra.vector]
+sum_norm_irr_quo [in mathcomp.character.character]
+sum_enum_uniq [in mathcomp.ssreflect.fintype]
+sum_card_class [in mathcomp.fingroup.action]
+sum_by_classes [in mathcomp.character.classfun]
+sum_cfunE [in mathcomp.character.classfun]
+sum_nat_eq0 [in mathcomp.ssreflect.bigop]
+sum_nat_const_nat [in mathcomp.ssreflect.bigop]
+sum_nat_const [in mathcomp.ssreflect.bigop]
+sum_index_rcosets_cycle [in mathcomp.solvable.finmodule]
+sum_eqE [in mathcomp.ssreflect.eqtype]
+sum_eqP [in mathcomp.ssreflect.eqtype]
+sum_totient_dvd [in mathcomp.solvable.cyclic]
+sum_ncycle_totient [in mathcomp.solvable.cyclic]
+sum_nat_dep_const [in mathcomp.ssreflect.finset]
+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]
+svalP [in mathcomp.ssreflect.eqtype]
+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]
+symplectic_type_group_structure [in mathcomp.solvable.extremal]
+Sym_trans [in mathcomp.solvable.alt]
+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]
+s2valP [in mathcomp.ssreflect.eqtype]
+s2valP' [in mathcomp.ssreflect.eqtype]
+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 | +(23233 entries) | +
| Notation Index | +A | +B | +C | +D | +E | +F | +G | +H | +I | +J | +K | +L | +M | +N | +O | +P | +Q | +R | +S | +T | +U | +V | +W | +X | +Y | +Z | +_ | +other | +(1373 entries) | +
| Module Index | +A | +B | +C | +D | +E | +F | +G | +H | +I | +J | +K | +L | +M | +N | +O | +P | +Q | +R | +S | +T | +U | +V | +W | +X | +Y | +Z | +_ | +other | +(213 entries) | +
| Variable Index | +A | +B | +C | +D | +E | +F | +G | +H | +I | +J | +K | +L | +M | +N | +O | +P | +Q | +R | +S | +T | +U | +V | +W | +X | +Y | +Z | +_ | +other | +(3475 entries) | +
| Library Index | +A | +B | +C | +D | +E | +F | +G | +H | +I | +J | +K | +L | +M | +N | +O | +P | +Q | +R | +S | +T | +U | +V | +W | +X | +Y | +Z | +_ | +other | +(89 entries) | +
| Lemma Index | +A | +B | +C | +D | +E | +F | +G | +H | +I | +J | +K | +L | +M | +N | +O | +P | +Q | +R | +S | +T | +U | +V | +W | +X | +Y | +Z | +_ | +other | +(11853 entries) | +
| Constructor Index | +A | +B | +C | +D | +E | +F | +G | +H | +I | +J | +K | +L | +M | +N | +O | +P | +Q | +R | +S | +T | +U | +V | +W | +X | +Y | +Z | +_ | +other | +(359 entries) | +
| Axiom Index | +A | +B | +C | +D | +E | +F | +G | +H | +I | +J | +K | +L | +M | +N | +O | +P | +Q | +R | +S | +T | +U | +V | +W | +X | +Y | +Z | +_ | +other | +(47 entries) | +
| Inductive Index | +A | +B | +C | +D | +E | +F | +G | +H | +I | +J | +K | +L | +M | +N | +O | +P | +Q | +R | +S | +T | +U | +V | +W | +X | +Y | +Z | +_ | +other | +(103 entries) | +
| Projection Index | +A | +B | +C | +D | +E | +F | +G | +H | +I | +J | +K | +L | +M | +N | +O | +P | +Q | +R | +S | +T | +U | +V | +W | +X | +Y | +Z | +_ | +other | +(266 entries) | +
| Section Index | +A | +B | +C | +D | +E | +F | +G | +H | +I | +J | +K | +L | +M | +N | +O | +P | +Q | +R | +S | +T | +U | +V | +W | +X | +Y | +Z | +_ | +other | +(1118 entries) | +
| Abbreviation Index | +A | +B | +C | +D | +E | +F | +G | +H | +I | +J | +K | +L | +M | +N | +O | +P | +Q | +R | +S | +T | +U | +V | +W | +X | +Y | +Z | +_ | +other | +(691 entries) | +
| Definition Index | +A | +B | +C | +D | +E | +F | +G | +H | +I | +J | +K | +L | +M | +N | +O | +P | +Q | +R | +S | +T | +U | +V | +W | +X | +Y | +Z | +_ | +other | +(3461 entries) | +
| Record Index | +A | +B | +C | +D | +E | +F | +G | +H | +I | +J | +K | +L | +M | +N | +O | +P | +Q | +R | +S | +T | +U | +V | +W | +X | +Y | +Z | +_ | +other | +(185 entries) | +