| 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
-S [abbreviation, in mathcomp.character.mxrepresentation]-same_fconnect1_r [lemma, in mathcomp.ssreflect.fingraph]
-same_fconnect1 [lemma, in mathcomp.ssreflect.fingraph]
-same_fconnect_finv [lemma, in mathcomp.ssreflect.fingraph]
-same_connect_rev [lemma, in mathcomp.ssreflect.fingraph]
-same_connect1r [lemma, in mathcomp.ssreflect.fingraph]
-same_connect1 [lemma, in mathcomp.ssreflect.fingraph]
-same_connect_r [lemma, in mathcomp.ssreflect.fingraph]
-same_connect [lemma, in mathcomp.ssreflect.fingraph]
-same_pblock [lemma, in mathcomp.ssreflect.finset]
-scalar_mx_hom [lemma, in mathcomp.character.mxrepresentation]
-scalar_mx_comm [lemma, in mathcomp.algebra.matrix]
-scalar_mxC [lemma, in mathcomp.algebra.matrix]
-scalar_mx_is_multiplicative [lemma, in mathcomp.algebra.matrix]
-scalar_mxM [lemma, in mathcomp.algebra.matrix]
-scalar_mx_block [lemma, in mathcomp.algebra.matrix]
-scalar_mx_is_scalar [lemma, in mathcomp.algebra.matrix]
-scalar_mx_sum_delta [lemma, in mathcomp.algebra.matrix]
-scalar_mx_is_additive [lemma, in mathcomp.algebra.matrix]
-scalar_mx [definition, in mathcomp.algebra.matrix]
-scalar_mx_key [lemma, in mathcomp.algebra.matrix]
-scalar_mx_cent [lemma, in mathcomp.algebra.mxalgebra]
-ScaleCompLfun [section, in mathcomp.algebra.vector]
-ScaleCompLfun.aT [variable, in mathcomp.algebra.vector]
-ScaleCompLfun.R [variable, in mathcomp.algebra.vector]
-ScaleCompLfun.rT [variable, in mathcomp.algebra.vector]
-ScaleCompLfun.vT [variable, in mathcomp.algebra.vector]
-scalemx [definition, in mathcomp.algebra.matrix]
-scalemxA [lemma, in mathcomp.algebra.matrix]
-scalemxAl [lemma, in mathcomp.algebra.matrix]
-scalemxAr [lemma, in mathcomp.algebra.matrix]
-scalemxDl [lemma, in mathcomp.algebra.matrix]
-scalemxDr [lemma, in mathcomp.algebra.matrix]
-scalemx_inj [lemma, in mathcomp.algebra.matrix]
-scalemx_eq0 [lemma, in mathcomp.algebra.matrix]
-scalemx_const [lemma, in mathcomp.algebra.matrix]
-scalemx_key [lemma, in mathcomp.algebra.matrix]
-scalemx_sub [lemma, in mathcomp.algebra.mxalgebra]
-scalemx1 [lemma, in mathcomp.algebra.matrix]
-scalerMzl [lemma, in mathcomp.algebra.ssrint]
-scalerMzr [lemma, in mathcomp.algebra.ssrint]
-scaler_int [lemma, in mathcomp.algebra.ssrint]
-scalezrE [lemma, in mathcomp.algebra.ssrint]
-scale_zchar [lemma, in mathcomp.character.vcharacter]
-scale_pair [definition, in mathcomp.algebra.ssralg]
-scale_lfunE [lemma, in mathcomp.algebra.vector]
-scale_lfun [definition, in mathcomp.algebra.vector]
-scale_scalar_mx [lemma, in mathcomp.algebra.matrix]
-scale_block_mx [lemma, in mathcomp.algebra.matrix]
-scale_col_mx [lemma, in mathcomp.algebra.matrix]
-scale_row_mx [lemma, in mathcomp.algebra.matrix]
-scale_poly_eq0 [lemma, in mathcomp.algebra.poly]
-scale_polyAl [lemma, in mathcomp.algebra.poly]
-scale_polyDl [lemma, in mathcomp.algebra.poly]
-scale_polyDr [lemma, in mathcomp.algebra.poly]
-scale_1poly [lemma, in mathcomp.algebra.poly]
-scale_polyA [lemma, in mathcomp.algebra.poly]
-scale_polyE [lemma, in mathcomp.algebra.poly]
-scale_poly [definition, in mathcomp.algebra.poly]
-scale_poly_key [lemma, in mathcomp.algebra.poly]
-scale_poly_def [definition, in mathcomp.algebra.poly]
-scale_is_groupAction [lemma, in mathcomp.character.mxabelem]
-scale_is_action [lemma, in mathcomp.character.mxabelem]
-scale_actE [lemma, in mathcomp.character.mxabelem]
-scale_act [definition, in mathcomp.character.mxabelem]
-scale1mx [lemma, in mathcomp.algebra.matrix]
-scalq [definition, in mathcomp.algebra.rat]
-scalqE [lemma, in mathcomp.algebra.rat]
-scalq_eq0 [lemma, in mathcomp.algebra.rat]
-scalq_def [definition, in mathcomp.algebra.rat]
-scalq_key [lemma, in mathcomp.algebra.rat]
-Scan [section, in mathcomp.ssreflect.seq]
-scanl [definition, in mathcomp.ssreflect.seq]
-scanlK [lemma, in mathcomp.ssreflect.seq]
-scanl_tupleP [lemma, in mathcomp.ssreflect.tuple]
-scanl_cat [lemma, in mathcomp.ssreflect.seq]
-Scan.f [variable, in mathcomp.ssreflect.seq]
-Scan.g [variable, in mathcomp.ssreflect.seq]
-Scan.T1 [variable, in mathcomp.ssreflect.seq]
-Scan.T2 [variable, in mathcomp.ssreflect.seq]
-Scan.x1 [variable, in mathcomp.ssreflect.seq]
-Scan.x2 [variable, in mathcomp.ssreflect.seq]
-SchurZassenhaus_trans_actsol [lemma, in mathcomp.solvable.hall]
-SchurZassenhaus_trans_sol [lemma, in mathcomp.solvable.hall]
-SchurZassenhaus_split [lemma, in mathcomp.solvable.hall]
-SCN [section, in mathcomp.solvable.maximal]
-SCN [definition, in mathcomp.solvable.maximal]
-SCN_max [lemma, in mathcomp.solvable.maximal]
-SCN_abelian [lemma, in mathcomp.solvable.maximal]
-SCN_P [lemma, in mathcomp.solvable.maximal]
-SCN_at [definition, in mathcomp.solvable.maximal]
-SCN.G [variable, in mathcomp.solvable.maximal]
-SCN.gT [variable, in mathcomp.solvable.maximal]
-SCN.p [variable, in mathcomp.solvable.maximal]
-SCN.SCNseries [section, in mathcomp.solvable.maximal]
-SCN.SCNseries.A [variable, in mathcomp.solvable.maximal]
-SCN.SCNseries.cAA [variable, in mathcomp.solvable.maximal]
-SCN.SCNseries.nZA [variable, in mathcomp.solvable.maximal]
-SCN.SCNseries.SCN_A [variable, in mathcomp.solvable.maximal]
-SCN.SCNseries.sZA [variable, in mathcomp.solvable.maximal]
-SCN.SCNseries.Z [variable, in mathcomp.solvable.maximal]
-SdPair [constructor, in mathcomp.fingroup.gproduct]
-sdpairE [lemma, in mathcomp.fingroup.gproduct]
-sdpair_setact [lemma, in mathcomp.fingroup.gproduct]
-sdpair_act [lemma, in mathcomp.fingroup.gproduct]
-sdpair1 [definition, in mathcomp.fingroup.gproduct]
-sdpair1_morphM [lemma, in mathcomp.fingroup.gproduct]
-sdpair2 [definition, in mathcomp.fingroup.gproduct]
-sdpair2_morphM [lemma, in mathcomp.fingroup.gproduct]
-sdprod [abbreviation, in mathcomp.fingroup.gproduct]
-sdprod [abbreviation, in mathcomp.fingroup.gproduct]
-Sdprod [section, in mathcomp.character.character]
-sdprodE [lemma, in mathcomp.fingroup.gproduct]
-sdprodEY [lemma, in mathcomp.fingroup.gproduct]
-sdprodg1 [lemma, in mathcomp.fingroup.gproduct]
-sdprodJ [lemma, in mathcomp.fingroup.gproduct]
-sdprodm [definition, in mathcomp.fingroup.gproduct]
-sdprodmE [lemma, in mathcomp.fingroup.gproduct]
-sdprodmEl [lemma, in mathcomp.fingroup.gproduct]
-sdprodmEr [lemma, in mathcomp.fingroup.gproduct]
-sdprodm_eqf [lemma, in mathcomp.fingroup.gproduct]
-sdprodm_sub [lemma, in mathcomp.fingroup.gproduct]
-sdprodm_norm [lemma, in mathcomp.fingroup.gproduct]
-sdprodP [lemma, in mathcomp.fingroup.gproduct]
-SDproduct [section, in mathcomp.character.classfun]
-SDproduct.defG [variable, in mathcomp.character.classfun]
-SDproduct.G [variable, in mathcomp.character.classfun]
-SDproduct.gT [variable, in mathcomp.character.classfun]
-SDproduct.H [variable, in mathcomp.character.classfun]
-SDproduct.K [variable, in mathcomp.character.classfun]
-SDproduct.nsKG [variable, in mathcomp.character.classfun]
-SDproduct.sHG [variable, in mathcomp.character.classfun]
-SDproduct.sKG [variable, in mathcomp.character.classfun]
-sdprodW [lemma, in mathcomp.fingroup.gproduct]
-sdprodWC [lemma, in mathcomp.fingroup.gproduct]
-sdprodWpp [lemma, in mathcomp.fingroup.gproduct]
-sdprodWY [lemma, in mathcomp.fingroup.gproduct]
-sdprod_p'core_HallP [lemma, in mathcomp.solvable.pgroup]
-sdprod_Hall_p'coreP [lemma, in mathcomp.solvable.pgroup]
-sdprod_pcore_HallP [lemma, in mathcomp.solvable.pgroup]
-sdprod_Hall_pcoreP [lemma, in mathcomp.solvable.pgroup]
-sdprod_normal_pHallP [lemma, in mathcomp.solvable.pgroup]
-sdprod_normal_p'HallP [lemma, in mathcomp.solvable.pgroup]
-sdprod_Hall [lemma, in mathcomp.solvable.pgroup]
-sdprod_sdpair [lemma, in mathcomp.fingroup.gproduct]
-sdprod_mulgA [lemma, in mathcomp.fingroup.gproduct]
-sdprod_mulVg [lemma, in mathcomp.fingroup.gproduct]
-sdprod_mul1g [lemma, in mathcomp.fingroup.gproduct]
-sdprod_mul [definition, in mathcomp.fingroup.gproduct]
-sdprod_mul_proof [lemma, in mathcomp.fingroup.gproduct]
-sdprod_inv [definition, in mathcomp.fingroup.gproduct]
-sdprod_inv_proof [lemma, in mathcomp.fingroup.gproduct]
-sdprod_one [definition, in mathcomp.fingroup.gproduct]
-sdprod_finMixin [definition, in mathcomp.fingroup.gproduct]
-sdprod_countMixin [definition, in mathcomp.fingroup.gproduct]
-sdprod_choiceMixin [definition, in mathcomp.fingroup.gproduct]
-sdprod_eqMixin [definition, in mathcomp.fingroup.gproduct]
-sdprod_by [inductive, in mathcomp.fingroup.gproduct]
-sdprod_recr [lemma, in mathcomp.fingroup.gproduct]
-sdprod_recl [lemma, in mathcomp.fingroup.gproduct]
-sdprod_modr [lemma, in mathcomp.fingroup.gproduct]
-sdprod_modl [lemma, in mathcomp.fingroup.gproduct]
-sdprod_subr [lemma, in mathcomp.fingroup.gproduct]
-sdprod_isog [lemma, in mathcomp.fingroup.gproduct]
-sdprod_isom [lemma, in mathcomp.fingroup.gproduct]
-sdprod_card [lemma, in mathcomp.fingroup.gproduct]
-sdprod_normal_complP [lemma, in mathcomp.fingroup.gproduct]
-sdprod_compl [lemma, in mathcomp.fingroup.gproduct]
-sdprod_context [lemma, in mathcomp.fingroup.gproduct]
-sdprod_Res_IirrK [lemma, in mathcomp.character.character]
-sdprod_Res_IirrE [lemma, in mathcomp.character.character]
-sdprod_Iirr0 [lemma, in mathcomp.character.character]
-sdprod_Iirr_eq0 [lemma, in mathcomp.character.character]
-sdprod_Iirr_inj [lemma, in mathcomp.character.character]
-sdprod_IirrK [lemma, in mathcomp.character.character]
-sdprod_IirrE [lemma, in mathcomp.character.character]
-sdprod_Iirr [definition, in mathcomp.character.character]
-sdprod_cfker [lemma, in mathcomp.character.classfun]
-Sdprod.defG [variable, in mathcomp.character.character]
-Sdprod.G [variable, in mathcomp.character.character]
-Sdprod.gT [variable, in mathcomp.character.character]
-Sdprod.H [variable, in mathcomp.character.character]
-Sdprod.K [variable, in mathcomp.character.character]
-Sdprod.nKG [variable, in mathcomp.character.character]
-sdprod1g [lemma, in mathcomp.fingroup.gproduct]
-sdT [abbreviation, in mathcomp.fingroup.gproduct]
-sdval [abbreviation, in mathcomp.fingroup.gproduct]
-sd1 [definition, in mathcomp.solvable.burnside_app]
-Sd1 [definition, in mathcomp.solvable.burnside_app]
-sd1_inv [lemma, in mathcomp.solvable.burnside_app]
-Sd1_inj [lemma, in mathcomp.solvable.burnside_app]
-sd2 [definition, in mathcomp.solvable.burnside_app]
-Sd2 [definition, in mathcomp.solvable.burnside_app]
-sd2_inv [lemma, in mathcomp.solvable.burnside_app]
-Sd2_inj [lemma, in mathcomp.solvable.burnside_app]
-SecondIsomorphism [section, in mathcomp.fingroup.quotient]
-SecondIsomorphism.gT [variable, in mathcomp.fingroup.quotient]
-SecondIsomorphism.H [variable, in mathcomp.fingroup.quotient]
-SecondIsomorphism.K [variable, in mathcomp.fingroup.quotient]
-SecondIsomorphism.nKH [variable, in mathcomp.fingroup.quotient]
-second_isog [lemma, in mathcomp.fingroup.quotient]
-second_isom [lemma, in mathcomp.fingroup.quotient]
-second_orthogonality_relation [lemma, in mathcomp.character.character]
-section [inductive, in mathcomp.solvable.jordanholder]
-Sections [section, in mathcomp.solvable.jordanholder]
-Sections.gT [variable, in mathcomp.solvable.jordanholder]
-section_eqmx [lemma, in mathcomp.character.mxrepresentation]
-section_eqmx_add [lemma, in mathcomp.character.mxrepresentation]
-section_repr [definition, in mathcomp.character.mxrepresentation]
-section_module [lemma, in mathcomp.character.mxrepresentation]
-section_repr_isog [lemma, in mathcomp.solvable.jordanholder]
-section_reprP [lemma, in mathcomp.solvable.jordanholder]
-section_repr [definition, in mathcomp.solvable.jordanholder]
-section_isog [definition, in mathcomp.solvable.jordanholder]
-section_finMixin [definition, in mathcomp.solvable.jordanholder]
-section_countMixin [definition, in mathcomp.solvable.jordanholder]
-section_choiceMixin [definition, in mathcomp.solvable.jordanholder]
-section_eqMixin [definition, in mathcomp.solvable.jordanholder]
-SemiDihedral [constructor, in mathcomp.solvable.extremal]
-semidihedral_classP [lemma, in mathcomp.solvable.extremal]
-semidihedral_structure [lemma, in mathcomp.solvable.extremal]
-semidihedral_gtype [definition, in mathcomp.solvable.extremal]
-semidirect_product [definition, in mathcomp.fingroup.gproduct]
-semiprime [definition, in mathcomp.solvable.frobenius]
-semiprimeJ [lemma, in mathcomp.solvable.frobenius]
-semiprimeS [lemma, in mathcomp.solvable.frobenius]
-semiprime_regular [lemma, in mathcomp.solvable.frobenius]
-semiregular [definition, in mathcomp.solvable.frobenius]
-semiregularJ [lemma, in mathcomp.solvable.frobenius]
-semiregularS [lemma, in mathcomp.solvable.frobenius]
-semiregular_prime [lemma, in mathcomp.solvable.frobenius]
-semiregular_sym [lemma, in mathcomp.solvable.frobenius]
-semiregular1l [lemma, in mathcomp.solvable.frobenius]
-semiregular1r [lemma, in mathcomp.solvable.frobenius]
-semisimple_Socle [lemma, in mathcomp.character.mxrepresentation]
-separable [definition, in mathcomp.field.separable]
-Separable [section, in mathcomp.field.separable]
-separable [abbreviation, in mathcomp.field.separable]
-separable [library]
-separableP [lemma, in mathcomp.field.separable]
-separablePn [lemma, in mathcomp.field.separable]
-SeparablePoly [section, in mathcomp.field.separable]
-SeparablePoly.R [variable, in mathcomp.field.separable]
-separableS [lemma, in mathcomp.field.separable]
-separableSl [lemma, in mathcomp.field.separable]
-separableSr [lemma, in mathcomp.field.separable]
-separable_Fadjoin_seq [lemma, in mathcomp.field.separable]
-separable_trans [lemma, in mathcomp.field.separable]
-separable_refl [lemma, in mathcomp.field.separable]
-separable_generator_maximal [lemma, in mathcomp.field.separable]
-separable_generatorP [lemma, in mathcomp.field.separable]
-separable_generator_mem [lemma, in mathcomp.field.separable]
-separable_generator [definition, in mathcomp.field.separable]
-separable_inseparable_decomposition [lemma, in mathcomp.field.separable]
-separable_sum [lemma, in mathcomp.field.separable]
-separable_add [lemma, in mathcomp.field.separable]
-separable_inseparable_element [lemma, in mathcomp.field.separable]
-separable_exponent [lemma, in mathcomp.field.separable]
-separable_elementS [lemma, in mathcomp.field.separable]
-separable_root_der [lemma, in mathcomp.field.separable]
-separable_nz_der [lemma, in mathcomp.field.separable]
-separable_elementP [lemma, in mathcomp.field.separable]
-separable_element [definition, in mathcomp.field.separable]
-separable_map [lemma, in mathcomp.field.separable]
-separable_prod_XsubC [lemma, in mathcomp.field.separable]
-separable_root [lemma, in mathcomp.field.separable]
-separable_mul [lemma, in mathcomp.field.separable]
-separable_deriv_eq0 [lemma, in mathcomp.field.separable]
-separable_nosquare [lemma, in mathcomp.field.separable]
-separable_coprime [lemma, in mathcomp.field.separable]
-separable_polyP [lemma, in mathcomp.field.separable]
-separable_poly_neq0 [lemma, in mathcomp.field.separable]
-separable_poly [definition, in mathcomp.field.separable]
-separable_Xn_sub_1 [lemma, in mathcomp.field.cyclotomic]
-Separable.Derivation [section, in mathcomp.field.separable]
-Separable.DerivationAlgebra [section, in mathcomp.field.separable]
-Separable.DerivationAlgebra.D [variable, in mathcomp.field.separable]
-Separable.DerivationAlgebra.derD [variable, in mathcomp.field.separable]
-Separable.DerivationAlgebra.E [variable, in mathcomp.field.separable]
-Separable.Derivation.D [variable, in mathcomp.field.separable]
-Separable.Derivation.derD [variable, in mathcomp.field.separable]
-Separable.Derivation.K [variable, in mathcomp.field.separable]
-Separable.F [variable, in mathcomp.field.separable]
-Separable.L [variable, in mathcomp.field.separable]
-Separable.PrimitiveElementTheorem [section, in mathcomp.field.separable]
-Separable.PrimitiveElementTheorem.FiniteCase [section, in mathcomp.field.separable]
-Separable.PrimitiveElementTheorem.FiniteCase.cyclic_or_large [variable, in mathcomp.field.separable]
-Separable.PrimitiveElementTheorem.FiniteCase.K_is_large [variable, in mathcomp.field.separable]
-Separable.PrimitiveElementTheorem.FiniteCase.N [variable, in mathcomp.field.separable]
-Separable.PrimitiveElementTheorem.K [variable, in mathcomp.field.separable]
-Separable.PrimitiveElementTheorem.sepKy [variable, in mathcomp.field.separable]
-Separable.PrimitiveElementTheorem.x [variable, in mathcomp.field.separable]
-Separable.PrimitiveElementTheorem.y [variable, in mathcomp.field.separable]
-Separable.SeparableElement [section, in mathcomp.field.separable]
-Separable.SeparableElement.ExtendDerivation [section, in mathcomp.field.separable]
-Separable.SeparableElement.ExtendDerivation.D [variable, in mathcomp.field.separable]
-Separable.SeparableElement.ExtendDerivation.derD [variable, in mathcomp.field.separable]
-Separable.SeparableElement.ExtendDerivation.Dx [variable, in mathcomp.field.separable]
-Separable.SeparableElement.K [variable, in mathcomp.field.separable]
-Separable.SeparableElement.Kx_x [variable, in mathcomp.field.separable]
-Separable.SeparableElement.sKxK [variable, in mathcomp.field.separable]
-Separable.SeparableElement.x [variable, in mathcomp.field.separable]
-seq [abbreviation, in mathcomp.ssreflect.seq]
-seq [library]
-SeqFinType [section, in mathcomp.ssreflect.fintype]
-SeqFinType.s [variable, in mathcomp.ssreflect.fintype]
-SeqFinType.T [variable, in mathcomp.ssreflect.fintype]
-seqn [definition, in mathcomp.ssreflect.seq]
-seqn_rec [definition, in mathcomp.ssreflect.seq]
-seqn_type [definition, in mathcomp.ssreflect.seq]
-SeqSub [constructor, in mathcomp.ssreflect.fintype]
-SeqSubType [section, in mathcomp.ssreflect.fintype]
-SeqSubType.s [variable, in mathcomp.ssreflect.fintype]
-SeqSubType.T [variable, in mathcomp.ssreflect.fintype]
-seqs1 [lemma, in mathcomp.solvable.burnside_app]
-SeqTuple [section, in mathcomp.ssreflect.tuple]
-SeqTuple.m [variable, in mathcomp.ssreflect.tuple]
-SeqTuple.n [variable, in mathcomp.ssreflect.tuple]
-SeqTuple.rT [variable, in mathcomp.ssreflect.tuple]
-SeqTuple.T [variable, in mathcomp.ssreflect.tuple]
-SeqTuple.U [variable, in mathcomp.ssreflect.tuple]
-Sequences [section, in mathcomp.ssreflect.seq]
-Sequences.n0 [variable, in mathcomp.ssreflect.seq]
-Sequences.SeqFind [section, in mathcomp.ssreflect.seq]
-Sequences.SeqFind.a [variable, in mathcomp.ssreflect.seq]
-Sequences.SubPred [section, in mathcomp.ssreflect.seq]
-Sequences.SubPred.a1 [variable, in mathcomp.ssreflect.seq]
-Sequences.SubPred.a2 [variable, in mathcomp.ssreflect.seq]
-Sequences.SubPred.s12 [variable, in mathcomp.ssreflect.seq]
-Sequences.T [variable, in mathcomp.ssreflect.seq]
-Sequences.x0 [variable, in mathcomp.ssreflect.seq]
-_ ++ _ (seq_scope) [notation, in mathcomp.ssreflect.seq]
-seqv_sub_adjoin [lemma, in mathcomp.field.falgebra]
-seq_tnthP [lemma, in mathcomp.ssreflect.tuple]
-seq_eqclass [definition, in mathcomp.ssreflect.seq]
-seq_ind2 [lemma, in mathcomp.ssreflect.seq]
-seq_countMixin [definition, in mathcomp.ssreflect.choice]
-seq_choiceMixin [lemma, in mathcomp.ssreflect.choice]
-seq_of_optK [lemma, in mathcomp.ssreflect.choice]
-seq_of_opt [definition, in mathcomp.ssreflect.choice]
-seq_sub_choiceMixin [definition, in mathcomp.ssreflect.fintype]
-seq_sub_finMixin [definition, in mathcomp.ssreflect.fintype]
-seq_sub_axiom [lemma, in mathcomp.ssreflect.fintype]
-seq_sub_countMixin [definition, in mathcomp.ssreflect.fintype]
-seq_sub_pickleK [lemma, in mathcomp.ssreflect.fintype]
-seq_sub_unpickle [definition, in mathcomp.ssreflect.fintype]
-seq_sub_pickle [definition, in mathcomp.ssreflect.fintype]
-seq_sub_enum [definition, in mathcomp.ssreflect.fintype]
-seq_sub_eqMixin [definition, in mathcomp.ssreflect.fintype]
-seq_sub [record, in mathcomp.ssreflect.fintype]
-seq_iso3_L [definition, in mathcomp.solvable.burnside_app]
-seq_iso_L [definition, in mathcomp.solvable.burnside_app]
-seq1_basis [lemma, in mathcomp.algebra.vector]
-seq1_free [lemma, in mathcomp.algebra.vector]
-SeriesDefs [section, in mathcomp.solvable.nilpotent]
-SeriesDefs.A [variable, in mathcomp.solvable.nilpotent]
-SeriesDefs.gT [variable, in mathcomp.solvable.nilpotent]
-SeriesDefs.n [variable, in mathcomp.solvable.nilpotent]
-series_repr [definition, in mathcomp.character.mxrepresentation]
-series_sol [lemma, in mathcomp.solvable.nilpotent]
-setact [definition, in mathcomp.fingroup.action]
-setactE [lemma, in mathcomp.fingroup.action]
-setactJ [lemma, in mathcomp.fingroup.action]
-setactVin [lemma, in mathcomp.fingroup.action]
-setact_orbit [lemma, in mathcomp.fingroup.action]
-setact_is_action [lemma, in mathcomp.fingroup.action]
-setC [definition, in mathcomp.ssreflect.finset]
-setCD [lemma, in mathcomp.ssreflect.finset]
-setCI [lemma, in mathcomp.ssreflect.finset]
-setCK [lemma, in mathcomp.ssreflect.finset]
-setCP [lemma, in mathcomp.ssreflect.finset]
-setCS [lemma, in mathcomp.ssreflect.finset]
-setCT [lemma, in mathcomp.ssreflect.finset]
-setCU [lemma, in mathcomp.ssreflect.finset]
-setC_bigcap [lemma, in mathcomp.ssreflect.finset]
-setC_bigcup [lemma, in mathcomp.ssreflect.finset]
-setC_inj [lemma, in mathcomp.ssreflect.finset]
-setC0 [lemma, in mathcomp.ssreflect.finset]
-setC11 [lemma, in mathcomp.ssreflect.finset]
-setD [definition, in mathcomp.ssreflect.finset]
-setDDl [lemma, in mathcomp.ssreflect.finset]
-setDDr [lemma, in mathcomp.ssreflect.finset]
-setDE [lemma, in mathcomp.ssreflect.finset]
-SetDef [module, in mathcomp.ssreflect.finset]
-SetDefSig [module, in mathcomp.ssreflect.finset]
-SetDefSig.finset [axiom, in mathcomp.ssreflect.finset]
-SetDefSig.finsetE [axiom, in mathcomp.ssreflect.finset]
-SetDefSig.pred_of_setE [axiom, in mathcomp.ssreflect.finset]
-SetDefSig.pred_of_set [axiom, in mathcomp.ssreflect.finset]
-SetDef.finset [definition, in mathcomp.ssreflect.finset]
-SetDef.finsetE [lemma, in mathcomp.ssreflect.finset]
-SetDef.pred_of_setE [lemma, in mathcomp.ssreflect.finset]
-SetDef.pred_of_set [definition, in mathcomp.ssreflect.finset]
-setDidPl [lemma, in mathcomp.ssreflect.finset]
-setDIl [lemma, in mathcomp.ssreflect.finset]
-setDIr [lemma, in mathcomp.ssreflect.finset]
-setDP [lemma, in mathcomp.ssreflect.finset]
-setDS [lemma, in mathcomp.ssreflect.finset]
-setDSS [lemma, in mathcomp.ssreflect.finset]
-setDT [lemma, in mathcomp.ssreflect.finset]
-setDUl [lemma, in mathcomp.ssreflect.finset]
-setDUr [lemma, in mathcomp.ssreflect.finset]
-setDv [lemma, in mathcomp.ssreflect.finset]
-setD_eq0 [lemma, in mathcomp.ssreflect.finset]
-setD0 [lemma, in mathcomp.ssreflect.finset]
-setD1K [lemma, in mathcomp.ssreflect.finset]
-setD1P [lemma, in mathcomp.ssreflect.finset]
-setD11 [lemma, in mathcomp.ssreflect.finset]
-setI [definition, in mathcomp.ssreflect.finset]
-setIA [lemma, in mathcomp.ssreflect.finset]
-setIAC [lemma, in mathcomp.ssreflect.finset]
-setIACA [lemma, in mathcomp.ssreflect.finset]
-setIC [lemma, in mathcomp.ssreflect.finset]
-setICA [lemma, in mathcomp.ssreflect.finset]
-setICr [lemma, in mathcomp.ssreflect.finset]
-setID [lemma, in mathcomp.ssreflect.finset]
-setIDA [lemma, in mathcomp.ssreflect.finset]
-setIDAC [lemma, in mathcomp.ssreflect.finset]
-setIdE [lemma, in mathcomp.ssreflect.finset]
-setIdP [lemma, in mathcomp.ssreflect.finset]
-setId2P [lemma, in mathcomp.ssreflect.finset]
-setIg1 [lemma, in mathcomp.fingroup.fingroup]
-setIid [lemma, in mathcomp.ssreflect.finset]
-setIidPl [lemma, in mathcomp.ssreflect.finset]
-setIidPr [lemma, in mathcomp.ssreflect.finset]
-setIIl [lemma, in mathcomp.ssreflect.finset]
-setIIr [lemma, in mathcomp.ssreflect.finset]
-setIK [lemma, in mathcomp.ssreflect.finset]
-setIP [lemma, in mathcomp.ssreflect.finset]
-setIS [lemma, in mathcomp.ssreflect.finset]
-setISS [lemma, in mathcomp.ssreflect.finset]
-setIT [lemma, in mathcomp.ssreflect.finset]
-setIUl [lemma, in mathcomp.ssreflect.finset]
-setIUr [lemma, in mathcomp.ssreflect.finset]
-setI_normal_Hall [lemma, in mathcomp.solvable.pgroup]
-setI_subnormal [lemma, in mathcomp.solvable.gseries]
-setI_im_cpair [lemma, in mathcomp.solvable.center]
-setI_transversal_pblock [lemma, in mathcomp.ssreflect.finset]
-setI_eq0 [lemma, in mathcomp.ssreflect.finset]
-setI_powerset [lemma, in mathcomp.ssreflect.finset]
-setI0 [lemma, in mathcomp.ssreflect.finset]
-setI1g [lemma, in mathcomp.fingroup.fingroup]
-setKI [lemma, in mathcomp.ssreflect.finset]
-setKU [lemma, in mathcomp.ssreflect.finset]
-setOps [section, in mathcomp.ssreflect.finset]
-setOpsAlgebra [section, in mathcomp.ssreflect.finset]
-setOpsAlgebra.T [variable, in mathcomp.ssreflect.finset]
-setOpsDefs [section, in mathcomp.ssreflect.finset]
-setOpsDefs.T [variable, in mathcomp.ssreflect.finset]
-setOps.T [variable, in mathcomp.ssreflect.finset]
-setP [lemma, in mathcomp.ssreflect.finset]
-setSD [lemma, in mathcomp.ssreflect.finset]
-setSI [lemma, in mathcomp.ssreflect.finset]
-setSU [lemma, in mathcomp.ssreflect.finset]
-setT [abbreviation, in mathcomp.ssreflect.finset]
-setTD [lemma, in mathcomp.ssreflect.finset]
-setTfor [definition, in mathcomp.ssreflect.finset]
-setTI [lemma, in mathcomp.ssreflect.finset]
-setTU [lemma, in mathcomp.ssreflect.finset]
-SetType [section, in mathcomp.ssreflect.finset]
-SetType.T [variable, in mathcomp.ssreflect.finset]
-setU [definition, in mathcomp.ssreflect.finset]
-setUA [lemma, in mathcomp.ssreflect.finset]
-setUAC [lemma, in mathcomp.ssreflect.finset]
-setUACA [lemma, in mathcomp.ssreflect.finset]
-setUC [lemma, in mathcomp.ssreflect.finset]
-setUCA [lemma, in mathcomp.ssreflect.finset]
-setUCr [lemma, in mathcomp.ssreflect.finset]
-setUid [lemma, in mathcomp.ssreflect.finset]
-setUidPl [lemma, in mathcomp.ssreflect.finset]
-setUidPr [lemma, in mathcomp.ssreflect.finset]
-setUIl [lemma, in mathcomp.ssreflect.finset]
-setUIr [lemma, in mathcomp.ssreflect.finset]
-setUK [lemma, in mathcomp.ssreflect.finset]
-setUP [lemma, in mathcomp.ssreflect.finset]
-setUS [lemma, in mathcomp.ssreflect.finset]
-setUSS [lemma, in mathcomp.ssreflect.finset]
-setUT [lemma, in mathcomp.ssreflect.finset]
-setUUl [lemma, in mathcomp.ssreflect.finset]
-setUUr [lemma, in mathcomp.ssreflect.finset]
-setU_eq0 [lemma, in mathcomp.ssreflect.finset]
-setU0 [lemma, in mathcomp.ssreflect.finset]
-setU1K [lemma, in mathcomp.ssreflect.finset]
-setU1P [lemma, in mathcomp.ssreflect.finset]
-setU1r [lemma, in mathcomp.ssreflect.finset]
-setU11 [lemma, in mathcomp.ssreflect.finset]
-setX [definition, in mathcomp.ssreflect.finset]
-setXP [lemma, in mathcomp.ssreflect.finset]
-setXS [lemma, in mathcomp.ssreflect.finset]
-setX_gen [lemma, in mathcomp.fingroup.gproduct]
-setX_dprod [lemma, in mathcomp.fingroup.gproduct]
-setX_prod [lemma, in mathcomp.fingroup.gproduct]
-set_gring_classM_coef [lemma, in mathcomp.character.integral_char]
-set_of_coset [projection, in mathcomp.fingroup.quotient]
-set_Frobenius_compl [lemma, in mathcomp.solvable.frobenius]
-set_nth_default [lemma, in mathcomp.ssreflect.seq]
-set_set_nth [lemma, in mathcomp.ssreflect.seq]
-set_nth_nil [lemma, in mathcomp.ssreflect.seq]
-set_nth [definition, in mathcomp.ssreflect.seq]
-set_invgM [lemma, in mathcomp.fingroup.fingroup]
-set_invgK [lemma, in mathcomp.fingroup.fingroup]
-set_mulgA [lemma, in mathcomp.fingroup.fingroup]
-set_mul1g [lemma, in mathcomp.fingroup.fingroup]
-set_invg [definition, in mathcomp.fingroup.fingroup]
-set_mulg [definition, in mathcomp.fingroup.fingroup]
-set_partition_big [lemma, in mathcomp.ssreflect.finset]
-set_partition_big_cond [lemma, in mathcomp.ssreflect.finset]
-set_cons [lemma, in mathcomp.ssreflect.finset]
-set_0Vmem [lemma, in mathcomp.ssreflect.finset]
-set_finMixin [definition, in mathcomp.ssreflect.finset]
-set_countMixin [definition, in mathcomp.ssreflect.finset]
-set_choiceMixin [definition, in mathcomp.ssreflect.finset]
-set_eqMixin [definition, in mathcomp.ssreflect.finset]
-set_of [definition, in mathcomp.ssreflect.finset]
-set_type [inductive, in mathcomp.ssreflect.finset]
-set0 [definition, in mathcomp.ssreflect.finset]
-set0D [lemma, in mathcomp.ssreflect.finset]
-set0I [lemma, in mathcomp.ssreflect.finset]
-set0Pn [lemma, in mathcomp.ssreflect.finset]
-set0U [lemma, in mathcomp.ssreflect.finset]
-set1 [definition, in mathcomp.ssreflect.finset]
-set1gE [lemma, in mathcomp.fingroup.fingroup]
-set1gP [lemma, in mathcomp.fingroup.fingroup]
-set1P [lemma, in mathcomp.ssreflect.finset]
-set1Ul [lemma, in mathcomp.ssreflect.finset]
-set1Ur [lemma, in mathcomp.ssreflect.finset]
-set1_inj [lemma, in mathcomp.ssreflect.finset]
-set11 [lemma, in mathcomp.ssreflect.finset]
-set2P [lemma, in mathcomp.ssreflect.finset]
-set21 [lemma, in mathcomp.ssreflect.finset]
-set22 [lemma, in mathcomp.ssreflect.finset]
-sG [abbreviation, in mathcomp.character.mxrepresentation]
-sgr [abbreviation, in mathcomp.algebra.rat]
-sgr [abbreviation, in mathcomp.algebra.ssrint]
-sgrEz [lemma, in mathcomp.algebra.ssrint]
-sgrMz [lemma, in mathcomp.algebra.ssrint]
-sgrz [lemma, in mathcomp.algebra.ssrint]
-sgr_numq [lemma, in mathcomp.algebra.rat]
-sgr_numq_div [lemma, in mathcomp.algebra.rat]
-sgr_denq [lemma, in mathcomp.algebra.rat]
-sgr_scalq [lemma, in mathcomp.algebra.rat]
-sgval [definition, in mathcomp.fingroup.fingroup]
-sgvalK [lemma, in mathcomp.fingroup.fingroup]
-sgvalM [lemma, in mathcomp.fingroup.fingroup]
-sgvalmK [lemma, in mathcomp.fingroup.morphism]
-sgval_sub [lemma, in mathcomp.fingroup.morphism]
-sgz [definition, in mathcomp.algebra.ssrint]
-Sgz [section, in mathcomp.algebra.ssrint]
-sgzE [definition, in mathcomp.algebra.ssrint]
-sgzM [lemma, in mathcomp.algebra.ssrint]
-sgzN [lemma, in mathcomp.algebra.ssrint]
-SgzNeg [constructor, in mathcomp.algebra.ssrint]
-SgzNull [constructor, in mathcomp.algebra.ssrint]
-sgzN1 [lemma, in mathcomp.algebra.ssrint]
-sgzP [lemma, in mathcomp.algebra.ssrint]
-SgzPos [constructor, in mathcomp.algebra.ssrint]
-SgzReal [section, in mathcomp.algebra.ssrint]
-SgzReal.R [variable, in mathcomp.algebra.ssrint]
-sgzX [lemma, in mathcomp.algebra.ssrint]
-sgz_lead_primitive [lemma, in mathcomp.algebra.intdiv]
-sgz_contents [lemma, in mathcomp.algebra.intdiv]
-sgz_eq [lemma, in mathcomp.algebra.ssrint]
-sgz_smul [lemma, in mathcomp.algebra.ssrint]
-sgz_le0 [lemma, in mathcomp.algebra.ssrint]
-sgz_ge0 [lemma, in mathcomp.algebra.ssrint]
-sgz_lt0 [lemma, in mathcomp.algebra.ssrint]
-sgz_gt0 [lemma, in mathcomp.algebra.ssrint]
-sgz_odd [lemma, in mathcomp.algebra.ssrint]
-sgz_eq0 [lemma, in mathcomp.algebra.ssrint]
-sgz_val [inductive, in mathcomp.algebra.ssrint]
-sgz_cp0 [lemma, in mathcomp.algebra.ssrint]
-sgz_id [lemma, in mathcomp.algebra.ssrint]
-sgz_int [lemma, in mathcomp.algebra.ssrint]
-sgz_sgr [lemma, in mathcomp.algebra.ssrint]
-sgz_def [lemma, in mathcomp.algebra.ssrint]
-Sgz.R [variable, in mathcomp.algebra.ssrint]
-sgz0 [lemma, in mathcomp.algebra.ssrint]
-sgz1 [lemma, in mathcomp.algebra.ssrint]
-sh [definition, in mathcomp.solvable.burnside_app]
-Sh [definition, in mathcomp.solvable.burnside_app]
-shape [definition, in mathcomp.ssreflect.seq]
-shape_rev [lemma, in mathcomp.ssreflect.seq]
-shorten [definition, in mathcomp.ssreflect.path]
-shortenP [lemma, in mathcomp.ssreflect.path]
-ShortenSpec [constructor, in mathcomp.ssreflect.path]
-shorten_spec [inductive, in mathcomp.ssreflect.path]
-sh_inv [lemma, in mathcomp.solvable.burnside_app]
-Sh_inj [lemma, in mathcomp.solvable.burnside_app]
-SigEqType [section, in mathcomp.ssreflect.eqtype]
-SigEqType.P [variable, in mathcomp.ssreflect.eqtype]
-SigEqType.T [variable, in mathcomp.ssreflect.eqtype]
-signr_scalq [lemma, in mathcomp.algebra.rat]
-SigProj [section, in mathcomp.ssreflect.eqtype]
-SigProj.P [variable, in mathcomp.ssreflect.eqtype]
-SigProj.Q [variable, in mathcomp.ssreflect.eqtype]
-SigProj.T [variable, in mathcomp.ssreflect.eqtype]
-sigW [lemma, in mathcomp.ssreflect.choice]
-sig_countMixin [definition, in mathcomp.ssreflect.choice]
-sig_choiceMixin [definition, in mathcomp.ssreflect.choice]
-sig_eqW [lemma, in mathcomp.ssreflect.choice]
-sig_finMixin [definition, in mathcomp.ssreflect.fintype]
-sig_eqMixin [definition, in mathcomp.ssreflect.eqtype]
-sig2W [lemma, in mathcomp.ssreflect.choice]
-sig2_eqW [lemma, in mathcomp.ssreflect.choice]
-simp [abbreviation, in mathcomp.algebra.matrix]
-simp [abbreviation, in mathcomp.algebra.polydiv]
-simp [abbreviation, in mathcomp.algebra.poly]
-simp [abbreviation, in mathcomp.algebra.mxalgebra]
-Simple [section, in mathcomp.solvable.gseries]
-simple [definition, in mathcomp.solvable.gseries]
-simpleP [lemma, in mathcomp.solvable.gseries]
-simple_Alt5 [lemma, in mathcomp.solvable.alt]
-simple_Alt5_base [lemma, in mathcomp.solvable.alt]
-simple_Alt_3 [lemma, in mathcomp.solvable.alt]
-simple_Socle [lemma, in mathcomp.character.mxrepresentation]
-simple_compsP [lemma, in mathcomp.solvable.jordanholder]
-simple_maxnormal [lemma, in mathcomp.solvable.gseries]
-simple_sol_prime [lemma, in mathcomp.solvable.maximal]
-SimplRel [definition, in mathcomp.ssreflect.ssrbool]
-simpl_rel [definition, in mathcomp.ssreflect.ssrbool]
-simpl_pred_sortE [lemma, in mathcomp.ssreflect.ssrbool]
-size [definition, in mathcomp.ssreflect.seq]
-sizeY [definition, in mathcomp.algebra.polyXY]
-sizeYE [lemma, in mathcomp.algebra.polyXY]
-sizeY_mulX [lemma, in mathcomp.algebra.polyXY]
-sizeY_eq0 [lemma, in mathcomp.algebra.polyXY]
-size_minCpoly [lemma, in mathcomp.field.algC]
-size_traject [lemma, in mathcomp.ssreflect.path]
-size_sort [lemma, in mathcomp.ssreflect.path]
-size_merge [lemma, in mathcomp.ssreflect.path]
-size_minPoly [lemma, in mathcomp.field.fieldext]
-size_Fadjoin_poly [lemma, in mathcomp.field.fieldext]
-size_basis [lemma, in mathcomp.algebra.vector]
-size_rat_int_poly [lemma, in mathcomp.algebra.intdiv]
-size_zprimitive [lemma, in mathcomp.algebra.intdiv]
-size_tuple [lemma, in mathcomp.ssreflect.tuple]
-size_mod_mxminpoly [lemma, in mathcomp.algebra.mxpoly]
-size_mxminpoly [lemma, in mathcomp.algebra.mxpoly]
-size_char_poly [lemma, in mathcomp.algebra.mxpoly]
-size_poly_XmY [lemma, in mathcomp.algebra.polyXY]
-size_poly_XaY [lemma, in mathcomp.algebra.polyXY]
-size_Cyclotomic [lemma, in mathcomp.field.cyclotomic]
-size_cyclotomic [lemma, in mathcomp.field.cyclotomic]
-size_permutations [lemma, in mathcomp.ssreflect.seq]
-size_tally_seq [lemma, in mathcomp.ssreflect.seq]
-size_allpairs [lemma, in mathcomp.ssreflect.seq]
-size_allpairs_dep [lemma, in mathcomp.ssreflect.seq]
-size_reshape [lemma, in mathcomp.ssreflect.seq]
-size_flatten [lemma, in mathcomp.ssreflect.seq]
-size_zip [lemma, in mathcomp.ssreflect.seq]
-size_scanl [lemma, in mathcomp.ssreflect.seq]
-size_pairmap [lemma, in mathcomp.ssreflect.seq]
-size_mkseq [lemma, in mathcomp.ssreflect.seq]
-size_iota [lemma, in mathcomp.ssreflect.seq]
-size_pmap_sub [lemma, in mathcomp.ssreflect.seq]
-size_pmap [lemma, in mathcomp.ssreflect.seq]
-size_map [lemma, in mathcomp.ssreflect.seq]
-size_rem [lemma, in mathcomp.ssreflect.seq]
-size_subseq_leqif [lemma, in mathcomp.ssreflect.seq]
-size_subseq [lemma, in mathcomp.ssreflect.seq]
-size_mask [lemma, in mathcomp.ssreflect.seq]
-size_rotr [lemma, in mathcomp.ssreflect.seq]
-size_incr_nth [lemma, in mathcomp.ssreflect.seq]
-size_undup [lemma, in mathcomp.ssreflect.seq]
-size_eq0 [lemma, in mathcomp.ssreflect.seq]
-size_rev [lemma, in mathcomp.ssreflect.seq]
-size_rot [lemma, in mathcomp.ssreflect.seq]
-size_take [lemma, in mathcomp.ssreflect.seq]
-size_takel [lemma, in mathcomp.ssreflect.seq]
-size_drop [lemma, in mathcomp.ssreflect.seq]
-size_filter [lemma, in mathcomp.ssreflect.seq]
-size_set_nth [lemma, in mathcomp.ssreflect.seq]
-size_belast [lemma, in mathcomp.ssreflect.seq]
-size_rcons [lemma, in mathcomp.ssreflect.seq]
-size_cat [lemma, in mathcomp.ssreflect.seq]
-size_nseq [lemma, in mathcomp.ssreflect.seq]
-size_ncons [lemma, in mathcomp.ssreflect.seq]
-size_behead [lemma, in mathcomp.ssreflect.seq]
-size_cfclass [lemma, in mathcomp.character.inertia]
-size_abelian_type [lemma, in mathcomp.solvable.abelian]
-size_enum_ord [lemma, in mathcomp.ssreflect.fintype]
-size_codom [lemma, in mathcomp.ssreflect.fintype]
-size_image [lemma, in mathcomp.ssreflect.fintype]
-size_map_poly [lemma, in mathcomp.algebra.poly]
-size_comp_poly2 [lemma, in mathcomp.algebra.poly]
-size_comp_poly [lemma, in mathcomp.algebra.poly]
-size_exp [lemma, in mathcomp.algebra.poly]
-size_prod_eq1 [lemma, in mathcomp.algebra.poly]
-size_prod_seq_eq1 [lemma, in mathcomp.algebra.poly]
-size_mul_eq1 [lemma, in mathcomp.algebra.poly]
-size_prod_seq [lemma, in mathcomp.algebra.poly]
-size_prod [lemma, in mathcomp.algebra.poly]
-size_Cmul [lemma, in mathcomp.algebra.poly]
-size_scale [lemma, in mathcomp.algebra.poly]
-size_mul [lemma, in mathcomp.algebra.poly]
-size_comp_poly_leq [lemma, in mathcomp.algebra.poly]
-size_map_polyC [lemma, in mathcomp.algebra.poly]
-size_map_inj_poly [lemma, in mathcomp.algebra.poly]
-size_map_poly_id0 [lemma, in mathcomp.algebra.poly]
-size_Xn_sub_1 [lemma, in mathcomp.algebra.poly]
-size_exp_XsubC [lemma, in mathcomp.algebra.poly]
-size_prod_XsubC [lemma, in mathcomp.algebra.poly]
-size_Mmonic [lemma, in mathcomp.algebra.poly]
-size_monicM [lemma, in mathcomp.algebra.poly]
-size_polyXn [lemma, in mathcomp.algebra.poly]
-size_XmulC [lemma, in mathcomp.algebra.poly]
-size_mulX [lemma, in mathcomp.algebra.poly]
-size_MXaddC [lemma, in mathcomp.algebra.poly]
-size_XaddC [lemma, in mathcomp.algebra.poly]
-size_XsubC [lemma, in mathcomp.algebra.poly]
-size_polyX [lemma, in mathcomp.algebra.poly]
-size_scale_leq [lemma, in mathcomp.algebra.poly]
-size_Msign [lemma, in mathcomp.algebra.poly]
-size_exp_leq [lemma, in mathcomp.algebra.poly]
-size_prod_leq [lemma, in mathcomp.algebra.poly]
-size_proper_mul [lemma, in mathcomp.algebra.poly]
-size_mul_leq [lemma, in mathcomp.algebra.poly]
-size_poly1 [lemma, in mathcomp.algebra.poly]
-size_sum [lemma, in mathcomp.algebra.poly]
-size_addl [lemma, in mathcomp.algebra.poly]
-size_add [lemma, in mathcomp.algebra.poly]
-size_opp [lemma, in mathcomp.algebra.poly]
-size_polyC_leq1 [lemma, in mathcomp.algebra.poly]
-size_poly1P [lemma, in mathcomp.algebra.poly]
-size_poly_gt0 [lemma, in mathcomp.algebra.poly]
-size_poly_leq0P [lemma, in mathcomp.algebra.poly]
-size_poly_leq0 [lemma, in mathcomp.algebra.poly]
-size_poly_eq0 [lemma, in mathcomp.algebra.poly]
-size_poly0 [lemma, in mathcomp.algebra.poly]
-size_poly_eq [lemma, in mathcomp.algebra.poly]
-size_poly [lemma, in mathcomp.algebra.poly]
-size_Poly [lemma, in mathcomp.algebra.poly]
-size_cons_poly [lemma, in mathcomp.algebra.poly]
-size_polyC [lemma, in mathcomp.algebra.poly]
-size_orbit [lemma, in mathcomp.ssreflect.fingraph]
-size0nil [lemma, in mathcomp.ssreflect.seq]
-size1_zip [lemma, in mathcomp.ssreflect.seq]
-size1_polyC [lemma, in mathcomp.algebra.poly]
-size2_zip [lemma, in mathcomp.ssreflect.seq]
-skew_field_dimS [lemma, in mathcomp.field.falgebra]
-skew_field_module_dimS [lemma, in mathcomp.field.falgebra]
-skew_field_module_semisimple [lemma, in mathcomp.field.falgebra]
-skew_field_algid1 [lemma, in mathcomp.field.falgebra]
-small_nil_class [lemma, in mathcomp.solvable.sylow]
-snd_morphM [lemma, in mathcomp.fingroup.gproduct]
-soc [abbreviation, in mathcomp.character.character]
-Socle [definition, in mathcomp.character.mxrepresentation]
-socleP [lemma, in mathcomp.character.mxrepresentation]
-socleType [record, in mathcomp.character.mxrepresentation]
-socle_rsimP [lemma, in mathcomp.character.mxrepresentation]
-socle_irr [lemma, in mathcomp.character.mxrepresentation]
-Socle_iso [lemma, in mathcomp.character.mxrepresentation]
-Socle_direct [lemma, in mathcomp.character.mxrepresentation]
-Socle_semisimple [lemma, in mathcomp.character.mxrepresentation]
-Socle_module [lemma, in mathcomp.character.mxrepresentation]
-socle_finMixin [definition, in mathcomp.character.mxrepresentation]
-socle_countMixin [definition, in mathcomp.character.mxrepresentation]
-socle_finType_subproof [lemma, in mathcomp.character.mxrepresentation]
-socle_choiceMixin [definition, in mathcomp.character.mxrepresentation]
-socle_eqMixin [definition, in mathcomp.character.mxrepresentation]
-socle_mem [lemma, in mathcomp.character.mxrepresentation]
-socle_repr [definition, in mathcomp.character.mxrepresentation]
-socle_module [definition, in mathcomp.character.mxrepresentation]
-socle_simple [lemma, in mathcomp.character.mxrepresentation]
-socle_mult [definition, in mathcomp.character.mxrepresentation]
-socle_base [definition, in mathcomp.character.mxrepresentation]
-socle_sort [inductive, in mathcomp.character.mxrepresentation]
-socle_enum [definition, in mathcomp.character.mxrepresentation]
-socle_exists [lemma, in mathcomp.character.mxrepresentation]
-socle_base_enum [projection, in mathcomp.character.mxrepresentation]
-socle_of_Iirr_bij [lemma, in mathcomp.character.character]
-socle_of_IirrK [lemma, in mathcomp.character.character]
-socle_Iirr0 [lemma, in mathcomp.character.character]
-socle_of_Iirr [definition, in mathcomp.character.character]
-Solvable [section, in mathcomp.solvable.nilpotent]
-solvable [definition, in mathcomp.solvable.nilpotent]
-SolvablePrimeFactor [section, in mathcomp.solvable.maximal]
-SolvablePrimeFactor.G [variable, in mathcomp.solvable.maximal]
-SolvablePrimeFactor.gT [variable, in mathcomp.solvable.maximal]
-solvableS [lemma, in mathcomp.solvable.nilpotent]
-solvable_has_lin_char [lemma, in mathcomp.character.character]
-solvable_irr_extendible_from_det [lemma, in mathcomp.character.inertia]
-solvable_norm_abelem [lemma, in mathcomp.solvable.maximal]
-Solvable.gT [variable, in mathcomp.solvable.nilpotent]
-solvable1 [lemma, in mathcomp.solvable.nilpotent]
-Solver [section, in mathcomp.algebra.vector]
-Solver.K [variable, in mathcomp.algebra.vector]
-Solver.lhs [variable, in mathcomp.algebra.vector]
-Solver.lhsf [variable, in mathcomp.algebra.vector]
-Solver.n [variable, in mathcomp.algebra.vector]
-Solver.rhs [variable, in mathcomp.algebra.vector]
-Solver.vT [variable, in mathcomp.algebra.vector]
-sol_coprime_Sylow_subset [lemma, in mathcomp.solvable.hall]
-sol_coprime_Sylow_trans [lemma, in mathcomp.solvable.hall]
-sol_coprime_Sylow_exists [lemma, in mathcomp.solvable.hall]
-sol_prime_factor_exists [lemma, in mathcomp.solvable.maximal]
-sol_der1_proper [lemma, in mathcomp.solvable.nilpotent]
-SomeHall [section, in mathcomp.solvable.sylow]
-SomeHall.gT [variable, in mathcomp.solvable.sylow]
-Some_inj [lemma, in mathcomp.ssreflect.ssrfun]
-sop [definition, in mathcomp.solvable.burnside_app]
-sop_morph [lemma, in mathcomp.solvable.burnside_app]
-sop_spec [lemma, in mathcomp.solvable.burnside_app]
-sop_inj [lemma, in mathcomp.solvable.burnside_app]
-sort [definition, in mathcomp.ssreflect.path]
-sorted [definition, in mathcomp.ssreflect.path]
-sorted_le_nth [lemma, in mathcomp.ssreflect.path]
-sorted_lt_nth [lemma, in mathcomp.ssreflect.path]
-sorted_uniq [lemma, in mathcomp.ssreflect.path]
-sorted_filter [lemma, in mathcomp.ssreflect.path]
-sorted_divisors_ltn [lemma, in mathcomp.ssreflect.prime]
-sorted_divisors [lemma, in mathcomp.ssreflect.prime]
-sorted_primes [lemma, in mathcomp.ssreflect.prime]
-SortSeq [section, in mathcomp.ssreflect.path]
-SortSeq.leT [variable, in mathcomp.ssreflect.path]
-SortSeq.leT_total [variable, in mathcomp.ssreflect.path]
-SortSeq.T [variable, in mathcomp.ssreflect.path]
-SortSeq.Transitive [section, in mathcomp.ssreflect.path]
-SortSeq.Transitive.leT_tr [variable, in mathcomp.ssreflect.path]
-sort_uniq [lemma, in mathcomp.ssreflect.path]
-sort_sorted [lemma, in mathcomp.ssreflect.path]
-space_choiceMixin [definition, in mathcomp.algebra.vector]
-space_eqMixin [definition, in mathcomp.algebra.vector]
-span [definition, in mathcomp.algebra.vector]
-span_bigcat [lemma, in mathcomp.algebra.vector]
-span_basis [lemma, in mathcomp.algebra.vector]
-span_cat [lemma, in mathcomp.algebra.vector]
-span_cons [lemma, in mathcomp.algebra.vector]
-span_seq1 [lemma, in mathcomp.algebra.vector]
-span_nil [lemma, in mathcomp.algebra.vector]
-span_def [lemma, in mathcomp.algebra.vector]
-span_subvP [lemma, in mathcomp.algebra.vector]
-span_expanded_def [definition, in mathcomp.algebra.vector]
-span_key [lemma, in mathcomp.algebra.vector]
-span_orthogonal [lemma, in mathcomp.character.classfun]
-Special [section, in mathcomp.solvable.maximal]
-special [definition, in mathcomp.solvable.maximal]
-SpecializeExtremals [section, in mathcomp.solvable.extremal]
-SpecializeExtremals.m [variable, in mathcomp.solvable.extremal]
-SpecializeExtremals.p [variable, in mathcomp.solvable.extremal]
-SpecializeExtremals.q [variable, in mathcomp.solvable.extremal]
-Special.A [variable, in mathcomp.solvable.maximal]
-Special.G [variable, in mathcomp.solvable.maximal]
-Special.gT [variable, in mathcomp.solvable.maximal]
-Special.p [variable, in mathcomp.solvable.maximal]
-Split [constructor, in mathcomp.ssreflect.path]
-split [inductive, in mathcomp.ssreflect.path]
-split [definition, in mathcomp.ssreflect.fintype]
-SplitHi [constructor, in mathcomp.ssreflect.fintype]
-splitK [lemma, in mathcomp.ssreflect.fintype]
-Splitl [constructor, in mathcomp.ssreflect.path]
-splitl [inductive, in mathcomp.ssreflect.path]
-SplitLo [constructor, in mathcomp.ssreflect.fintype]
-splitP [lemma, in mathcomp.ssreflect.path]
-splitP [lemma, in mathcomp.ssreflect.fintype]
-splitPl [lemma, in mathcomp.ssreflect.path]
-splitPr [lemma, in mathcomp.ssreflect.path]
-splitP2r [lemma, in mathcomp.ssreflect.path]
-Splitr [constructor, in mathcomp.ssreflect.path]
-splitr [inductive, in mathcomp.ssreflect.path]
-splitsP [lemma, in mathcomp.fingroup.gproduct]
-splits_over [definition, in mathcomp.fingroup.gproduct]
-SplittingField [module, in mathcomp.field.galois]
-splittingFieldFor [definition, in mathcomp.field.galois]
-SplittingFieldFor [section, in mathcomp.field.galois]
-splittingFieldForS [lemma, in mathcomp.field.galois]
-SplittingFieldFor.F [variable, in mathcomp.field.galois]
-SplittingFieldFor.L [variable, in mathcomp.field.galois]
-splittingFieldP [lemma, in mathcomp.field.galois]
-SplittingFieldTheory [section, in mathcomp.field.galois]
-SplittingFieldTheory.F [variable, in mathcomp.field.galois]
-SplittingFieldTheory.L [variable, in mathcomp.field.galois]
-SplittingField.algType [definition, in mathcomp.field.galois]
-SplittingField.axiom [definition, in mathcomp.field.galois]
-SplittingField.base [projection, in mathcomp.field.galois]
-SplittingField.choiceType [definition, in mathcomp.field.galois]
-SplittingField.class [definition, in mathcomp.field.galois]
-SplittingField.Class [constructor, in mathcomp.field.galois]
-SplittingField.ClassDef [section, in mathcomp.field.galois]
-SplittingField.ClassDef.cT [variable, in mathcomp.field.galois]
-SplittingField.ClassDef.F [variable, in mathcomp.field.galois]
-SplittingField.ClassDef.phF [variable, in mathcomp.field.galois]
-SplittingField.ClassDef.T [variable, in mathcomp.field.galois]
-SplittingField.ClassDef.xT [variable, in mathcomp.field.galois]
-SplittingField.class_of [record, in mathcomp.field.galois]
-SplittingField.clone [definition, in mathcomp.field.galois]
-SplittingField.comRingType [definition, in mathcomp.field.galois]
-SplittingField.comUnitRingType [definition, in mathcomp.field.galois]
-SplittingField.eqType [definition, in mathcomp.field.galois]
-SplittingField.Exports [module, in mathcomp.field.galois]
-SplittingField.Exports.SplittingFieldType [abbreviation, in mathcomp.field.galois]
-SplittingField.Exports.splittingFieldType [abbreviation, in mathcomp.field.galois]
-[ splittingFieldType _ of _ ] (form_scope) [notation, in mathcomp.field.galois]
-[ splittingFieldType _ of _ for _ ] (form_scope) [notation, in mathcomp.field.galois]
-SplittingField.FalgType [definition, in mathcomp.field.galois]
-SplittingField.fieldExtType [definition, in mathcomp.field.galois]
-SplittingField.fieldType [definition, in mathcomp.field.galois]
-SplittingField.idomainType [definition, in mathcomp.field.galois]
-SplittingField.lalgType [definition, in mathcomp.field.galois]
-SplittingField.lmodType [definition, in mathcomp.field.galois]
-SplittingField.pack [definition, in mathcomp.field.galois]
-SplittingField.Pack [constructor, in mathcomp.field.galois]
-SplittingField.ringType [definition, in mathcomp.field.galois]
-SplittingField.sort [projection, in mathcomp.field.galois]
-SplittingField.type [record, in mathcomp.field.galois]
-SplittingField.unitAlgType [definition, in mathcomp.field.galois]
-SplittingField.unitRingType [definition, in mathcomp.field.galois]
-SplittingField.vectType [definition, in mathcomp.field.galois]
-SplittingField.xclass [abbreviation, in mathcomp.field.galois]
-SplittingField.zmodType [definition, in mathcomp.field.galois]
-splittingPoly [lemma, in mathcomp.field.galois]
-splitting_galoisField [lemma, in mathcomp.field.galois]
-splitting_normalField [lemma, in mathcomp.field.galois]
-splitting_field_normal [lemma, in mathcomp.field.galois]
-splitting_cyclic_primitive_root [lemma, in mathcomp.character.mxrepresentation]
-split_spec [inductive, in mathcomp.ssreflect.fintype]
-split_subproof [lemma, in mathcomp.ssreflect.fintype]
-split1 [lemma, in mathcomp.algebra.zmodp]
-split1_extraspecial [lemma, in mathcomp.solvable.maximal]
-Split2r [constructor, in mathcomp.ssreflect.path]
-split2r [inductive, in mathcomp.ssreflect.path]
-sqrnD [lemma, in mathcomp.ssreflect.ssrnat]
-sqrnD_sub [lemma, in mathcomp.ssreflect.ssrnat]
-sqrn_inj [lemma, in mathcomp.ssreflect.ssrnat]
-sqrn_gt0 [lemma, in mathcomp.ssreflect.ssrnat]
-sqrn_sub [lemma, in mathcomp.ssreflect.ssrnat]
-sqrt_cfnorm_gt0 [lemma, in mathcomp.character.classfun]
-sqrt_cfnorm_eq0 [lemma, in mathcomp.character.classfun]
-sqrt_cfnorm_ge0 [lemma, in mathcomp.character.classfun]
-sqr_Cint_ge1 [lemma, in mathcomp.field.algC]
-square [definition, in mathcomp.solvable.burnside_app]
-square_coloring_number8 [definition, in mathcomp.solvable.burnside_app]
-square_coloring_number4 [definition, in mathcomp.solvable.burnside_app]
-square_coloring_number2 [definition, in mathcomp.solvable.burnside_app]
-sr [abbreviation, in mathcomp.character.mxrepresentation]
-ssetI [definition, in mathcomp.ssreflect.finset]
-ssimS [abbreviation, in mathcomp.character.mxrepresentation]
-ssralg [library]
-ssrbool [library]
-ssreflect [library]
-ssrfun [library]
-ssrint [library]
-ssrmatching [library]
-ssrnat [library]
-ssrnotations [library]
-ssrnum [library]
-ssval [projection, in mathcomp.ssreflect.fintype]
-ssvalP [projection, in mathcomp.ssreflect.fintype]
-sT [abbreviation, in mathcomp.ssreflect.fintype]
-sT [abbreviation, in mathcomp.fingroup.fingroup]
-sT [abbreviation, in mathcomp.ssreflect.finset]
-stable [lemma, in mathcomp.solvable.burnside_app]
-StableCompositionSeries [section, in mathcomp.solvable.jordanholder]
-StableCompositionSeries.A [variable, in mathcomp.solvable.jordanholder]
-StableCompositionSeries.aT [variable, in mathcomp.solvable.jordanholder]
-StableCompositionSeries.D [variable, in mathcomp.solvable.jordanholder]
-StableCompositionSeries.MaxAinvProps [section, in mathcomp.solvable.jordanholder]
-StableCompositionSeries.MaxAinvProps.K [variable, in mathcomp.solvable.jordanholder]
-StableCompositionSeries.MaxAinvProps.N [variable, in mathcomp.solvable.jordanholder]
-StableCompositionSeries.rT [variable, in mathcomp.solvable.jordanholder]
-StableCompositionSeries.to [variable, in mathcomp.solvable.jordanholder]
-stable_factor [definition, in mathcomp.solvable.gseries]
-stable_rowg_mxK [lemma, in mathcomp.character.mxabelem]
-stab_semiprime [lemma, in mathcomp.solvable.frobenius]
-stab_ntransitiveI [lemma, in mathcomp.solvable.primitive_action]
-stab_ntransitive [lemma, in mathcomp.solvable.primitive_action]
-StandardRepresentation [section, in mathcomp.character.character]
-StandardRepresentation.DsumRepr [section, in mathcomp.character.character]
-StandardRepresentation.DsumRepr.n [variable, in mathcomp.character.character]
-StandardRepresentation.DsumRepr.rG [variable, in mathcomp.character.character]
-StandardRepresentation.G [variable, in mathcomp.character.character]
-StandardRepresentation.gT [variable, in mathcomp.character.character]
-StandardRepresentation.ProdRepr [section, in mathcomp.character.character]
-StandardRepresentation.ProdRepr.n1 [variable, in mathcomp.character.character]
-StandardRepresentation.ProdRepr.n2 [variable, in mathcomp.character.character]
-StandardRepresentation.ProdRepr.rG1 [variable, in mathcomp.character.character]
-StandardRepresentation.ProdRepr.rG2 [variable, in mathcomp.character.character]
-StandardRepresentation.R [variable, in mathcomp.character.character]
-standard_grepr [definition, in mathcomp.character.character]
-standard_irr_coef [definition, in mathcomp.character.character]
-standard_socle [definition, in mathcomp.character.character]
-standard_irr [definition, in mathcomp.character.character]
-strict_adjunction [lemma, in mathcomp.ssreflect.fingraph]
-strongest_coprime_quotient_cent [lemma, in mathcomp.solvable.hall]
-StrongJordanHolder [section, in mathcomp.solvable.jordanholder]
-StrongJordanHolderUniqueness [lemma, in mathcomp.solvable.jordanholder]
-StrongJordanHolder.A [variable, in mathcomp.solvable.jordanholder]
-StrongJordanHolder.aT [variable, in mathcomp.solvable.jordanholder]
-StrongJordanHolder.AuxiliaryLemmas [section, in mathcomp.solvable.jordanholder]
-StrongJordanHolder.AuxiliaryLemmas.A [variable, in mathcomp.solvable.jordanholder]
-StrongJordanHolder.AuxiliaryLemmas.aT [variable, in mathcomp.solvable.jordanholder]
-StrongJordanHolder.AuxiliaryLemmas.D [variable, in mathcomp.solvable.jordanholder]
-StrongJordanHolder.AuxiliaryLemmas.rT [variable, in mathcomp.solvable.jordanholder]
-StrongJordanHolder.AuxiliaryLemmas.to [variable, in mathcomp.solvable.jordanholder]
-StrongJordanHolder.D [variable, in mathcomp.solvable.jordanholder]
-StrongJordanHolder.rT [variable, in mathcomp.solvable.jordanholder]
-StrongJordanHolder.to [variable, in mathcomp.solvable.jordanholder]
-strong_Primitive_Element_Theorem [lemma, in mathcomp.field.separable]
-Sub [abbreviation, in mathcomp.ssreflect.eqtype]
-Sub [projection, in mathcomp.ssreflect.eqtype]
-subact [definition, in mathcomp.fingroup.action]
-SubAction [section, in mathcomp.fingroup.action]
-SubAction.aT [variable, in mathcomp.fingroup.action]
-SubAction.D [variable, in mathcomp.fingroup.action]
-SubAction.rT [variable, in mathcomp.fingroup.action]
-SubAction.sP [variable, in mathcomp.fingroup.action]
-SubAction.sT [variable, in mathcomp.fingroup.action]
-SubAction.to [variable, in mathcomp.fingroup.action]
-subact_is_action [lemma, in mathcomp.fingroup.action]
-subact_dom [definition, in mathcomp.fingroup.action]
-subcentP [lemma, in mathcomp.solvable.center]
-subcent_dprod [lemma, in mathcomp.fingroup.gproduct]
-subcent_sdprod [lemma, in mathcomp.fingroup.gproduct]
-subcent_TImulg [lemma, in mathcomp.fingroup.gproduct]
-subcent_char [lemma, in mathcomp.solvable.center]
-subcent_normal [lemma, in mathcomp.solvable.center]
-subcent_norm [lemma, in mathcomp.solvable.center]
-subcent_sub [lemma, in mathcomp.solvable.center]
-subcent1C [lemma, in mathcomp.solvable.center]
-subcent1P [lemma, in mathcomp.solvable.center]
-subcent1_extraspecial_maximal [lemma, in mathcomp.solvable.maximal]
-subcent1_cycle_normal [lemma, in mathcomp.solvable.center]
-subcent1_cycle_norm [lemma, in mathcomp.solvable.center]
-subcent1_cycle_sub [lemma, in mathcomp.solvable.center]
-subcent1_sub [lemma, in mathcomp.solvable.center]
-subcent1_id [lemma, in mathcomp.solvable.center]
-subCountType [record, in mathcomp.ssreflect.choice]
-SubCountType [constructor, in mathcomp.ssreflect.choice]
-SubCountType [section, in mathcomp.ssreflect.choice]
-SubCountType.P [variable, in mathcomp.ssreflect.choice]
-SubCountType.T [variable, in mathcomp.ssreflect.choice]
-subCount_sort [projection, in mathcomp.ssreflect.choice]
-subCset [lemma, in mathcomp.ssreflect.finset]
-SubDaddsmxSpec [constructor, in mathcomp.algebra.mxalgebra]
-subdom [abbreviation, in mathcomp.fingroup.action]
-subDset [lemma, in mathcomp.ssreflect.finset]
-SubDsumsmxSpec [constructor, in mathcomp.algebra.mxalgebra]
-subD1set [lemma, in mathcomp.ssreflect.finset]
-subEproper [lemma, in mathcomp.ssreflect.finset]
-SubEqMixin [definition, in mathcomp.ssreflect.eqtype]
-SubEqType [section, in mathcomp.ssreflect.eqtype]
-SubEqType.P [variable, in mathcomp.ssreflect.eqtype]
-SubEqType.sT [variable, in mathcomp.ssreflect.eqtype]
-SubEqType.T [variable, in mathcomp.ssreflect.eqtype]
-SubFalgType [section, in mathcomp.field.falgebra]
-SubFalgType.A [variable, in mathcomp.field.falgebra]
-SubFalgType.aT [variable, in mathcomp.field.falgebra]
-SubFalgType.K [variable, in mathcomp.field.falgebra]
-subFExtend [definition, in mathcomp.field.fieldext]
-subfext_idomainMixin [definition, in mathcomp.field.fieldext]
-subfext_fieldMixin [definition, in mathcomp.field.fieldext]
-subfext_unitRingMixin [definition, in mathcomp.field.fieldext]
-subfext_inv [definition, in mathcomp.field.fieldext]
-subfext_comRingMixin [definition, in mathcomp.field.fieldext]
-subfext_mul [definition, in mathcomp.field.fieldext]
-subfext_zmodMixin [definition, in mathcomp.field.fieldext]
-subfext_opp [definition, in mathcomp.field.fieldext]
-subfext_add [definition, in mathcomp.field.fieldext]
-subfext0 [definition, in mathcomp.field.fieldext]
-subfext1 [definition, in mathcomp.field.fieldext]
-SubFieldExtension [section, in mathcomp.field.fieldext]
-SubFieldExtension.F [variable, in mathcomp.field.fieldext]
-SubFieldExtension.iota [variable, in mathcomp.field.fieldext]
-SubFieldExtension.iotaFz [variable, in mathcomp.field.fieldext]
-SubFieldExtension.iotaPz_modp [variable, in mathcomp.field.fieldext]
-SubFieldExtension.iotaPz_repr [variable, in mathcomp.field.fieldext]
-SubFieldExtension.Irreducible [section, in mathcomp.field.fieldext]
-SubFieldExtension.Irreducible.irr_p [variable, in mathcomp.field.fieldext]
-SubFieldExtension.Irreducible.nz_p [variable, in mathcomp.field.fieldext]
-SubFieldExtension.L [variable, in mathcomp.field.fieldext]
-SubFieldExtension.n [variable, in mathcomp.field.fieldext]
-SubFieldExtension.NonZero [section, in mathcomp.field.fieldext]
-SubFieldExtension.NonZero.nz_p [variable, in mathcomp.field.fieldext]
-SubFieldExtension.nz_p0 [variable, in mathcomp.field.fieldext]
-SubFieldExtension.n_gt0 [variable, in mathcomp.field.fieldext]
-SubFieldExtension.p [variable, in mathcomp.field.fieldext]
-SubFieldExtension.poly_rV_modp_K [variable, in mathcomp.field.fieldext]
-SubFieldExtension.pz0 [variable, in mathcomp.field.fieldext]
-SubFieldExtension.p0 [variable, in mathcomp.field.fieldext]
-SubFieldExtension.p0z0 [variable, in mathcomp.field.fieldext]
-SubFieldExtension.p0_mon [variable, in mathcomp.field.fieldext]
-SubFieldExtension.subfx_poly_invE [variable, in mathcomp.field.fieldext]
-SubFieldExtension.wf_p [variable, in mathcomp.field.fieldext]
-SubFieldExtension.z [variable, in mathcomp.field.fieldext]
-SubFieldExtension.z0 [variable, in mathcomp.field.fieldext]
-SubFieldExtension.z0Ciota [variable, in mathcomp.field.fieldext]
-_ ^iota (ring_scope) [notation, in mathcomp.field.fieldext]
-SubFieldExtType [definition, in mathcomp.field.fieldext]
-subfield_closed [lemma, in mathcomp.field.fieldext]
-subFinGroupMixin [definition, in mathcomp.fingroup.fingroup]
-SubFinMixin [definition, in mathcomp.ssreflect.fintype]
-SubFinMixin_for [definition, in mathcomp.ssreflect.fintype]
-subFinType [record, in mathcomp.ssreflect.fintype]
-SubFinType [constructor, in mathcomp.ssreflect.fintype]
-SubFinType [section, in mathcomp.ssreflect.fintype]
-SubFinType.P [variable, in mathcomp.ssreflect.fintype]
-SubFinType.T [variable, in mathcomp.ssreflect.fintype]
-subFin_mixin [definition, in mathcomp.ssreflect.fintype]
-subFin_sort [projection, in mathcomp.ssreflect.fintype]
-subfxE [lemma, in mathcomp.field.fieldext]
-subfxEroot [lemma, in mathcomp.field.fieldext]
-SubfxFalgType [definition, in mathcomp.field.fieldext]
-SubfxVectMixin [definition, in mathcomp.field.fieldext]
-SubfxVectType [definition, in mathcomp.field.fieldext]
-subfx_irreducibleP [lemma, in mathcomp.field.fieldext]
-subfx_inj_base [lemma, in mathcomp.field.fieldext]
-subfx_injZ [lemma, in mathcomp.field.fieldext]
-subfx_inj_root [lemma, in mathcomp.field.fieldext]
-subfx_inj_eval [lemma, in mathcomp.field.fieldext]
-subfx_evalZ [lemma, in mathcomp.field.fieldext]
-subfx_scaleAr [lemma, in mathcomp.field.fieldext]
-subfx_scaleAl [lemma, in mathcomp.field.fieldext]
-subfx_lmodMixin [definition, in mathcomp.field.fieldext]
-subfx_scalerDl [lemma, in mathcomp.field.fieldext]
-subfx_scalerDr [lemma, in mathcomp.field.fieldext]
-subfx_scaler1r [lemma, in mathcomp.field.fieldext]
-subfx_scalerA [lemma, in mathcomp.field.fieldext]
-subfx_scale [definition, in mathcomp.field.fieldext]
-subfx_eval_is_rmorphism [lemma, in mathcomp.field.fieldext]
-subfx_root [definition, in mathcomp.field.fieldext]
-subfx_eval [definition, in mathcomp.field.fieldext]
-subfx_inj_is_rmorphism [lemma, in mathcomp.field.fieldext]
-subfx_inv0 [lemma, in mathcomp.field.fieldext]
-subfx_fieldAxiom [lemma, in mathcomp.field.fieldext]
-subfx_inv_rep [definition, in mathcomp.field.fieldext]
-subfx_poly_inv [definition, in mathcomp.field.fieldext]
-subfx_mul_rep [definition, in mathcomp.field.fieldext]
-subfx_inj [definition, in mathcomp.field.fieldext]
-subg [definition, in mathcomp.fingroup.fingroup]
-Subg [constructor, in mathcomp.fingroup.fingroup]
-subgacentE [lemma, in mathcomp.fingroup.action]
-subgacent1E [lemma, in mathcomp.fingroup.action]
-subGcfker [lemma, in mathcomp.character.character]
-subgK [lemma, in mathcomp.fingroup.fingroup]
-subgM [lemma, in mathcomp.fingroup.fingroup]
-subgmK [lemma, in mathcomp.fingroup.morphism]
-subgP [lemma, in mathcomp.fingroup.fingroup]
-subgroups [definition, in mathcomp.fingroup.fingroup]
-subgroup_transitiveP [lemma, in mathcomp.fingroup.action]
-subgroup_transitivePin [lemma, in mathcomp.fingroup.action]
-subg_mx_abs_irr [lemma, in mathcomp.character.mxrepresentation]
-subg_mx_irr [lemma, in mathcomp.character.mxrepresentation]
-subg_mx_faithful [lemma, in mathcomp.character.mxrepresentation]
-subg_repr [definition, in mathcomp.character.mxrepresentation]
-subg_mx_repr [lemma, in mathcomp.character.mxrepresentation]
-subg_default [lemma, in mathcomp.fingroup.fingroup]
-subg_mulP [lemma, in mathcomp.fingroup.fingroup]
-subg_invP [lemma, in mathcomp.fingroup.fingroup]
-subg_oneP [lemma, in mathcomp.fingroup.fingroup]
-subg_mul [definition, in mathcomp.fingroup.fingroup]
-subg_inv [definition, in mathcomp.fingroup.fingroup]
-subg_one [definition, in mathcomp.fingroup.fingroup]
-subg_inj [lemma, in mathcomp.fingroup.fingroup]
-subg_finMixin [definition, in mathcomp.fingroup.fingroup]
-subg_countMixin [definition, in mathcomp.fingroup.fingroup]
-subg_choiceMixin [definition, in mathcomp.fingroup.fingroup]
-subg_eqMixin [definition, in mathcomp.fingroup.fingroup]
-subg_of [inductive, in mathcomp.fingroup.fingroup]
-subG1 [lemma, in mathcomp.fingroup.fingroup]
-subG1_contra [lemma, in mathcomp.fingroup.fingroup]
-subHall_Sylow [lemma, in mathcomp.solvable.pgroup]
-subHall_Hall [lemma, in mathcomp.solvable.pgroup]
-subIset [lemma, in mathcomp.ssreflect.finset]
-subitv [definition, in mathcomp.algebra.interval]
-subitvP [lemma, in mathcomp.algebra.interval]
-subitvPl [lemma, in mathcomp.algebra.interval]
-subitvPr [lemma, in mathcomp.algebra.interval]
-SubK [lemma, in mathcomp.ssreflect.eqtype]
-subKn [lemma, in mathcomp.ssreflect.ssrnat]
-submod_mx_irr [lemma, in mathcomp.character.mxrepresentation]
-submod_mx_faithful [lemma, in mathcomp.character.mxrepresentation]
-submod_mx_repr [lemma, in mathcomp.character.mxrepresentation]
-submod_mx [definition, in mathcomp.character.mxrepresentation]
-SubMorphism [section, in mathcomp.fingroup.morphism]
-SubMorphism.G [variable, in mathcomp.fingroup.morphism]
-SubMorphism.gT [variable, in mathcomp.fingroup.morphism]
-submx [definition, in mathcomp.algebra.mxalgebra]
-submxE [lemma, in mathcomp.algebra.mxalgebra]
-submxElt [lemma, in mathcomp.algebra.mxalgebra]
-submxK [lemma, in mathcomp.algebra.matrix]
-submxMfree [lemma, in mathcomp.algebra.mxalgebra]
-submxMl [lemma, in mathcomp.algebra.mxalgebra]
-submxMr [lemma, in mathcomp.algebra.mxalgebra]
-submxP [lemma, in mathcomp.algebra.mxalgebra]
-submx_full [lemma, in mathcomp.algebra.mxalgebra]
-submx_trans [lemma, in mathcomp.algebra.mxalgebra]
-submx_refl [lemma, in mathcomp.algebra.mxalgebra]
-submx_key [lemma, in mathcomp.algebra.mxalgebra]
-submx_def [definition, in mathcomp.algebra.mxalgebra]
-submx0 [lemma, in mathcomp.algebra.mxalgebra]
-submx0null [lemma, in mathcomp.algebra.mxalgebra]
-submx1 [lemma, in mathcomp.algebra.mxalgebra]
-subn [definition, in mathcomp.ssreflect.ssrnat]
-subnAC [lemma, in mathcomp.ssreflect.ssrnat]
-subnBA [lemma, in mathcomp.ssreflect.ssrnat]
-subnDA [lemma, in mathcomp.ssreflect.ssrnat]
-subnDl [lemma, in mathcomp.ssreflect.ssrnat]
-subnDr [lemma, in mathcomp.ssreflect.ssrnat]
-subnE [lemma, in mathcomp.ssreflect.ssrnat]
-subnK [lemma, in mathcomp.ssreflect.ssrnat]
-subnKC [lemma, in mathcomp.ssreflect.ssrnat]
-subnn [lemma, in mathcomp.ssreflect.ssrnat]
-Subnormal [section, in mathcomp.solvable.gseries]
-subnormal [definition, in mathcomp.solvable.gseries]
-subnormalEl [lemma, in mathcomp.solvable.gseries]
-subnormalEr [lemma, in mathcomp.solvable.gseries]
-subnormalEsupport [lemma, in mathcomp.solvable.gseries]
-subnormalP [lemma, in mathcomp.solvable.gseries]
-subnormal_sub [lemma, in mathcomp.solvable.gseries]
-subnormal_trans [lemma, in mathcomp.solvable.gseries]
-subnormal_refl [lemma, in mathcomp.solvable.gseries]
-Subnormal.gT [variable, in mathcomp.solvable.gseries]
-Subnormal.path_setIgr [variable, in mathcomp.solvable.gseries]
-Subnormal.setIgr [variable, in mathcomp.solvable.gseries]
-Subnormal.sub_setIgr [variable, in mathcomp.solvable.gseries]
-subnS [lemma, in mathcomp.ssreflect.ssrnat]
-subnSK [lemma, in mathcomp.ssreflect.ssrnat]
-subn_exp [lemma, in mathcomp.ssreflect.binomial]
-subn_sqr [lemma, in mathcomp.ssreflect.ssrnat]
-subn_if_gt [lemma, in mathcomp.ssreflect.ssrnat]
-subn_eq0 [lemma, in mathcomp.ssreflect.ssrnat]
-subn_gt0 [lemma, in mathcomp.ssreflect.ssrnat]
-subn_rec [definition, in mathcomp.ssreflect.ssrnat]
-subn0 [lemma, in mathcomp.ssreflect.ssrnat]
-subn1 [lemma, in mathcomp.ssreflect.ssrnat]
-subn2 [lemma, in mathcomp.ssreflect.ssrnat]
-SubP [lemma, in mathcomp.ssreflect.eqtype]
-subq [definition, in mathcomp.algebra.rat]
-subq_ge0 [lemma, in mathcomp.algebra.rat]
-subr_lersif0 [definition, in mathcomp.algebra.interval]
-subr_lersif0r [lemma, in mathcomp.algebra.interval]
-subr_lersifr0 [lemma, in mathcomp.algebra.interval]
-subseq [definition, in mathcomp.ssreflect.seq]
-Subseq [section, in mathcomp.ssreflect.seq]
-subseqP [lemma, in mathcomp.ssreflect.seq]
-subseq_sorted [lemma, in mathcomp.ssreflect.path]
-subseq_order_path [lemma, in mathcomp.ssreflect.path]
-subseq_uniqP [lemma, in mathcomp.ssreflect.seq]
-subseq_filter [lemma, in mathcomp.ssreflect.seq]
-subseq_uniq [lemma, in mathcomp.ssreflect.seq]
-subseq_rcons [lemma, in mathcomp.ssreflect.seq]
-subseq_cons [lemma, in mathcomp.ssreflect.seq]
-subseq_trans [lemma, in mathcomp.ssreflect.seq]
-subseq_refl [lemma, in mathcomp.ssreflect.seq]
-Subseq.T [variable, in mathcomp.ssreflect.seq]
-subseq0 [lemma, in mathcomp.ssreflect.seq]
-subseries_repr [definition, in mathcomp.character.mxrepresentation]
-subsetC [lemma, in mathcomp.ssreflect.finset]
-subsetD [lemma, in mathcomp.ssreflect.finset]
-SubsetDef [module, in mathcomp.ssreflect.fintype]
-SubsetDefSig [module, in mathcomp.ssreflect.fintype]
-SubsetDefSig.subset [axiom, in mathcomp.ssreflect.fintype]
-SubsetDefSig.subsetEdef [axiom, in mathcomp.ssreflect.fintype]
-SubsetDef.subset [definition, in mathcomp.ssreflect.fintype]
-SubsetDef.subsetEdef [definition, in mathcomp.ssreflect.fintype]
-subsetDl [lemma, in mathcomp.ssreflect.finset]
-subsetDP [lemma, in mathcomp.ssreflect.finset]
-subsetDr [lemma, in mathcomp.ssreflect.finset]
-subsetD1 [lemma, in mathcomp.ssreflect.finset]
-subsetD1P [lemma, in mathcomp.ssreflect.finset]
-subsetE [lemma, in mathcomp.ssreflect.fintype]
-subsetI [lemma, in mathcomp.ssreflect.finset]
-subsetIidl [lemma, in mathcomp.ssreflect.finset]
-subsetIidr [lemma, in mathcomp.ssreflect.finset]
-subsetIl [lemma, in mathcomp.ssreflect.finset]
-subsetIP [lemma, in mathcomp.ssreflect.finset]
-subsetIr [lemma, in mathcomp.ssreflect.finset]
-subsetP [lemma, in mathcomp.ssreflect.fintype]
-subsetPn [lemma, in mathcomp.ssreflect.fintype]
-subsets_disjoint [lemma, in mathcomp.ssreflect.finset]
-subsetT [lemma, in mathcomp.ssreflect.finset]
-subsetT_hint [lemma, in mathcomp.ssreflect.finset]
-subsetU [lemma, in mathcomp.ssreflect.finset]
-subsetUl [lemma, in mathcomp.ssreflect.finset]
-subsetUr [lemma, in mathcomp.ssreflect.finset]
-subsetU1 [lemma, in mathcomp.ssreflect.finset]
-subsetv [definition, in mathcomp.algebra.vector]
-subset_disjoint [lemma, in mathcomp.ssreflect.fintype]
-subset_all [lemma, in mathcomp.ssreflect.fintype]
-subset_trans [lemma, in mathcomp.ssreflect.fintype]
-subset_leqif_card [lemma, in mathcomp.ssreflect.fintype]
-subset_cardP [lemma, in mathcomp.ssreflect.fintype]
-subset_eqP [lemma, in mathcomp.ssreflect.fintype]
-subset_pred1 [lemma, in mathcomp.ssreflect.fintype]
-subset_predT [lemma, in mathcomp.ssreflect.fintype]
-subset_leq_card [lemma, in mathcomp.ssreflect.fintype]
-subset_def [abbreviation, in mathcomp.ssreflect.fintype]
-subset_type [abbreviation, in mathcomp.ssreflect.fintype]
-subset_faithful [lemma, in mathcomp.fingroup.action]
-subset_gen [lemma, in mathcomp.fingroup.fingroup]
-subset_closure [lemma, in mathcomp.ssreflect.fingraph]
-subset_dfs [lemma, in mathcomp.ssreflect.fingraph]
-subset_neq0 [lemma, in mathcomp.ssreflect.finset]
-subset_leqif_cards [lemma, in mathcomp.ssreflect.finset]
-subset0 [lemma, in mathcomp.ssreflect.finset]
-subset1 [lemma, in mathcomp.ssreflect.finset]
-subSKn [lemma, in mathcomp.ssreflect.ssrnat]
-subSn [lemma, in mathcomp.ssreflect.ssrnat]
-subSnn [lemma, in mathcomp.ssreflect.ssrnat]
-subSocle_direct [lemma, in mathcomp.character.mxrepresentation]
-subSocle_iso [lemma, in mathcomp.character.mxrepresentation]
-subSocle_semisimple [lemma, in mathcomp.character.mxrepresentation]
-subSocle_module [lemma, in mathcomp.character.mxrepresentation]
-SubSpec [constructor, in mathcomp.ssreflect.eqtype]
-subSS [lemma, in mathcomp.ssreflect.ssrnat]
-subTset [lemma, in mathcomp.ssreflect.finset]
-subType [record, in mathcomp.ssreflect.eqtype]
-SubType [constructor, in mathcomp.ssreflect.eqtype]
-SubType [section, in mathcomp.ssreflect.eqtype]
-SubType.P [variable, in mathcomp.ssreflect.eqtype]
-SubType.T [variable, in mathcomp.ssreflect.eqtype]
-SubType.Theory [section, in mathcomp.ssreflect.eqtype]
-SubType.Theory.insub_eq_aux [variable, in mathcomp.ssreflect.eqtype]
-SubType.Theory.sT [variable, in mathcomp.ssreflect.eqtype]
-subUset [lemma, in mathcomp.ssreflect.finset]
-subUsetP [lemma, in mathcomp.ssreflect.finset]
-subV [abbreviation, in mathcomp.algebra.vector]
-SubVector [section, in mathcomp.algebra.vector]
-SubVector.K [variable, in mathcomp.algebra.vector]
-SubVector.U [variable, in mathcomp.algebra.vector]
-SubVector.vT [variable, in mathcomp.algebra.vector]
-subvf [lemma, in mathcomp.algebra.vector]
-subvP [lemma, in mathcomp.algebra.vector]
-subvPn [lemma, in mathcomp.algebra.vector]
-subvP_adjoin [lemma, in mathcomp.field.falgebra]
-Subvs [constructor, in mathcomp.algebra.vector]
-subvsP [lemma, in mathcomp.algebra.vector]
-subvs_fieldMixin [lemma, in mathcomp.field.fieldext]
-subvs_mul_eq0 [definition, in mathcomp.field.fieldext]
-subvs_mulC [definition, in mathcomp.field.fieldext]
-subvs_vectMixin [definition, in mathcomp.algebra.vector]
-subvs_vect_iso [lemma, in mathcomp.algebra.vector]
-subvs_inj [lemma, in mathcomp.algebra.vector]
-subvs_lmodMixin [definition, in mathcomp.algebra.vector]
-subvs_zmodMixin [definition, in mathcomp.algebra.vector]
-subvs_choiceMixin [definition, in mathcomp.algebra.vector]
-subvs_eqMixin [definition, in mathcomp.algebra.vector]
-subvs_of [inductive, in mathcomp.algebra.vector]
-subvs_scaleAr [lemma, in mathcomp.field.falgebra]
-subvs_scaleAl [lemma, in mathcomp.field.falgebra]
-subvs_ringMixin [definition, in mathcomp.field.falgebra]
-subvs_mulDr [lemma, in mathcomp.field.falgebra]
-subvs_mulDl [lemma, in mathcomp.field.falgebra]
-subvs_mul1 [lemma, in mathcomp.field.falgebra]
-subvs_mu1l [lemma, in mathcomp.field.falgebra]
-subvs_mulA [lemma, in mathcomp.field.falgebra]
-subvs_mul [definition, in mathcomp.field.falgebra]
-subvs_one [definition, in mathcomp.field.falgebra]
-subvv [lemma, in mathcomp.algebra.vector]
-subv_bigcapP [lemma, in mathcomp.algebra.vector]
-subv_cap [lemma, in mathcomp.algebra.vector]
-subv_sumP [lemma, in mathcomp.algebra.vector]
-subv_add [lemma, in mathcomp.algebra.vector]
-subv_anti [lemma, in mathcomp.algebra.vector]
-subv_trans [lemma, in mathcomp.algebra.vector]
-subv_adjoin_seq [lemma, in mathcomp.field.falgebra]
-subv_adjoin [lemma, in mathcomp.field.falgebra]
-subv_cent1 [lemma, in mathcomp.field.falgebra]
-subv0 [lemma, in mathcomp.algebra.vector]
-subxx [lemma, in mathcomp.ssreflect.fintype]
-subxx_hint [lemma, in mathcomp.ssreflect.fintype]
-subX_agenv [lemma, in mathcomp.field.falgebra]
-subzn [lemma, in mathcomp.algebra.ssrint]
-subzSS [lemma, in mathcomp.algebra.ssrint]
-sub_pcore [lemma, in mathcomp.solvable.pgroup]
-sub_in_pcore [lemma, in mathcomp.solvable.pgroup]
-sub_Hall_pcore [lemma, in mathcomp.solvable.pgroup]
-sub_normal_Hall [lemma, in mathcomp.solvable.pgroup]
-sub_pHall [lemma, in mathcomp.solvable.pgroup]
-sub_in_constt [lemma, in mathcomp.solvable.pgroup]
-sub_p_elt [lemma, in mathcomp.solvable.pgroup]
-sub_pgroup [lemma, in mathcomp.solvable.pgroup]
-sub_cosetpre_quo [lemma, in mathcomp.fingroup.quotient]
-sub_quotient_pre [lemma, in mathcomp.fingroup.quotient]
-sub_cosetpre [lemma, in mathcomp.fingroup.quotient]
-sub_im_coset [lemma, in mathcomp.fingroup.quotient]
-sub_path [lemma, in mathcomp.ssreflect.path]
-sub_conjC_vchar [lemma, in mathcomp.character.vcharacter]
-sub_aut_zchar [lemma, in mathcomp.character.vcharacter]
-sub_baseField [lemma, in mathcomp.field.fieldext]
-sub_adjoin1v [lemma, in mathcomp.field.fieldext]
-sub_pnat_coprime [lemma, in mathcomp.ssreflect.prime]
-sub_in_pnat [lemma, in mathcomp.ssreflect.prime]
-sub_in_partn [lemma, in mathcomp.ssreflect.prime]
-sub_adjoin_separable_generator [lemma, in mathcomp.field.separable]
-sub_inseparable [lemma, in mathcomp.field.separable]
-sub_span [lemma, in mathcomp.algebra.vector]
-sub_annihilant_neq0 [lemma, in mathcomp.algebra.polyXY]
-sub_annihilantP [lemma, in mathcomp.algebra.polyXY]
-sub_annihilant_in_ideal [lemma, in mathcomp.algebra.polyXY]
-sub_annihilant [definition, in mathcomp.algebra.polyXY]
-sub_all [lemma, in mathcomp.ssreflect.seq]
-sub_count [lemma, in mathcomp.ssreflect.seq]
-sub_has [lemma, in mathcomp.ssreflect.seq]
-sub_find [lemma, in mathcomp.ssreflect.seq]
-sub_inertia_Ind [lemma, in mathcomp.character.inertia]
-sub_inertia_Res [lemma, in mathcomp.character.inertia]
-sub_Inertia [lemma, in mathcomp.character.inertia]
-sub_inertia [lemma, in mathcomp.character.inertia]
-sub_countMixin [definition, in mathcomp.ssreflect.choice]
-sub_choiceClass [definition, in mathcomp.ssreflect.choice]
-sub_choiceMixin [definition, in mathcomp.ssreflect.choice]
-sub_Ldiv [lemma, in mathcomp.solvable.abelian]
-sub_LdivT [lemma, in mathcomp.solvable.abelian]
-sub_ordK [lemma, in mathcomp.ssreflect.fintype]
-sub_ord [definition, in mathcomp.ssreflect.fintype]
-sub_ord_proof [lemma, in mathcomp.ssreflect.fintype]
-sub_enum_uniq [lemma, in mathcomp.ssreflect.fintype]
-sub_enum [definition, in mathcomp.ssreflect.fintype]
-sub_proper_trans [lemma, in mathcomp.ssreflect.fintype]
-sub_astabQR [lemma, in mathcomp.fingroup.action]
-sub_astabQ [lemma, in mathcomp.fingroup.action]
-sub_afixRs_norm [lemma, in mathcomp.fingroup.action]
-sub_afixRs_norms [lemma, in mathcomp.fingroup.action]
-sub_act_proof [lemma, in mathcomp.fingroup.action]
-sub_astab1 [lemma, in mathcomp.fingroup.action]
-sub_astab1_in [lemma, in mathcomp.fingroup.action]
-sub_cfker_mod [lemma, in mathcomp.character.classfun]
-sub_morphim_cfker [lemma, in mathcomp.character.classfun]
-sub_cfker_morph [lemma, in mathcomp.character.classfun]
-sub_cfker_Res [lemma, in mathcomp.character.classfun]
-sub_iso_to [lemma, in mathcomp.character.classfun]
-sub_orthonormal [lemma, in mathcomp.character.classfun]
-sub_pairwise_orthogonal [lemma, in mathcomp.character.classfun]
-sub_eqMixin [definition, in mathcomp.ssreflect.eqtype]
-Sub_spec [inductive, in mathcomp.ssreflect.eqtype]
-sub_sort [projection, in mathcomp.ssreflect.eqtype]
-sub_abelem_rV_im [lemma, in mathcomp.character.mxabelem]
-sub_rVabelem_im [lemma, in mathcomp.character.mxabelem]
-sub_rVabelem [lemma, in mathcomp.character.mxabelem]
-sub_im_abelem_rV [lemma, in mathcomp.character.mxabelem]
-sub_rowg_mx [lemma, in mathcomp.character.mxabelem]
-sub_der1_abelian [lemma, in mathcomp.solvable.commutator]
-sub_der1_normal [lemma, in mathcomp.solvable.commutator]
-sub_der1_norm [lemma, in mathcomp.solvable.commutator]
-sub_isog [lemma, in mathcomp.fingroup.morphism]
-sub_isom [lemma, in mathcomp.fingroup.morphism]
-sub_morphpre_injm [lemma, in mathcomp.fingroup.morphism]
-sub_morphpre_im [lemma, in mathcomp.fingroup.morphism]
-sub_morphim_pre [lemma, in mathcomp.fingroup.morphism]
-sub_abelian_normal [lemma, in mathcomp.fingroup.fingroup]
-sub_abelian_norm [lemma, in mathcomp.fingroup.fingroup]
-sub_abelian_cent2 [lemma, in mathcomp.fingroup.fingroup]
-sub_abelian_cent [lemma, in mathcomp.fingroup.fingroup]
-sub_cent1 [lemma, in mathcomp.fingroup.fingroup]
-sub_gcore [lemma, in mathcomp.fingroup.fingroup]
-sub_gen [lemma, in mathcomp.fingroup.fingroup]
-sub_class_support [lemma, in mathcomp.fingroup.fingroup]
-sub_conjgV [lemma, in mathcomp.fingroup.fingroup]
-sub_conjg [lemma, in mathcomp.fingroup.fingroup]
-sub_rcosetV [lemma, in mathcomp.fingroup.fingroup]
-sub_rcoset [lemma, in mathcomp.fingroup.fingroup]
-sub_lcosetV [lemma, in mathcomp.fingroup.fingroup]
-sub_lcoset [lemma, in mathcomp.fingroup.fingroup]
-sub_center_normal [lemma, in mathcomp.solvable.center]
-sub_agenv [lemma, in mathcomp.field.falgebra]
-sub_cyclic_char [lemma, in mathcomp.solvable.cyclic]
-sub_dsumsmx [lemma, in mathcomp.algebra.mxalgebra]
-sub_dsumsmx_spec [inductive, in mathcomp.algebra.mxalgebra]
-sub_daddsmx [lemma, in mathcomp.algebra.mxalgebra]
-sub_daddsmx_spec [inductive, in mathcomp.algebra.mxalgebra]
-sub_bigcapmxP [lemma, in mathcomp.algebra.mxalgebra]
-sub_capmx [lemma, in mathcomp.algebra.mxalgebra]
-sub_capmx_gen [lemma, in mathcomp.algebra.mxalgebra]
-sub_kermxP [lemma, in mathcomp.algebra.mxalgebra]
-sub_sumsmxP [lemma, in mathcomp.algebra.mxalgebra]
-sub_addsmxP [lemma, in mathcomp.algebra.mxalgebra]
-sub_rVP [lemma, in mathcomp.algebra.mxalgebra]
-sub_ltmx_trans [lemma, in mathcomp.algebra.mxalgebra]
-sub_imset_pre [lemma, in mathcomp.ssreflect.finset]
-sub_nilpotent_cent2 [lemma, in mathcomp.solvable.sylow]
-sub0mx [lemma, in mathcomp.algebra.mxalgebra]
-sub0n [lemma, in mathcomp.ssreflect.ssrnat]
-sub0seq [lemma, in mathcomp.ssreflect.seq]
-sub0set [lemma, in mathcomp.ssreflect.finset]
-sub0v [lemma, in mathcomp.algebra.vector]
-sub1b [lemma, in mathcomp.ssreflect.ssrnat]
-sub1G [lemma, in mathcomp.fingroup.fingroup]
-sub1mx [lemma, in mathcomp.algebra.mxalgebra]
-sub1seq [lemma, in mathcomp.ssreflect.seq]
-sub1set [lemma, in mathcomp.ssreflect.finset]
-sub1v [lemma, in mathcomp.field.fieldext]
-sub1_agenv [lemma, in mathcomp.field.falgebra]
-succn [abbreviation, in mathcomp.ssreflect.ssrnat]
-succnK [lemma, in mathcomp.ssreflect.ssrnat]
-succn_inj [lemma, in mathcomp.ssreflect.ssrnat]
-suffix_subseq [lemma, in mathcomp.ssreflect.seq]
-SumEqType [section, in mathcomp.ssreflect.eqtype]
-SumEqType.T1 [variable, in mathcomp.ssreflect.eqtype]
-SumEqType.T2 [variable, in mathcomp.ssreflect.eqtype]
-SumFinType [section, in mathcomp.ssreflect.fintype]
-SumFinType.T1 [variable, in mathcomp.ssreflect.fintype]
-SumFinType.T2 [variable, in mathcomp.ssreflect.fintype]
-sumfv [lemma, in mathcomp.algebra.vector]
-sumKx [abbreviation, in mathcomp.field.fieldext]
-summxE [lemma, in mathcomp.algebra.matrix]
-summx_sub_sums [lemma, in mathcomp.algebra.mxalgebra]
-summx_sub [lemma, in mathcomp.algebra.mxalgebra]
-sumMz [lemma, in mathcomp.algebra.ssrint]
-sumn [definition, in mathcomp.ssreflect.seq]
-sumnE [lemma, in mathcomp.ssreflect.bigop]
-sumn_flatten [lemma, in mathcomp.ssreflect.seq]
-sumn_rev [lemma, in mathcomp.ssreflect.seq]
-sumn_rot [lemma, in mathcomp.ssreflect.seq]
-sumn_rcons [lemma, in mathcomp.ssreflect.seq]
-sumn_count [lemma, in mathcomp.ssreflect.seq]
-sumn_cat [lemma, in mathcomp.ssreflect.seq]
-sumn_nseq [lemma, in mathcomp.ssreflect.seq]
-sumsmxMr [lemma, in mathcomp.algebra.mxalgebra]
-sumsmxMr_gen [lemma, in mathcomp.algebra.mxalgebra]
-sumsmxS [lemma, in mathcomp.algebra.mxalgebra]
-sumsmx_semisimple [lemma, in mathcomp.character.mxrepresentation]
-sumsmx_module [lemma, in mathcomp.character.mxrepresentation]
-sumsmx_subP [lemma, in mathcomp.algebra.mxalgebra]
-sumsmx_sup [lemma, in mathcomp.algebra.mxalgebra]
-sumV [abbreviation, in mathcomp.algebra.vector]
-Sumv [constructor, in mathcomp.algebra.vector]
-SumvPi [section, in mathcomp.algebra.vector]
-SumvPi.K [variable, in mathcomp.algebra.vector]
-SumvPi.vT [variable, in mathcomp.algebra.vector]
-sumv_pi_nat_sum [lemma, in mathcomp.algebra.vector]
-sumv_pi_sum [lemma, in mathcomp.algebra.vector]
-sumv_pi [abbreviation, in mathcomp.algebra.vector]
-sumv_pi_uniq_sum [lemma, in mathcomp.algebra.vector]
-sumv_pi_for [definition, in mathcomp.algebra.vector]
-sumv_sup [lemma, in mathcomp.algebra.vector]
-sum_norm2_char_generators [lemma, in mathcomp.character.integral_char]
-sum_ffun [lemma, in mathcomp.algebra.ssralg]
-sum_ffunE [lemma, in mathcomp.algebra.ssralg]
-sum_irr_degree [lemma, in mathcomp.character.mxrepresentation]
-sum_mxsimple_direct_sub [lemma, in mathcomp.character.mxrepresentation]
-sum_mxsimple_direct_compl [lemma, in mathcomp.character.mxrepresentation]
-sum_lfunE [lemma, in mathcomp.algebra.vector]
-sum_norm_irr_quo [lemma, in mathcomp.character.character]
-sum_countMixin [definition, in mathcomp.ssreflect.choice]
-sum_choiceMixin [definition, in mathcomp.ssreflect.choice]
-sum_of_opair [definition, in mathcomp.ssreflect.choice]
-sum_finMixin [definition, in mathcomp.ssreflect.fintype]
-sum_enum_uniq [lemma, in mathcomp.ssreflect.fintype]
-sum_enum [definition, in mathcomp.ssreflect.fintype]
-sum_card_class [lemma, in mathcomp.fingroup.action]
-sum_by_classes [lemma, in mathcomp.character.classfun]
-sum_cfunE [lemma, in mathcomp.character.classfun]
-sum_nat_eq0 [lemma, in mathcomp.ssreflect.bigop]
-sum_nat_const_nat [lemma, in mathcomp.ssreflect.bigop]
-sum_nat_const [lemma, in mathcomp.ssreflect.bigop]
-sum_index_rcosets_cycle [lemma, in mathcomp.solvable.finmodule]
-sum_eqE [lemma, in mathcomp.ssreflect.eqtype]
-sum_eqP [lemma, in mathcomp.ssreflect.eqtype]
-sum_eq [definition, in mathcomp.ssreflect.eqtype]
-sum_totient_dvd [lemma, in mathcomp.solvable.cyclic]
-sum_ncycle_totient [lemma, in mathcomp.solvable.cyclic]
-sum_nat_cond_const [lemma, in mathcomp.ssreflect.finset]
-sum1dep_card [lemma, in mathcomp.ssreflect.finset]
-sum1_size [lemma, in mathcomp.ssreflect.bigop]
-sum1_count [lemma, in mathcomp.ssreflect.bigop]
-sum1_card [lemma, in mathcomp.ssreflect.bigop]
-support [abbreviation, in mathcomp.algebra.ssralg]
-Support [section, in mathcomp.ssreflect.finfun]
-supportE [lemma, in mathcomp.ssreflect.finfun]
-supportP [lemma, in mathcomp.ssreflect.finfun]
-support_zchar [lemma, in mathcomp.character.vcharacter]
-support_cfAut [lemma, in mathcomp.character.classfun]
-support_cfuni [lemma, in mathcomp.character.classfun]
-support_cfun [lemma, in mathcomp.character.classfun]
-support_for [definition, in mathcomp.ssreflect.finfun]
-Support.aT [variable, in mathcomp.ssreflect.finfun]
-Support.rT [variable, in mathcomp.ssreflect.finfun]
-sup_field_module [lemma, in mathcomp.field.fieldext]
-sv [definition, in mathcomp.solvable.burnside_app]
-Sv [definition, in mathcomp.solvable.burnside_app]
-sval [abbreviation, in mathcomp.ssreflect.eqtype]
-svalP [lemma, in mathcomp.ssreflect.eqtype]
-sv_inv [lemma, in mathcomp.solvable.burnside_app]
-Sv_inj [lemma, in mathcomp.solvable.burnside_app]
-swapXY [definition, in mathcomp.algebra.polyXY]
-swapXYK [lemma, in mathcomp.algebra.polyXY]
-swapXY_map [lemma, in mathcomp.algebra.polyXY]
-swapXY_poly_XmY [lemma, in mathcomp.algebra.polyXY]
-swapXY_poly_XaY [lemma, in mathcomp.algebra.polyXY]
-swapXY_comp_poly [lemma, in mathcomp.algebra.polyXY]
-swapXY_is_scalable [lemma, in mathcomp.algebra.polyXY]
-swapXY_is_multiplicative [lemma, in mathcomp.algebra.polyXY]
-swapXY_eq0 [lemma, in mathcomp.algebra.polyXY]
-swapXY_map_polyC [lemma, in mathcomp.algebra.polyXY]
-swapXY_is_additive [lemma, in mathcomp.algebra.polyXY]
-swapXY_Y [lemma, in mathcomp.algebra.polyXY]
-swapXY_X [lemma, in mathcomp.algebra.polyXY]
-swapXY_polyC [lemma, in mathcomp.algebra.polyXY]
-swapXY_def [definition, in mathcomp.algebra.polyXY]
-swapXY_key [lemma, in mathcomp.algebra.polyXY]
-SwizzleAdd [abbreviation, in mathcomp.algebra.matrix]
-SwizzleLin [abbreviation, in mathcomp.algebra.matrix]
-swizzle_mx_is_scalable [lemma, in mathcomp.algebra.matrix]
-swizzle_mx_is_additive [lemma, in mathcomp.algebra.matrix]
-swizzle_mx [definition, in mathcomp.algebra.matrix]
-Syl [definition, in mathcomp.solvable.pgroup]
-Sylow [definition, in mathcomp.solvable.pgroup]
-Sylow [section, in mathcomp.solvable.sylow]
-sylow [library]
-SylowJ [lemma, in mathcomp.solvable.pgroup]
-SylowP [lemma, in mathcomp.solvable.pgroup]
-SylowSolvableAct [section, in mathcomp.solvable.hall]
-SylowSolvableAct.gT [variable, in mathcomp.solvable.hall]
-SylowSolvableAct.p [variable, in mathcomp.solvable.hall]
-Sylow_subnorm [lemma, in mathcomp.solvable.sylow]
-Sylow_gen [lemma, in mathcomp.solvable.sylow]
-Sylow_transversal_gen [lemma, in mathcomp.solvable.sylow]
-Sylow_setI_normal [lemma, in mathcomp.solvable.sylow]
-Sylow_Jsub [lemma, in mathcomp.solvable.sylow]
-Sylow_subJ [lemma, in mathcomp.solvable.sylow]
-Sylow_trans [lemma, in mathcomp.solvable.sylow]
-Sylow_exists [lemma, in mathcomp.solvable.sylow]
-Sylow_superset [lemma, in mathcomp.solvable.sylow]
-Sylow's_theorem [lemma, in mathcomp.solvable.sylow]
-Sylow.G [variable, in mathcomp.solvable.sylow]
-Sylow.gT [variable, in mathcomp.solvable.sylow]
-Sylow.p [variable, in mathcomp.solvable.sylow]
-Sylow1 [lemma, in mathcomp.solvable.pgroup]
-Sylvester_mxE [lemma, in mathcomp.algebra.mxpoly]
-Sylvester_mx [definition, in mathcomp.algebra.mxpoly]
-Syl_trans [lemma, in mathcomp.solvable.sylow]
-Sym [definition, in mathcomp.solvable.alt]
-SymAltDef [section, in mathcomp.solvable.alt]
-SymAltDef.n [variable, in mathcomp.solvable.alt]
-SymAltDef.T [variable, in mathcomp.solvable.alt]
-'Alt_T [notation, in mathcomp.solvable.alt]
-'Sym_T [notation, in mathcomp.solvable.alt]
-symplectic_type_group_structure [lemma, in mathcomp.solvable.extremal]
-Sym_trans [lemma, in mathcomp.solvable.alt]
-s0 [definition, in mathcomp.solvable.burnside_app]
-S0 [definition, in mathcomp.solvable.burnside_app]
-S0f [definition, in mathcomp.solvable.burnside_app]
-S0_inv [lemma, in mathcomp.solvable.burnside_app]
-s05 [definition, in mathcomp.solvable.burnside_app]
-S05 [definition, in mathcomp.solvable.burnside_app]
-S05f [definition, in mathcomp.solvable.burnside_app]
-S05_inj [lemma, in mathcomp.solvable.burnside_app]
-s1 [definition, in mathcomp.solvable.burnside_app]
-S1 [definition, in mathcomp.solvable.burnside_app]
-S1f [definition, in mathcomp.solvable.burnside_app]
-S1_inv [lemma, in mathcomp.solvable.burnside_app]
-s14 [definition, in mathcomp.solvable.burnside_app]
-S14 [definition, in mathcomp.solvable.burnside_app]
-S14f [definition, in mathcomp.solvable.burnside_app]
-S14_inj [lemma, in mathcomp.solvable.burnside_app]
-s2 [definition, in mathcomp.solvable.burnside_app]
-S2 [definition, in mathcomp.solvable.burnside_app]
-S2f [definition, in mathcomp.solvable.burnside_app]
-s2val [definition, in mathcomp.ssreflect.eqtype]
-s2valP [lemma, in mathcomp.ssreflect.eqtype]
-s2valP' [lemma, in mathcomp.ssreflect.eqtype]
-S2_inv [lemma, in mathcomp.solvable.burnside_app]
-s23 [definition, in mathcomp.solvable.burnside_app]
-S23 [definition, in mathcomp.solvable.burnside_app]
-S23f [definition, in mathcomp.solvable.burnside_app]
-s23_inv [lemma, in mathcomp.solvable.burnside_app]
-S23_inv [lemma, in mathcomp.solvable.burnside_app]
-s3 [definition, in mathcomp.solvable.burnside_app]
-S3 [definition, in mathcomp.solvable.burnside_app]
-S3f [definition, in mathcomp.solvable.burnside_app]
-S3_inv [lemma, in mathcomp.solvable.burnside_app]
-s4 [definition, in mathcomp.solvable.burnside_app]
-S4 [definition, in mathcomp.solvable.burnside_app]
-S4f [definition, in mathcomp.solvable.burnside_app]
-S4_inv [lemma, in mathcomp.solvable.burnside_app]
-s5 [definition, in mathcomp.solvable.burnside_app]
-S5 [definition, in mathcomp.solvable.burnside_app]
-S5f [definition, in mathcomp.solvable.burnside_app]
-S5_inv [lemma, in mathcomp.solvable.burnside_app]
-s6 [definition, in mathcomp.solvable.burnside_app]
-S6 [definition, in mathcomp.solvable.burnside_app]
-S6f [definition, in mathcomp.solvable.burnside_app]
-S6_inv [lemma, 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) | -