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