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)