| Global Index | +A | +B | +C | +D | +E | +F | +G | +H | +I | +J | +K | +L | +M | +N | +O | +P | +Q | +R | +S | +T | +U | +V | +W | +X | +Y | +Z | +_ | +other | +(23233 entries) | +
| Notation Index | +A | +B | +C | +D | +E | +F | +G | +H | +I | +J | +K | +L | +M | +N | +O | +P | +Q | +R | +S | +T | +U | +V | +W | +X | +Y | +Z | +_ | +other | +(1373 entries) | +
| Module Index | +A | +B | +C | +D | +E | +F | +G | +H | +I | +J | +K | +L | +M | +N | +O | +P | +Q | +R | +S | +T | +U | +V | +W | +X | +Y | +Z | +_ | +other | +(213 entries) | +
| Variable Index | +A | +B | +C | +D | +E | +F | +G | +H | +I | +J | +K | +L | +M | +N | +O | +P | +Q | +R | +S | +T | +U | +V | +W | +X | +Y | +Z | +_ | +other | +(3475 entries) | +
| Library Index | +A | +B | +C | +D | +E | +F | +G | +H | +I | +J | +K | +L | +M | +N | +O | +P | +Q | +R | +S | +T | +U | +V | +W | +X | +Y | +Z | +_ | +other | +(89 entries) | +
| Lemma Index | +A | +B | +C | +D | +E | +F | +G | +H | +I | +J | +K | +L | +M | +N | +O | +P | +Q | +R | +S | +T | +U | +V | +W | +X | +Y | +Z | +_ | +other | +(11853 entries) | +
| Constructor Index | +A | +B | +C | +D | +E | +F | +G | +H | +I | +J | +K | +L | +M | +N | +O | +P | +Q | +R | +S | +T | +U | +V | +W | +X | +Y | +Z | +_ | +other | +(359 entries) | +
| Axiom Index | +A | +B | +C | +D | +E | +F | +G | +H | +I | +J | +K | +L | +M | +N | +O | +P | +Q | +R | +S | +T | +U | +V | +W | +X | +Y | +Z | +_ | +other | +(47 entries) | +
| Inductive Index | +A | +B | +C | +D | +E | +F | +G | +H | +I | +J | +K | +L | +M | +N | +O | +P | +Q | +R | +S | +T | +U | +V | +W | +X | +Y | +Z | +_ | +other | +(103 entries) | +
| Projection Index | +A | +B | +C | +D | +E | +F | +G | +H | +I | +J | +K | +L | +M | +N | +O | +P | +Q | +R | +S | +T | +U | +V | +W | +X | +Y | +Z | +_ | +other | +(266 entries) | +
| Section Index | +A | +B | +C | +D | +E | +F | +G | +H | +I | +J | +K | +L | +M | +N | +O | +P | +Q | +R | +S | +T | +U | +V | +W | +X | +Y | +Z | +_ | +other | +(1118 entries) | +
| Abbreviation Index | +A | +B | +C | +D | +E | +F | +G | +H | +I | +J | +K | +L | +M | +N | +O | +P | +Q | +R | +S | +T | +U | +V | +W | +X | +Y | +Z | +_ | +other | +(691 entries) | +
| Definition Index | +A | +B | +C | +D | +E | +F | +G | +H | +I | +J | +K | +L | +M | +N | +O | +P | +Q | +R | +S | +T | +U | +V | +W | +X | +Y | +Z | +_ | +other | +(3461 entries) | +
| Record Index | +A | +B | +C | +D | +E | +F | +G | +H | +I | +J | +K | +L | +M | +N | +O | +P | +Q | +R | +S | +T | +U | +V | +W | +X | +Y | +Z | +_ | +other | +(185 entries) | +
S
+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_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]
+seq2_ind [lemma, in mathcomp.ssreflect.seq]
+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]
+size [definition, in mathcomp.ssreflect.seq]
+sizeT [definition, in mathcomp.field.closed_field]
+sizeTP [lemma, in mathcomp.field.closed_field]
+sizeT_qf [lemma, in mathcomp.field.closed_field]
+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_allpairs [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 [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_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]
+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_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 [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]
+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_refl [lemma, in mathcomp.ssreflect.seq]
+subseq_trans [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.sT [variable, in mathcomp.ssreflect.eqtype]
+SubType.T [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]
+sumn_flatten [lemma, in mathcomp.ssreflect.seq]
+sumn_rev [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]
+sumpT [definition, in mathcomp.field.closed_field]
+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_dep_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 | +(23233 entries) | +
| Notation Index | +A | +B | +C | +D | +E | +F | +G | +H | +I | +J | +K | +L | +M | +N | +O | +P | +Q | +R | +S | +T | +U | +V | +W | +X | +Y | +Z | +_ | +other | +(1373 entries) | +
| Module Index | +A | +B | +C | +D | +E | +F | +G | +H | +I | +J | +K | +L | +M | +N | +O | +P | +Q | +R | +S | +T | +U | +V | +W | +X | +Y | +Z | +_ | +other | +(213 entries) | +
| Variable Index | +A | +B | +C | +D | +E | +F | +G | +H | +I | +J | +K | +L | +M | +N | +O | +P | +Q | +R | +S | +T | +U | +V | +W | +X | +Y | +Z | +_ | +other | +(3475 entries) | +
| Library Index | +A | +B | +C | +D | +E | +F | +G | +H | +I | +J | +K | +L | +M | +N | +O | +P | +Q | +R | +S | +T | +U | +V | +W | +X | +Y | +Z | +_ | +other | +(89 entries) | +
| Lemma Index | +A | +B | +C | +D | +E | +F | +G | +H | +I | +J | +K | +L | +M | +N | +O | +P | +Q | +R | +S | +T | +U | +V | +W | +X | +Y | +Z | +_ | +other | +(11853 entries) | +
| Constructor Index | +A | +B | +C | +D | +E | +F | +G | +H | +I | +J | +K | +L | +M | +N | +O | +P | +Q | +R | +S | +T | +U | +V | +W | +X | +Y | +Z | +_ | +other | +(359 entries) | +
| Axiom Index | +A | +B | +C | +D | +E | +F | +G | +H | +I | +J | +K | +L | +M | +N | +O | +P | +Q | +R | +S | +T | +U | +V | +W | +X | +Y | +Z | +_ | +other | +(47 entries) | +
| Inductive Index | +A | +B | +C | +D | +E | +F | +G | +H | +I | +J | +K | +L | +M | +N | +O | +P | +Q | +R | +S | +T | +U | +V | +W | +X | +Y | +Z | +_ | +other | +(103 entries) | +
| Projection Index | +A | +B | +C | +D | +E | +F | +G | +H | +I | +J | +K | +L | +M | +N | +O | +P | +Q | +R | +S | +T | +U | +V | +W | +X | +Y | +Z | +_ | +other | +(266 entries) | +
| Section Index | +A | +B | +C | +D | +E | +F | +G | +H | +I | +J | +K | +L | +M | +N | +O | +P | +Q | +R | +S | +T | +U | +V | +W | +X | +Y | +Z | +_ | +other | +(1118 entries) | +
| Abbreviation Index | +A | +B | +C | +D | +E | +F | +G | +H | +I | +J | +K | +L | +M | +N | +O | +P | +Q | +R | +S | +T | +U | +V | +W | +X | +Y | +Z | +_ | +other | +(691 entries) | +
| Definition Index | +A | +B | +C | +D | +E | +F | +G | +H | +I | +J | +K | +L | +M | +N | +O | +P | +Q | +R | +S | +T | +U | +V | +W | +X | +Y | +Z | +_ | +other | +(3461 entries) | +
| Record Index | +A | +B | +C | +D | +E | +F | +G | +H | +I | +J | +K | +L | +M | +N | +O | +P | +Q | +R | +S | +T | +U | +V | +W | +X | +Y | +Z | +_ | +other | +(185 entries) | +