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 | (14626 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 | (165 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 | (112 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 | (7292 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 | (761 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 | (250 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 | (390 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 | (84 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 | (3144 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 | (126 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 | (28 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 | (2221 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 | (53 entries) |

## S

S [abbreviation, in mxrepresentation]sameP [lemma, in ssrbool]

same_count1 [definition, in seq]

same_fconnect1 [lemma, in fingraph]

same_connect_rev [lemma, in fingraph]

same_connect_r [lemma, in fingraph]

same_fconnect_finv [lemma, in fingraph]

same_fconnect1_r [lemma, in fingraph]

same_cover_at [lemma, in finset]

same_connect [lemma, in fingraph]

scalar_mx_cent [lemma, in mxalgebra]

scalar_mx_comm [lemma, in matrix]

scalar_mx_is_multiplicative [lemma, in matrix]

scalar_mxC [lemma, in matrix]

scalar_mx_is_additive [lemma, in matrix]

scalar_mx_sum_delta [lemma, in matrix]

scalar_mx_block [lemma, in matrix]

scalar_mxM [lemma, in matrix]

scalar_mx_rmorphism [definition, in matrix]

scalar_mx_additive [definition, in matrix]

scalar_mx_hom [lemma, in mxrepresentation]

scalar_mx [definition, in matrix]

scalar_mx_is_scalar [lemma, in matrix]

ScaleLapp [section, in vector]

ScaleLapp.f [variable, in vector]

ScaleLapp.R [variable, in vector]

ScaleLapp.V [variable, in vector]

ScaleLapp.W [variable, in vector]

scalemx [definition, in matrix]

scalemxA [lemma, in matrix]

scalemxAl [lemma, in matrix]

scalemxAr [lemma, in matrix]

scalemx_sub [lemma, in mxalgebra]

scalemx_addr [lemma, in matrix]

scalemx_addl [lemma, in matrix]

scalemx_const [lemma, in matrix]

scalemx1 [lemma, in matrix]

scaler_eq0 [lemma, in poly]

scale_lapp_Ar [lemma, in vector]

scale_lapp [definition, in vector]

scale_poly_addr [lemma, in poly]

scale_polyE [lemma, in poly]

scale_actE [lemma, in mxabelem]

scale_col_mx [lemma, in matrix]

scale_1poly [lemma, in poly]

scale_is_action [lemma, in mxabelem]

scale_groupAction [definition, in mxabelem]

scale_action [definition, in mxabelem]

scale_scalar_mx [lemma, in matrix]

scale_poly [definition, in poly]

scale_lapp_Al [lemma, in vector]

scale_polyA [lemma, in poly]

scale_block_mx [lemma, in matrix]

scale_poly1 [lemma, in poly]

scale_lappE [lemma, in vector]

scale_is_groupAction [lemma, in mxabelem]

scale_row_mx [lemma, in matrix]

scale_act [definition, in mxabelem]

scale_poly_addl [lemma, in poly]

scale_poly_mull [lemma, in poly]

scale1mx [lemma, in matrix]

scalp [definition, in poly]

scalp_map [lemma, in poly]

scalp_Ineq0 [lemma, in poly]

Scan [section, in seq]

scanl [definition, in seq]

scanlK [lemma, in seq]

scanl_tuple [definition, in tuple]

scanl_tupleP [lemma, in tuple]

scanl_cat [lemma, in seq]

Scan.f [variable, in seq]

Scan.g [variable, in seq]

Scan.T1 [variable, in seq]

Scan.T2 [variable, in seq]

Scan.x1 [variable, in seq]

Scan.x2 [variable, in seq]

SchurZassenhaus_trans_actsol [lemma, in hall]

SchurZassenhaus_trans_sol [lemma, in hall]

SchurZassenhaus_split [lemma, in hall]

SCN [section, in maximal]

SCN [definition, in maximal]

SCN_P [lemma, in maximal]

SCN_max [lemma, in maximal]

SCN_at [definition, in maximal]

SCN_abelian [lemma, in maximal]

SCN.G [variable, in maximal]

SCN.gT [variable, in maximal]

SCN.p [variable, in maximal]

SCN.SCNseries [section, in maximal]

SCN.SCNseries.A [variable, in maximal]

SCN.SCNseries.SCN_A [variable, in maximal]

SdPair [constructor, in gproduct]

sdpairE [lemma, in gproduct]

sdpair_act [lemma, in gproduct]

sdpair_setact [lemma, in gproduct]

sdpair1 [definition, in gproduct]

sdpair1_morphism [definition, in gproduct]

sdpair1_morphM [lemma, in gproduct]

sdpair2 [definition, in gproduct]

sdpair2_morphism [definition, in gproduct]

sdpair2_morphM [lemma, in gproduct]

sdprod [abbreviation, in gproduct]

sdprod [abbreviation, in gproduct]

sdprodE [lemma, in gproduct]

sdprodEY [lemma, in gproduct]

sdprodg1 [lemma, in gproduct]

sdprodm [definition, in gproduct]

sdprodmE [lemma, in gproduct]

sdprodmEl [lemma, in gproduct]

sdprodmEr [lemma, in gproduct]

sdprodm_morphism [definition, in gproduct]

sdprodm_norm [lemma, in gproduct]

sdprodm_eqf [lemma, in gproduct]

sdprodm_sub [lemma, in gproduct]

sdprodP [lemma, in gproduct]

sdprod_by [inductive, in gproduct]

sdprod_groupType [definition, in gproduct]

sdprod_baseFinGroupType [definition, in gproduct]

sdprod_groupMixin [definition, in gproduct]

sdprod_subFinType [definition, in gproduct]

sdprod_finType [definition, in gproduct]

sdprod_subCountType [definition, in gproduct]

sdprod_countType [definition, in gproduct]

sdprod_choiceType [definition, in gproduct]

sdprod_eqType [definition, in gproduct]

sdprod_subType [definition, in gproduct]

sdprod_finMixin [definition, in gproduct]

sdprod_recr [lemma, in gproduct]

sdprod_choiceMixin [definition, in gproduct]

sdprod_compl [lemma, in gproduct]

sdprod_mul_proof [lemma, in gproduct]

sdprod_one [definition, in gproduct]

sdprod_eqMixin [definition, in gproduct]

sdprod_inv_proof [lemma, in gproduct]

sdprod_card [lemma, in gproduct]

sdprod_normal_complP [lemma, in gproduct]

sdprod_Hall_p'coreP [lemma, in pgroup]

sdprod_normal_p'HallP [lemma, in pgroup]

sdprod_sdpair [lemma, in gproduct]

sdprod_modl [lemma, in gproduct]

sdprod_inv [definition, in gproduct]

sdprod_Hall_pcoreP [lemma, in pgroup]

sdprod_mulVg [lemma, in gproduct]

sdprod_mul1g [lemma, in gproduct]

sdprod_mul [definition, in gproduct]

sdprod_Hall [lemma, in pgroup]

sdprod_countMixin [definition, in gproduct]

sdprod_context [lemma, in gproduct]

sdprod_modr [lemma, in gproduct]

sdprod_recl [lemma, in gproduct]

sdprod_pcore_HallP [lemma, in pgroup]

sdprod_normal_pHallP [lemma, in pgroup]

sdprod_mulgA [lemma, in gproduct]

sdprod_p'core_HallP [lemma, in pgroup]

sdprod1g [lemma, in gproduct]

sdT [abbreviation, in gproduct]

sdval [abbreviation, in gproduct]

Sec [constructor, in jordanholder]

SecondIsomorphism [section, in quotient]

SecondIsomorphism.gT [variable, in quotient]

SecondIsomorphism.H [variable, in quotient]

SecondIsomorphism.K [variable, in quotient]

SecondIsomorphism.nKH [variable, in quotient]

second_isog [lemma, in quotient]

second_isom [lemma, in quotient]

section [inductive, in jordanholder]

Sections [section, in jordanholder]

Sections.gT [variable, in jordanholder]

section_subFinType [definition, in jordanholder]

section_finType [definition, in jordanholder]

section_subCountType [definition, in jordanholder]

section_countType [definition, in jordanholder]

section_choiceType [definition, in jordanholder]

section_eqType [definition, in jordanholder]

section_subType [definition, in jordanholder]

section_group [definition, in jordanholder]

section_finMixin [definition, in jordanholder]

section_repr [definition, in mxrepresentation]

section_eqMixin [definition, in jordanholder]

section_reprP [lemma, in jordanholder]

section_repr [definition, in jordanholder]

section_repr_isog [lemma, in jordanholder]

section_choiceMixin [definition, in jordanholder]

section_module [lemma, in mxrepresentation]

section_countMixin [definition, in jordanholder]

section_isog [definition, in jordanholder]

section_eqmx_add [lemma, in mxrepresentation]

section_eqmx [lemma, in mxrepresentation]

self_inverse [definition, in ssrfun]

SemiDihedral [constructor, in extremal]

semidihedral_structure [lemma, in extremal]

semidihedral_classP [lemma, in extremal]

semidihedral_gtype [definition, in extremal]

semidirect_product [definition, in gproduct]

semiprime [definition, in frobenius]

semiprime_regular [lemma, in frobenius]

semiregular [definition, in frobenius]

semiregular_sym [lemma, in frobenius]

semiregular_prime [lemma, in frobenius]

semiregular1l [lemma, in frobenius]

semiregular1r [lemma, in frobenius]

semisimple_Socle [lemma, in mxrepresentation]

seq [inductive, in seq]

seq [library]

SeqFinType [section, in fintype]

SeqFinType.s [variable, in fintype]

SeqFinType.T [variable, in fintype]

seqn [definition, in seq]

seqn_type [definition, in seq]

seqn_rec [definition, in seq]

SeqSub [constructor, in fintype]

SeqTuple [section, in tuple]

SeqTuple.n [variable, in tuple]

SeqTuple.rT [variable, in tuple]

SeqTuple.T [variable, in tuple]

Sequences [section, in seq]

Sequences.n0 [variable, in seq]

Sequences.SeqFind [section, in seq]

Sequences.SeqFind.a [variable, in seq]

Sequences.T [variable, in seq]

Sequences.x0 [variable, in seq]

seq_countMixin [definition, in choice]

seq_of_tag_countK [lemma, in choice]

seq_sub_countMixin [definition, in fintype]

seq_sub [record, in fintype]

seq_polyXn [lemma, in poly]

seq_sub_pickle [definition, in fintype]

seq_sub_subFinType [definition, in fintype]

seq_sub_finType [definition, in fintype]

seq_sub_subCountType [definition, in fintype]

seq_sub_countType [definition, in fintype]

seq_sub_choiceType [definition, in fintype]

seq_sub_eqType [definition, in fintype]

seq_sub_subType [definition, in fintype]

seq_sub_finMixin [definition, in fintype]

seq_poly0 [lemma, in poly]

seq_sub_unpickle [definition, in fintype]

seq_sub_enum [definition, in fintype]

seq_sub_choiceMixin [definition, in fintype]

seq_countType [definition, in choice]

seq_choiceType [definition, in choice]

seq_of_optK [lemma, in choice]

seq_factor [lemma, in poly]

seq_sub_eqMixin [definition, in fintype]

seq_predType [definition, in seq]

seq_eqType [definition, in seq]

seq_eqMixin [definition, in seq]

seq_mul_polyX [lemma, in poly]

seq_of_tag_count [definition, in choice]

seq_choiceMixin [definition, in choice]

seq_of_opt [definition, in choice]

seq_sub_pickleK [lemma, in fintype]

Seq2 [module, in choice]

seq2_ofK [lemma, in choice]

seq2_of [definition, in choice]

SeriesDefs [section, in nilpotent]

SeriesDefs.A [variable, in nilpotent]

SeriesDefs.gT [variable, in nilpotent]

SeriesDefs.n [variable, in nilpotent]

series_sol [lemma, in nilpotent]

series_repr [definition, in mxrepresentation]

setact [definition, in action]

setactE [lemma, in action]

setactJ [lemma, in action]

setactVin [lemma, in action]

setact_orbit [lemma, in action]

setact_is_action [lemma, in action]

setC [definition, in finset]

setCD [lemma, in finset]

setCI [lemma, in finset]

setCK [lemma, in finset]

setCP [lemma, in finset]

setCS [lemma, in finset]

setCT [lemma, in finset]

setCU [lemma, in finset]

setC_inj [lemma, in finset]

setC_bigcup [lemma, in finset]

setC_bigcap [lemma, in finset]

setC0 [lemma, in finset]

setC11 [lemma, in finset]

setD [definition, in finset]

setDDl [lemma, in finset]

setDDr [lemma, in finset]

setDE [lemma, in finset]

SetDef [module, in finset]

SetDefSig [module, in finset]

SetDefSig.finset [axiom, in finset]

SetDefSig.finsetE [axiom, in finset]

SetDefSig.pred_of_setE [axiom, in finset]

SetDefSig.pred_of_set [axiom, in finset]

SetDef.finset [definition, in finset]

SetDef.finsetE [lemma, in finset]

SetDef.pred_of_set [definition, in finset]

SetDef.pred_of_setE [lemma, in finset]

setDidPl [lemma, in finset]

setDIl [lemma, in finset]

setDIr [lemma, in finset]

setDP [lemma, in finset]

setDS [lemma, in finset]

setDSS [lemma, in finset]

setDT [lemma, in finset]

setDUl [lemma, in finset]

setDUr [lemma, in finset]

setDv [lemma, in finset]

setD_eq0 [lemma, in finset]

setD0 [lemma, in finset]

setD1K [lemma, in finset]

setD1P [lemma, in finset]

setD11 [lemma, in finset]

setI [definition, in finset]

setIA [lemma, in finset]

setIAC [lemma, in finset]

setIC [lemma, in finset]

setICA [lemma, in finset]

setICr [lemma, in finset]

setID [lemma, in finset]

setIdE [lemma, in finset]

setIdP [lemma, in finset]

setIgr [definition, in gseries]

setIg1 [lemma, in fingroup]

setIid [lemma, in finset]

setIidPl [lemma, in finset]

setIidPr [lemma, in finset]

setIIl [lemma, in finset]

setIIr [lemma, in finset]

setIK [lemma, in finset]

setIP [lemma, in finset]

setIS [lemma, in finset]

setISS [lemma, in finset]

setIT [lemma, in finset]

setIUl [lemma, in finset]

setIUr [lemma, in finset]

setI_eq0 [lemma, in finset]

setI_normal_Hall [lemma, in pgroup]

setI_group [definition, in fingroup]

setI_addoid [definition, in finset]

setI_muloid [definition, in finset]

setI_comoid [definition, in finset]

setI_monoid [definition, in finset]

setI_im_cpair [lemma, in center]

setI_subnormal [lemma, in gseries]

setI0 [lemma, in finset]

setI1g [lemma, in fingroup]

setKI [lemma, in finset]

setKU [lemma, in finset]

setOps [section, in finset]

setOpsAlgebra [section, in finset]

setOpsAlgebra.T [variable, in finset]

setOpsDefs [section, in finset]

setOpsDefs.T [variable, in finset]

setOps.T [variable, in finset]

setP [lemma, in finset]

setSD [lemma, in finset]

setSI [lemma, in finset]

setSU [lemma, in finset]

setT [abbreviation, in finset]

setTD [lemma, in finset]

setTfor [definition, in finset]

setTI [lemma, in finset]

setTU [lemma, in finset]

SetType [section, in finset]

SetType.T [variable, in finset]

setT_group [definition, in fingroup]

setU [definition, in finset]

setUA [lemma, in finset]

setUAC [lemma, in finset]

setUC [lemma, in finset]

setUCA [lemma, in finset]

setUCr [lemma, in finset]

setUid [lemma, in finset]

setUidPl [lemma, in finset]

setUidPr [lemma, in finset]

setUIl [lemma, in finset]

setUIr [lemma, in finset]

setUK [lemma, in finset]

setUP [lemma, in finset]

setUS [lemma, in finset]

setUSS [lemma, in finset]

setUT [lemma, in finset]

setUUl [lemma, in finset]

setUUr [lemma, in finset]

setU_addoid [definition, in finset]

setU_muloid [definition, in finset]

setU_comoid [definition, in finset]

setU_monoid [definition, in finset]

setU_eq0 [lemma, in finset]

setU0 [lemma, in finset]

setU1K [lemma, in finset]

setU1P [lemma, in finset]

setU1r [lemma, in finset]

setU11 [lemma, in finset]

setX [definition, in finset]

setXP [lemma, in finset]

setXS [lemma, in finset]

setX_group [definition, in gproduct]

setX_gen [lemma, in gproduct]

setX_dprod [lemma, in gproduct]

setX_prod [lemma, in gproduct]

set_invgK [lemma, in fingroup]

set_partition_big [lemma, in finset]

set_of_subFinType [definition, in finset]

set_of_finType [definition, in finset]

set_of_subCountType [definition, in finset]

set_of_countType [definition, in finset]

set_of_choiceType [definition, in finset]

set_of_eqType [definition, in finset]

set_of_subType [definition, in finset]

set_predType [definition, in finset]

set_subFinType [definition, in finset]

set_finType [definition, in finset]

set_subCountType [definition, in finset]

set_countType [definition, in finset]

set_choiceType [definition, in finset]

set_eqType [definition, in finset]

set_subType [definition, in finset]

set_type [inductive, in finset]

set_mulgA [lemma, in fingroup]

set_invg [definition, in fingroup]

set_set_nth [lemma, in seq]

set_0Vmem [lemma, in finset]

set_nth_nil [lemma, in seq]

set_nth_default [lemma, in seq]

set_nth [definition, in seq]

set_choiceMixin [definition, in finset]

set_invgM [lemma, in fingroup]

set_finMixin [definition, in finset]

set_action [definition, in action]

set_countMixin [definition, in finset]

set_mulg [definition, in fingroup]

set_of_coset [projection, in quotient]

set_cons [lemma, in finset]

set_eqMixin [definition, in finset]

set_of [definition, in finset]

set_mul1g [lemma, in fingroup]

set0 [definition, in finset]

set0D [lemma, in finset]

set0I [lemma, in finset]

set0Pn [lemma, in finset]

set0U [lemma, in finset]

set1 [definition, in finset]

set1gE [lemma, in fingroup]

set1gP [lemma, in fingroup]

set1P [lemma, in finset]

set1Ul [lemma, in finset]

set1Ur [lemma, in finset]

set1_group [definition, in fingroup]

set1_inj [lemma, in finset]

set11 [lemma, in finset]

set2P [lemma, in finset]

set21 [lemma, in finset]

set22 [lemma, in finset]

sfT [definition, in fintype]

sG [abbreviation, in mxrepresentation]

sgval [definition, in fingroup]

sgvalK [lemma, in fingroup]

sgvalM [lemma, in fingroup]

sgvalmK [lemma, in morphism]

sgval_morphism [definition, in morphism]

sgval_sub [lemma, in morphism]

sgzZG [definition, in center]

sgzZZ [definition, in center]

sG_f'fG [definition, in mxrepresentation]

sG_f'fG [definition, in mxrepresentation]

shape [definition, in seq]

sHD [definition, in action]

sHG [definition, in mxrepresentation]

sHG [definition, in quotient]

sHG [definition, in finmodule]

shorten [definition, in path]

shortenP [lemma, in path]

ShortenSpec [constructor, in path]

shorten_spec [inductive, in path]

SigEqType [section, in eqtype]

SigEqType.P [variable, in eqtype]

SigEqType.T [variable, in eqtype]

sign_morph [definition, in alt]

SigProj [section, in eqtype]

SigProj.P [variable, in eqtype]

SigProj.Q [variable, in eqtype]

SigProj.T [variable, in eqtype]

sigW [lemma, in choice]

sig_subFinType [definition, in fintype]

sig_finType [definition, in fintype]

sig_finMixin [definition, in fintype]

sig_choiceMixin [definition, in choice]

sig_eqType [definition, in eqtype]

sig_subType [definition, in eqtype]

sig_eqMixin [definition, in eqtype]

sig_subCountType [definition, in choice]

sig_countType [definition, in choice]

sig_choiceType [definition, in choice]

sig_countMixin [definition, in choice]

sig2W [lemma, in choice]

simp [abbreviation, in poly]

simp [abbreviation, in matrix]

simp [abbreviation, in mxalgebra]

simple [definition, in gseries]

Simple [section, in gseries]

Simple [section, in maximal]

simpleP [lemma, in gseries]

simple_Socle [lemma, in mxrepresentation]

simple_sol_prime [lemma, in maximal]

simple_Alt_3 [lemma, in alt]

simple_maxnormal [lemma, in gseries]

simple_Alt5 [lemma, in alt]

simple_compsP [lemma, in jordanholder]

simple_Alt5_base [lemma, in alt]

SimplFun [section, in ssrfun]

SimplFun [constructor, in ssrfun]

SimplFunDelta [definition, in ssrfun]

SimplFun.aT [variable, in ssrfun]

SimplFun.rT [variable, in ssrfun]

SimplPred [definition, in ssrbool]

simplPredType [definition, in ssrbool]

SimplRel [definition, in ssrbool]

simpl_pred [definition, in ssrbool]

simpl_fun [inductive, in ssrfun]

simpl_mem.pT [variable, in ssrbool]

simpl_rel [definition, in ssrbool]

simpl_mem [section, in ssrbool]

simpl_mem.T [variable, in ssrbool]

simpl_predE [lemma, in ssrbool]

size [definition, in seq]

size_pairmap [lemma, in seq]

size_nseq [lemma, in seq]

size_ncons [lemma, in seq]

size_subseq [lemma, in seq]

size_eqp [lemma, in poly]

size_poly [lemma, in poly]

size_flatten [lemma, in seq]

size_scanl [lemma, in seq]

size_cat [lemma, in seq]

size_abelian_type [lemma, in abelian]

size_scaler [lemma, in poly]

size_sum [lemma, in poly]

size_polyC [lemma, in poly]

size_map_poly [lemma, in poly]

size_mkseq [lemma, in seq]

size_Xn_sub_1 [lemma, in poly]

size_is_basis [lemma, in vector]

size_add [lemma, in poly]

size_char_poly [lemma, in mxpoly]

size_zip [lemma, in seq]

size_loop [definition, in vector]

size_amulX [lemma, in poly]

size_allpairs [lemma, in seq]

size_belast [lemma, in seq]

size_incr_nth [lemma, in seq]

size_mod_mxminpoly [lemma, in mxpoly]

size_poly_cons [lemma, in poly]

size_mxminpoly [lemma, in mxpoly]

size_poly1 [lemma, in poly]

size_poly_eq [lemma, in poly]

size_subseq_leqif [lemma, in seq]

size_mul_monic [lemma, in poly]

size_Poly [lemma, in poly]

size_pmap [lemma, in seq]

size_monic_mul [lemma, in poly]

size_takel [lemma, in seq]

size_drop [lemma, in seq]

size_mul_id [lemma, in poly]

size_rev [lemma, in seq]

size_sign_mul [lemma, in poly]

size_poly0 [lemma, in poly]

size_dvdp [lemma, in poly]

size_poly_eq0 [lemma, in poly]

size_sort [lemma, in path]

size_mask [lemma, in seq]

size_opp [lemma, in poly]

size_take [lemma, in seq]

size_basis [lemma, in vector]

size_exp [lemma, in poly]

size_dvdMp_leqif [lemma, in poly]

size_polyX [lemma, in poly]

size_eq0 [lemma, in seq]

size_set_nth [lemma, in seq]

size_prod_factors [lemma, in poly]

size_enum_ord [lemma, in fintype]

size_rotr [lemma, in seq]

size_merge [lemma, in path]

size_mul [lemma, in poly]

size_proper_mul [lemma, in poly]

size_undup [lemma, in seq]

size_map [lemma, in seq]

size_orbit [lemma, in fingraph]

size_traject [lemma, in path]

size_diagA [definition, in mxpoly]

size_exp_id [lemma, in poly]

size_rot [lemma, in seq]

size_tuple [lemma, in tuple]

size_rcons [lemma, in seq]

size_behead [lemma, in seq]

size_polyC_mul [lemma, in poly]

size_polyXn [lemma, in poly]

size_addl [lemma, in poly]

size_pmap_sub [lemma, in seq]

size_iota [lemma, in seq]

size0nil [lemma, in seq]

size1_polyC [lemma, in poly]

size1_zip [lemma, in seq]

size2_zip [lemma, in seq]

small_nil_class [lemma, in sylow]

snd_morphism [definition, in gproduct]

snd_morphM [lemma, in gproduct]

Socle [definition, in mxrepresentation]

socleP [lemma, in mxrepresentation]

socleType [record, in mxrepresentation]

socle_finType_subproof [lemma, in mxrepresentation]

socle_repr [definition, in mxrepresentation]

socle_eqMixin [definition, in mxrepresentation]

socle_mem [lemma, in mxrepresentation]

socle_base [definition, in mxrepresentation]

socle_base_enum [projection, in mxrepresentation]

socle_subFinType [definition, in mxrepresentation]

socle_finType [definition, in mxrepresentation]

socle_subCountType [definition, in mxrepresentation]

socle_countType [definition, in mxrepresentation]

socle_choiceType [definition, in mxrepresentation]

socle_eqType [definition, in mxrepresentation]

socle_subType [definition, in mxrepresentation]

socle_val [definition, in mxrepresentation]

socle_exists [lemma, in mxrepresentation]

socle_mult [definition, in mxrepresentation]

socle_irr [lemma, in mxrepresentation]

socle_choiceMixin [definition, in mxrepresentation]

socle_rsimP [lemma, in mxrepresentation]

socle_module [definition, in mxrepresentation]

socle_simple [lemma, in mxrepresentation]

Socle_module [lemma, in mxrepresentation]

Socle_semisimple [lemma, in mxrepresentation]

socle_sort [inductive, in mxrepresentation]

Socle_direct [lemma, in mxrepresentation]

socle_finMixin [definition, in mxrepresentation]

socle_countMixin [definition, in mxrepresentation]

socle_enum [definition, in mxrepresentation]

Socle_iso [lemma, in mxrepresentation]

solG' [definition, in hall]

Solvable [section, in nilpotent]

solvable [definition, in nilpotent]

SolvablePrimeFactor [section, in maximal]

SolvablePrimeFactor.G [variable, in maximal]

SolvablePrimeFactor.gT [variable, in maximal]

solvableS [lemma, in nilpotent]

solvable_norm_abelem [lemma, in maximal]

Solvable.gT [variable, in nilpotent]

solvable1 [lemma, in nilpotent]

Solver [section, in vector]

Solver.feq [variable, in vector]

Solver.feq_linear [variable, in vector]

Solver.K [variable, in vector]

Solver.n [variable, in vector]

Solver.V [variable, in vector]

Solver.veq [variable, in vector]

sol_coprime_Sylow_trans [lemma, in hall]

sol_coprime_Sylow_exists [lemma, in hall]

sol_der1_proper [lemma, in nilpotent]

sol_prime_factor_exists [lemma, in maximal]

sol_coprime_Sylow_subset [lemma, in hall]

some [abbreviation, in ssrfun]

SomeChoiceTypes [section, in choice]

SomeChoiceTypes.P [variable, in choice]

SomeChoiceTypes.T [variable, in choice]

SomeHall [section, in sylow]

SomeHall.gT [variable, in sylow]

sort [definition, in path]

sorted [definition, in path]

sorted_sort [lemma, in path]

sorted_divisors_ltn [lemma, in prime]

sorted_divisors [lemma, in prime]

sorted_rev [lemma, in path]

sorted_ltn_iota [lemma, in path]

sorted_ltn_uniq_leq [lemma, in path]

sorted_primes [lemma, in prime]

sorted_filter [lemma, in path]

sorted_uniq [lemma, in path]

sorted_merge [lemma, in path]

sorted_iota [lemma, in path]

SortSeq [section, in path]

SortSeq.leT [variable, in path]

SortSeq.leT_total [variable, in path]

SortSeq.T [variable, in path]

SortSeq.Transitive [section, in path]

SortSeq.Transitive.leT_tr [variable, in path]

sort_of_simpl_pred [definition, in ssrbool]

sort_uniq [lemma, in path]

span [definition, in vector]

span_seq1 [lemma, in vector]

span_nil [lemma, in vector]

span_cons [lemma, in vector]

span_subsetl [lemma, in vector]

span_mx_row [lemma, in vector]

span_bigcat [lemma, in vector]

span_cat [lemma, in vector]

span_mulmx [lemma, in vector]

span_mx [definition, in vector]

span_subset [lemma, in vector]

span_eq [lemma, in vector]

span_vs2mx [lemma, in vector]

special [definition, in maximal]

Special [section, in maximal]

SpecializeExtremals [section, in extremal]

SpecializeExtremals.m [variable, in extremal]

Special.A [variable, in maximal]

Special.G [variable, in maximal]

Special.gT [variable, in maximal]

Special.p [variable, in maximal]

split [definition, in fintype]

split [inductive, in path]

Split [constructor, in path]

SplitHi [constructor, in fintype]

splitK [lemma, in fintype]

splitl [inductive, in path]

Splitl [constructor, in path]

SplitLo [constructor, in fintype]

splitP [lemma, in fintype]

splitP [lemma, in path]

splitPl [lemma, in path]

splitPr [lemma, in path]

splitP2r [lemma, in path]

Splitr [constructor, in path]

splitr [inductive, in path]

splitsP [lemma, in gproduct]

splits_over [definition, in gproduct]

splitting_cyclic_primitive_root [lemma, in mxrepresentation]

split_spec [inductive, in fintype]

split_subproof [lemma, in fintype]

split_diagA [definition, in mxpoly]

split1 [lemma, in zmodp]

split1_extraspecial [lemma, in maximal]

Split2r [constructor, in path]

split2r [inductive, in path]

sqrn_inj [lemma, in ssrnat]

sqrn_sub [lemma, in ssrnat]

sqrn_distn [lemma, in ssrnat]

sqrn_add_sub [lemma, in ssrnat]

sqrn_add [lemma, in ssrnat]

sqrn_gt0 [lemma, in ssrnat]

sr [abbreviation, in mxrepresentation]

ssetI [definition, in finset]

ssGD [definition, in action]

ssimS [abbreviation, in mxrepresentation]

ssralg [library]

ssrbool [library]

ssreflect [library]

ssrfun [library]

ssrnat [library]

SsrSyntax [module, in ssreflect]

ssr_wlog [definition, in ssreflect]

ssr_suff [definition, in ssreflect]

ssr_have [definition, in ssreflect]

ssr_congr_arrow [lemma, in ssreflect]

ssval [projection, in fintype]

ssvalP [projection, in fintype]

sT [abbreviation, in gseries]

sT [abbreviation, in fingroup]

sT [abbreviation, in nilpotent]

sT [abbreviation, in finset]

sT [abbreviation, in nilpotent]

StableCompositionSeries [section, in jordanholder]

StableCompositionSeries.A [variable, in jordanholder]

StableCompositionSeries.aT [variable, in jordanholder]

StableCompositionSeries.D [variable, in jordanholder]

StableCompositionSeries.MaxAinvProps [section, in jordanholder]

StableCompositionSeries.MaxAinvProps.K [variable, in jordanholder]

StableCompositionSeries.MaxAinvProps.N [variable, in jordanholder]

StableCompositionSeries.rT [variable, in jordanholder]

StableCompositionSeries.to [variable, in jordanholder]

stable_factor [definition, in gseries]

stable_rowg_mxK [lemma, in mxabelem]

stab_ntransitive [lemma, in primitive_action]

stab_semiprime [lemma, in frobenius]

stab_ntransitiveI [lemma, in primitive_action]

strict_adjunction [lemma, in fingraph]

strongest_coprime_quotient_cent [lemma, in hall]

StrongJordanHolder [section, in jordanholder]

StrongJordanHolderUniqueness [lemma, in jordanholder]

StrongJordanHolder.A [variable, in jordanholder]

StrongJordanHolder.aT [variable, in jordanholder]

StrongJordanHolder.AuxiliaryLemmas [section, in jordanholder]

StrongJordanHolder.AuxiliaryLemmas.A [variable, in jordanholder]

StrongJordanHolder.AuxiliaryLemmas.aT [variable, in jordanholder]

StrongJordanHolder.AuxiliaryLemmas.D [variable, in jordanholder]

StrongJordanHolder.AuxiliaryLemmas.rT [variable, in jordanholder]

StrongJordanHolder.AuxiliaryLemmas.to [variable, in jordanholder]

StrongJordanHolder.D [variable, in jordanholder]

StrongJordanHolder.rT [variable, in jordanholder]

StrongJordanHolder.to [variable, in jordanholder]

Sub [projection, in eqtype]

subact [definition, in action]

SubAction [section, in action]

subaction [definition, in action]

SubAction.aT [variable, in action]

SubAction.D [variable, in action]

SubAction.rT [variable, in action]

SubAction.sP [variable, in action]

SubAction.sT [variable, in action]

SubAction.to [variable, in action]

subact_dom [definition, in action]

subact_dom_group [definition, in action]

subact_is_action [lemma, in action]

subBaseFinGroupType [definition, in fingroup]

subcentP [lemma, in center]

subcent_dprod [lemma, in gproduct]

subcent_sub [lemma, in center]

subcent_TImulg [lemma, in gproduct]

subcent_char [lemma, in center]

subcent_sdprod [lemma, in gproduct]

subcent_norm [lemma, in center]

subcent_normal [lemma, in center]

subcent1C [lemma, in center]

subcent1P [lemma, in center]

subcent1_cycle_norm [lemma, in center]

subcent1_extraspecial_maximal [lemma, in maximal]

subcent1_cycle_normal [lemma, in center]

subcent1_cycle_sub [lemma, in center]

subcent1_id [lemma, in center]

subcent1_sub [lemma, in center]

SubCountType [section, in choice]

SubCountType [constructor, in choice]

subCountType [record, in choice]

SubCountType.P [variable, in choice]

SubCountType.T [variable, in choice]

subCount_sort [projection, in choice]

subCset [lemma, in finset]

SubDaddsmxSpec [constructor, in mxalgebra]

subdom [abbreviation, in action]

subDset [lemma, in finset]

SubDsumsmxSpec [constructor, in mxalgebra]

subD1set [lemma, in finset]

subEproper [lemma, in finset]

SubEqMixin [definition, in eqtype]

SubEqType [section, in eqtype]

SubEqType.P [variable, in eqtype]

SubEqType.sT [variable, in eqtype]

SubEqType.T [variable, in eqtype]

subFinGroupMixin [definition, in fingroup]

subFinGroupType [definition, in fingroup]

SubFinMixin [definition, in fintype]

SubFinMixin_for [definition, in fintype]

SubFinType [constructor, in fintype]

subFinType [record, in fintype]

SubFinType [section, in fintype]

subFinType_finType [definition, in fintype]

subFinType_subCountType [definition, in fintype]

SubFinType.P [variable, in fintype]

SubFinType.T [variable, in fintype]

subFin_mixin [definition, in fintype]

subFin_sort [projection, in fintype]

Subg [constructor, in fingroup]

subg [definition, in fingroup]

subgacentE [lemma, in action]

subgacent1E [lemma, in action]

subgK [lemma, in fingroup]

subgM [lemma, in fingroup]

subgmK [lemma, in morphism]

subgP [lemma, in fingroup]

subgroups [definition, in fingroup]

subgroup_transitiveP [lemma, in action]

subgroup_transitivePin [lemma, in action]

subg_one [definition, in fingroup]

subg_mx_repr [lemma, in mxrepresentation]

subg_inv [definition, in fingroup]

subg_subFinType [definition, in fingroup]

subg_finType [definition, in fingroup]

subg_subCountType [definition, in fingroup]

subg_countType [definition, in fingroup]

subg_choiceType [definition, in fingroup]

subg_eqType [definition, in fingroup]

subg_subType [definition, in fingroup]

subg_morphism [definition, in morphism]

subg_mx_faithful [lemma, in mxrepresentation]

subg_invP [lemma, in fingroup]

subg_mulP [lemma, in fingroup]

subg_countMixin [definition, in fingroup]

subg_default [lemma, in fingroup]

subg_oneP [lemma, in fingroup]

subg_mul [definition, in fingroup]

subg_mx_abs_irr [lemma, in mxrepresentation]

subg_of [inductive, in fingroup]

subg_choiceMixin [definition, in fingroup]

subg_eqMixin [definition, in fingroup]

subg_finMixin [definition, in fingroup]

subg_repr [definition, in mxrepresentation]

subg_inj [lemma, in fingroup]

subg_mx_irr [lemma, in mxrepresentation]

subG1 [lemma, in fingroup]

subG1_contra [lemma, in fingroup]

subHall_Sylow [lemma, in pgroup]

subHall_Hall [lemma, in pgroup]

subIset [lemma, in finset]

SubK [lemma, in eqtype]

subKn [lemma, in ssrnat]

submod_mx [definition, in mxrepresentation]

submod_repr [definition, in mxrepresentation]

submod_mx_repr [lemma, in mxrepresentation]

submod_mx_faithful [lemma, in mxrepresentation]

submod_mx_irr [lemma, in mxrepresentation]

SubMorphism [section, in morphism]

SubMorphism.G [variable, in morphism]

SubMorphism.gT [variable, in morphism]

submx [definition, in mxalgebra]

submxE [lemma, in mxalgebra]

submxElt [lemma, in mxalgebra]

submxK [lemma, in matrix]

submxMfree [lemma, in mxalgebra]

submxMl [lemma, in mxalgebra]

submxMr [lemma, in mxalgebra]

submxP [lemma, in mxalgebra]

submx_def [definition, in mxalgebra]

submx_trans [lemma, in mxalgebra]

submx_full [lemma, in mxalgebra]

submx_key [lemma, in mxalgebra]

submx_refl [lemma, in mxalgebra]

submx0 [lemma, in mxalgebra]

submx0null [lemma, in mxalgebra]

submx1 [lemma, in mxalgebra]

subn [definition, in ssrnat]

subnAC [lemma, in ssrnat]

subnE [lemma, in ssrnat]

subnK [lemma, in ssrnat]

subnKC [lemma, in ssrnat]

subnn [lemma, in ssrnat]

subnormal [definition, in gseries]

Subnormal [section, in gseries]

subnormalEl [lemma, in gseries]

subnormalEr [lemma, in gseries]

subnormalEsupport [lemma, in gseries]

subnormalP [lemma, in gseries]

subnormal_trans [lemma, in gseries]

subnormal_sub [lemma, in gseries]

subnormal_refl [lemma, in gseries]

Subnormal.gT [variable, in gseries]

subn_add2l [lemma, in ssrnat]

subn_if_gt [lemma, in ssrnat]

subn_sub [lemma, in ssrnat]

subn_exp [lemma, in binomial]

subn_gt0 [lemma, in ssrnat]

subn_add2r [lemma, in ssrnat]

subn_rec [definition, in ssrnat]

subn_sqr [lemma, in ssrnat]

subn_subA [lemma, in ssrnat]

subn_eq0 [lemma, in ssrnat]

subn0 [lemma, in ssrnat]

subn1 [lemma, in ssrnat]

subn2 [lemma, in ssrnat]

subon_bij [lemma, in ssrbool]

subon1 [lemma, in ssrbool]

subon1l [lemma, in ssrbool]

subon2 [lemma, in ssrbool]

SubP [lemma, in eqtype]

subpred [definition, in ssrbool]

subrel [definition, in ssrbool]

subrelUl [lemma, in ssrbool]

subrelUr [lemma, in ssrbool]

subseq [definition, in seq]

Subseq [section, in seq]

subseqP [lemma, in seq]

subseq_refl [lemma, in seq]

subseq_rcons [lemma, in seq]

subseq_cat [lemma, in seq]

subseq_order_path [lemma, in path]

subseq_cons [lemma, in seq]

subseq_seq1 [lemma, in seq]

subseq_trans [lemma, in seq]

subseq_sorted [lemma, in path]

subseq_uniq [lemma, in seq]

Subseq.T [variable, in seq]

subseq0 [lemma, in seq]

subseries_repr [definition, in mxrepresentation]

subsetC [lemma, in finset]

subsetD [lemma, in finset]

SubsetDef [module, in fintype]

SubsetDefSig [module, in fintype]

SubsetDefSig.subset [axiom, in fintype]

SubsetDefSig.subsetEdef [axiom, in fintype]

SubsetDef.subset [definition, in fintype]

SubsetDef.subsetEdef [definition, in fintype]

subsetDl [lemma, in finset]

subsetDP [lemma, in finset]

subsetDr [lemma, in finset]

subsetD1 [lemma, in finset]

subsetD1P [lemma, in finset]

subsetE [lemma, in fintype]

subsetI [lemma, in finset]

subsetIidl [lemma, in finset]

subsetIidr [lemma, in finset]

subsetIl [lemma, in finset]

subsetIP [lemma, in finset]

subsetIr [lemma, in finset]

subsetP [lemma, in fintype]

subsetPn [lemma, in fintype]

subsets_disjoint [lemma, in finset]

subsetT [lemma, in finset]

subsetU [lemma, in finset]

subsetUl [lemma, in finset]

subsetUr [lemma, in finset]

subsetU1 [lemma, in finset]

subsetv [definition, in vector]

subset_closure [lemma, in fingraph]

subset_type [abbreviation, in fintype]

subset_cardP [lemma, in fintype]

subset_gen [lemma, in fingroup]

subset_unlock [definition, in fintype]

subset_dfs [lemma, in fingraph]

subset_predT [lemma, in fintype]

subset_all [lemma, in fintype]

subset_pred1 [lemma, in fintype]

subset_faithful [lemma, in action]

subset_trans [lemma, in fintype]

subset_disjoint [lemma, in fintype]

subset_def [abbreviation, in fintype]

subset_eqP [lemma, in fintype]

subset_leqif_cards [lemma, in finset]

subset_leq_card [lemma, in fintype]

subset_leqif_card [lemma, in fintype]

subset0 [lemma, in finset]

subset1 [lemma, in finset]

subSnn [lemma, in ssrnat]

subSocle_module [lemma, in mxrepresentation]

subSocle_semisimple [lemma, in mxrepresentation]

subSocle_iso [lemma, in mxrepresentation]

subSocle_direct [lemma, in mxrepresentation]

SubSpec [constructor, in eqtype]

subSS [lemma, in ssrnat]

subTset [lemma, in finset]

SubType [constructor, in eqtype]

subType [record, in eqtype]

SubType [section, in eqtype]

SubType.P [variable, in eqtype]

SubType.sT [variable, in eqtype]

SubType.T [variable, in eqtype]

subUset [lemma, in finset]

subUsetP [lemma, in finset]

Subv [constructor, in vector]

SubVectorType [section, in vector]

SubVectorType.K [variable, in vector]

SubVectorType.V [variable, in vector]

SubVectorType.vs [variable, in vector]

subvectP [lemma, in vector]

subvect_scale_addl [lemma, in vector]

subvect_inj [lemma, in vector]

subvect_add0 [lemma, in vector]

subvect_add [definition, in vector]

subvect_lmodMixin [definition, in vector]

subvect_zero [definition, in vector]

subvect_choiceMixin [definition, in vector]

subvect_addA [lemma, in vector]

subvect_addC [lemma, in vector]

subvect_opp [definition, in vector]

subvect_addN [lemma, in vector]

subvect_eqMixin [definition, in vector]

subvect_zmodMixin [definition, in vector]

subvect_is_linear [lemma, in vector]

subvect_scale [definition, in vector]

subvect_scaleA [lemma, in vector]

subvect_scale1 [lemma, in vector]

subvect_VectMixin [definition, in vector]

subvect_bij [lemma, in vector]

subvect_scale_addr [lemma, in vector]

subvect_of [inductive, in vector]

subvect_v2rv [definition, in vector]

subvect_vectType [definition, in vector]

subvect_linear [definition, in vector]

subvect_lmodType [definition, in vector]

subvect_zmodType [definition, in vector]

subvect_choiceType [definition, in vector]

subvect_eqType [definition, in vector]

subvect_subType [definition, in vector]

subvf [lemma, in vector]

subvP [lemma, in vector]

subv_refl [lemma, in vector]

subv_anti [lemma, in vector]

subv_sumP [lemma, in vector]

subv_bigcapP [lemma, in vector]

subv_cap [lemma, in vector]

subv_trans [lemma, in vector]

subv_diffv0 [lemma, in vector]

subv_add [lemma, in vector]

subv0 [lemma, in vector]

subxx [lemma, in fintype]

subxx_hint [lemma, in fintype]

sub_isom [lemma, in morphism]

sub_cosetpre_quo [lemma, in quotient]

sub_normal_Hall [lemma, in pgroup]

sub_der1_norm [lemma, in commutator]

sub_in3 [lemma, in ssrbool]

sub_in21 [lemma, in ssrbool]

sub_in_bij [lemma, in ssrbool]

sub_der1_abelian [lemma, in commutator]

sub_daddsmx_spec [inductive, in mxalgebra]

sub_quotient_pre [lemma, in quotient]

sub_in11 [lemma, in ssrbool]

sub_class_support [lemma, in fingroup]

sub_ord [definition, in fintype]

sub_in2 [lemma, in ssrbool]

sub_abelem_rV_im [lemma, in mxabelem]

sub_dsumsmx_spec [inductive, in mxalgebra]

sub_center_normal [lemma, in center]

sub_in1 [lemma, in ssrbool]

sub_act_proof [lemma, in action]

Sub_spec [inductive, in eqtype]

sub_astabQ [lemma, in action]

sub_qidmx [definition, in mxalgebra]

sub_astab1 [lemma, in action]

sub_capmx [lemma, in mxalgebra]

sub_lcoset [lemma, in fingroup]

sub_morphim_pre [lemma, in morphism]

sub_cyclic_char [lemma, in cyclic]

sub_rcosetV [lemma, in fingroup]

sub_pcore [lemma, in pgroup]

sub_capmx_gen [lemma, in mxalgebra]

sub_enum [definition, in fintype]

sub_im_coset [lemma, in quotient]

sub_in_pnat [lemma, in prime]

sub_mem [definition, in ssrbool]

sub_morphpre_injm [lemma, in morphism]

sub_in111 [lemma, in ssrbool]

sub_proper_trans [lemma, in fintype]

sub_choiceMixin [definition, in choice]

sub_cosetpre [lemma, in quotient]

sub_rcoset [lemma, in fingroup]

sub_Hall_pcore [lemma, in pgroup]

sub_afixRs_norm [lemma, in action]

sub_im_abelem_rV [lemma, in mxabelem]

sub_astab1_in [lemma, in action]

sub_ordK [lemma, in fintype]

sub_lcosetV [lemma, in fingroup]

sub_sumsmxP [lemma, in mxalgebra]

sub_bigcapmxP [lemma, in mxalgebra]

sub_morphpre_im [lemma, in morphism]

sub_abelian_normal [lemma, in fingroup]

sub_in_constt [lemma, in pgroup]

sub_abelian_cent [lemma, in fingroup]

sub_in_pcore [lemma, in pgroup]

sub_rVP [lemma, in mxalgebra]

sub_eqType [definition, in eqtype]

sub_isog [lemma, in morphism]

sub_conjg [lemma, in fingroup]

sub_setIgr [definition, in gseries]

sub_rowg_mx [lemma, in mxabelem]

sub_afixRs_norms [lemma, in action]

sub_Ldiv [lemma, in abelian]

sub_countType [definition, in choice]

sub_choiceType [definition, in choice]

sub_abelian_cent2 [lemma, in fingroup]

sub_rVabelem [lemma, in mxabelem]

sub_pnat_coprime [lemma, in prime]

sub_abelian_norm [lemma, in fingroup]

sub_gen [lemma, in fingroup]

sub_addsmxP [lemma, in mxalgebra]

sub_nilpotent_cent2 [lemma, in sylow]

sub_sort [projection, in eqtype]

sub_eqMixin [definition, in eqtype]

sub_in_partn [lemma, in prime]

sub_enum_uniq [lemma, in fintype]

sub_ltmx_trans [lemma, in mxalgebra]

sub_path [lemma, in path]

sub_in12 [lemma, in ssrbool]

sub_p_elt [lemma, in pgroup]

sub_pgroup [lemma, in pgroup]

sub_pHall [lemma, in pgroup]

sub_sub_minn [lemma, in ssrnat]

sub_daddsmx [lemma, in mxalgebra]

sub_conjgV [lemma, in fingroup]

sub_countMixin [definition, in choice]

sub_astabQR [lemma, in action]

sub_ord_proof [lemma, in fintype]

sub_rVabelem_im [lemma, in mxabelem]

sub_dsumsmx [lemma, in mxalgebra]

sub_der1_normal [lemma, in commutator]

sub_kermxP [lemma, in mxalgebra]

sub_choiceClass [definition, in choice]

sub_cent1 [lemma, in fingroup]

sub_LdivT [lemma, in abelian]

sub_imset_pre [lemma, in finset]

sub0mx [lemma, in mxalgebra]

sub0n [lemma, in ssrnat]

sub0seq [lemma, in seq]

sub0set [lemma, in finset]

sub0v [lemma, in vector]

sub1b [lemma, in ssrnat]

sub1G [lemma, in fingroup]

sub1mx [lemma, in mxalgebra]

sub1set [lemma, in finset]

succn [abbreviation, in ssrnat]

succnK [lemma, in ssrnat]

succn_inj [lemma, in ssrnat]

SumEqType [section, in eqtype]

SumEqType.T1 [variable, in eqtype]

SumEqType.T2 [variable, in eqtype]

SumFinType [section, in fintype]

SumFinType.T1 [variable, in fintype]

SumFinType.T2 [variable, in fintype]

sumfv [lemma, in vector]

summxE [lemma, in matrix]

summx_sub_sums [lemma, in mxalgebra]

summx_sub [lemma, in mxalgebra]

sumn [definition, in seq]

sumn_nseq [lemma, in seq]

sumn_cat [lemma, in seq]

sumsmxMr [lemma, in mxalgebra]

sumsmxMr_gen [lemma, in mxalgebra]

sumsmxS [lemma, in mxalgebra]

sumsmx_subP [lemma, in mxalgebra]

sumsmx_module [lemma, in mxrepresentation]

sumsmx_semisimple [lemma, in mxrepresentation]

sumsmx_sup [lemma, in mxalgebra]

sums_R [definition, in mxrepresentation]

Sumv [constructor, in vector]

sumv_sum_pi [lemma, in vector]

sumv_pi [definition, in vector]

sumv_sup [lemma, in vector]

sum_nat_dep_const [lemma, in finset]

sum_lappE [lemma, in vector]

sum_nat_const_nat [lemma, in bigop]

sum_phi_dvd [lemma, in cyclic]

sum_eq [definition, in eqtype]

sum_finType [definition, in fintype]

sum_finMixin [definition, in fintype]

sum_card_class [lemma, in action]

sum_irr_degree [lemma, in mxrepresentation]

sum_card_rcosets_pcycles [lemma, in finmodule]

sum_enum_uniq [lemma, in fintype]

sum_choiceMixin [definition, in choice]

sum_enum [definition, in fintype]

sum_mxsimple_direct_compl [lemma, in mxrepresentation]

sum_nat_eq0 [lemma, in bigop]

sum_ncycle_phi [lemma, in cyclic]

sum_eqType [definition, in eqtype]

sum_eqMixin [definition, in eqtype]

sum_nat_const [lemma, in bigop]

sum_ffunE [lemma, in ssralg]

sum_countType [definition, in choice]

sum_choiceType [definition, in choice]

sum_countMixin [definition, in choice]

sum_eqE [lemma, in eqtype]

sum_mxsimple_direct_sub [lemma, in mxrepresentation]

sum_mxsum [definition, in mxalgebra]

sum_eqP [lemma, in eqtype]

sum_addv [definition, in vector]

sum0v [lemma, in vector]

sum1dep_card [lemma, in finset]

sum1_card [lemma, in bigop]

support [definition, in finfun]

sval [abbreviation, in eqtype]

svalP [lemma, in eqtype]

sv_val [definition, in vector]

SwizzleAdd [abbreviation, in matrix]

SwizzleLin [abbreviation, in matrix]

swizzle_mx [definition, in matrix]

swizzle_mx_is_additive [lemma, in matrix]

swizzle_mx_scalable [definition, in matrix]

swizzle_mx_additive [definition, in matrix]

swizzle_mx_is_scalable [lemma, in matrix]

Syl [definition, in pgroup]

Sylow [definition, in pgroup]

Sylow [section, in sylow]

sylow [library]

SylowJ [lemma, in pgroup]

SylowP [lemma, in pgroup]

SylowSolvableAct [section, in hall]

SylowSolvableAct.gT [variable, in hall]

SylowSolvableAct.p [variable, in hall]

Sylow_Jsub [lemma, in sylow]

Sylow_superset [lemma, in sylow]

Sylow_gen [lemma, in sylow]

Sylow_subJ [lemma, in sylow]

Sylow_transversal_gen [lemma, in sylow]

Sylow_subnorm [lemma, in sylow]

Sylow_setI_normal [lemma, in sylow]

Sylow_trans [lemma, in sylow]

Sylow_exists [lemma, in sylow]

Sylow's_theorem [lemma, in sylow]

Sylow.G [variable, in sylow]

Sylow.gT [variable, in sylow]

Sylow.p [variable, in sylow]

Sylow1 [lemma, in pgroup]

Sylvester_mx [definition, in mxpoly]

Sylvester_mxE [lemma, in mxpoly]

Syl_trans [lemma, in sylow]

Sym [definition, in alt]

SymAltDef [section, in alt]

SymAltDef.T [variable, in alt]

symmetric [definition, in ssrbool]

symmetric_from_pre [lemma, in ssrbool]

symplectic_type_group_structure [lemma, in extremal]

Sym_trans [lemma, in alt]

Sym_group [definition, in alt]

sZA [definition, in maximal]

sZH [definition, in center]

sZK [definition, in center]

sZS [definition, in mxabelem]

s2val [definition, in eqtype]

s2valP [lemma, in eqtype]

s2valP' [lemma, in eqtype]

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 | (14626 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 | (165 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 | (112 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 | (7292 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 | (761 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 | (250 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 | (390 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 | (84 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 | (3144 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 | (126 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 | (28 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 | (2221 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 | (53 entries) |