| 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 | -(23836 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 | -(1409 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 | -(221 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 | -(3574 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 | -(90 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 | -(12096 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 | -(368 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 | -(107 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 | -(273 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 | -(1140 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 | -(728 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 | -(3596 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 | -(189 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_ind2 [in mathcomp.ssreflect.seq]
-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]
-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]
-simpl_pred_sortE [in mathcomp.ssreflect.ssrbool]
-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_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_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_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_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_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_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]
-Some_inj [in mathcomp.ssreflect.ssrfun]
-sop_morph [in mathcomp.solvable.burnside_app]
-sop_spec [in mathcomp.solvable.burnside_app]
-sop_inj [in mathcomp.solvable.burnside_app]
-sorted_le_nth [in mathcomp.ssreflect.path]
-sorted_lt_nth [in mathcomp.ssreflect.path]
-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]
-subr_lersif0r [in mathcomp.algebra.interval]
-subr_lersifr0 [in mathcomp.algebra.interval]
-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_trans [in mathcomp.ssreflect.seq]
-subseq_refl [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]
-sumnE [in mathcomp.ssreflect.bigop]
-sumn_flatten [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]
-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_cond_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 | -(23836 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 | -(1409 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 | -(221 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 | -(3574 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 | -(90 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 | -(12096 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 | -(368 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 | -(107 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 | -(273 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 | -(1140 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 | -(728 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 | -(3596 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 | -(189 entries) | -