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 (definition)

same_count1 [in seq]
scalar_mx_rmorphism [in matrix]
scalar_mx_additive [in matrix]
scalar_mx [in matrix]
scalemx [in matrix]
scale_lapp [in vector]
scale_groupAction [in mxabelem]
scale_action [in mxabelem]
scale_poly [in poly]
scale_act [in mxabelem]
scalp [in poly]
scanl [in seq]
scanl_tuple [in tuple]
SCN [in maximal]
SCN_at [in maximal]
sdpair1 [in gproduct]
sdpair1_morphism [in gproduct]
sdpair2 [in gproduct]
sdpair2_morphism [in gproduct]
sdprodm [in gproduct]
sdprodm_morphism [in gproduct]
sdprod_groupType [in gproduct]
sdprod_baseFinGroupType [in gproduct]
sdprod_groupMixin [in gproduct]
sdprod_subFinType [in gproduct]
sdprod_finType [in gproduct]
sdprod_subCountType [in gproduct]
sdprod_countType [in gproduct]
sdprod_choiceType [in gproduct]
sdprod_eqType [in gproduct]
sdprod_subType [in gproduct]
sdprod_finMixin [in gproduct]
sdprod_choiceMixin [in gproduct]
sdprod_one [in gproduct]
sdprod_eqMixin [in gproduct]
sdprod_inv [in gproduct]
sdprod_mul [in gproduct]
sdprod_countMixin [in gproduct]
section_subFinType [in jordanholder]
section_finType [in jordanholder]
section_subCountType [in jordanholder]
section_countType [in jordanholder]
section_choiceType [in jordanholder]
section_eqType [in jordanholder]
section_subType [in jordanholder]
section_group [in jordanholder]
section_finMixin [in jordanholder]
section_repr [in mxrepresentation]
section_eqMixin [in jordanholder]
section_repr [in jordanholder]
section_choiceMixin [in jordanholder]
section_countMixin [in jordanholder]
section_isog [in jordanholder]
self_inverse [in ssrfun]
semidihedral_gtype [in extremal]
semidirect_product [in gproduct]
semiprime [in frobenius]
semiregular [in frobenius]
seqn [in seq]
seqn_type [in seq]
seqn_rec [in seq]
seq_countMixin [in choice]
seq_sub_countMixin [in fintype]
seq_sub_pickle [in fintype]
seq_sub_subFinType [in fintype]
seq_sub_finType [in fintype]
seq_sub_subCountType [in fintype]
seq_sub_countType [in fintype]
seq_sub_choiceType [in fintype]
seq_sub_eqType [in fintype]
seq_sub_subType [in fintype]
seq_sub_finMixin [in fintype]
seq_sub_unpickle [in fintype]
seq_sub_enum [in fintype]
seq_sub_choiceMixin [in fintype]
seq_countType [in choice]
seq_choiceType [in choice]
seq_sub_eqMixin [in fintype]
seq_predType [in seq]
seq_eqType [in seq]
seq_eqMixin [in seq]
seq_of_tag_count [in choice]
seq_choiceMixin [in choice]
seq_of_opt [in choice]
seq2_of [in choice]
series_repr [in mxrepresentation]
setact [in action]
setC [in finset]
setD [in finset]
SetDef.finset [in finset]
SetDef.pred_of_set [in finset]
setI [in finset]
setIgr [in gseries]
setI_group [in fingroup]
setI_addoid [in finset]
setI_muloid [in finset]
setI_comoid [in finset]
setI_monoid [in finset]
setTfor [in finset]
setT_group [in fingroup]
setU [in finset]
setU_addoid [in finset]
setU_muloid [in finset]
setU_comoid [in finset]
setU_monoid [in finset]
setX [in finset]
setX_group [in gproduct]
set_of_subFinType [in finset]
set_of_finType [in finset]
set_of_subCountType [in finset]
set_of_countType [in finset]
set_of_choiceType [in finset]
set_of_eqType [in finset]
set_of_subType [in finset]
set_predType [in finset]
set_subFinType [in finset]
set_finType [in finset]
set_subCountType [in finset]
set_countType [in finset]
set_choiceType [in finset]
set_eqType [in finset]
set_subType [in finset]
set_invg [in fingroup]
set_nth [in seq]
set_choiceMixin [in finset]
set_finMixin [in finset]
set_action [in action]
set_countMixin [in finset]
set_mulg [in fingroup]
set_eqMixin [in finset]
set_of [in finset]
set0 [in finset]
set1 [in finset]
set1_group [in fingroup]
sfT [in fintype]
sgval [in fingroup]
sgval_morphism [in morphism]
sgzZG [in center]
sgzZZ [in center]
sG_f'fG [in mxrepresentation]
sG_f'fG [in mxrepresentation]
shape [in seq]
sHD [in action]
sHG [in mxrepresentation]
sHG [in quotient]
sHG [in finmodule]
shorten [in path]
sign_morph [in alt]
sig_subFinType [in fintype]
sig_finType [in fintype]
sig_finMixin [in fintype]
sig_choiceMixin [in choice]
sig_eqType [in eqtype]
sig_subType [in eqtype]
sig_eqMixin [in eqtype]
sig_subCountType [in choice]
sig_countType [in choice]
sig_choiceType [in choice]
sig_countMixin [in choice]
simple [in gseries]
SimplFunDelta [in ssrfun]
SimplPred [in ssrbool]
simplPredType [in ssrbool]
SimplRel [in ssrbool]
simpl_pred [in ssrbool]
simpl_rel [in ssrbool]
size [in seq]
size_loop [in vector]
size_diagA [in mxpoly]
snd_morphism [in gproduct]
Socle [in mxrepresentation]
socle_repr [in mxrepresentation]
socle_eqMixin [in mxrepresentation]
socle_base [in mxrepresentation]
socle_subFinType [in mxrepresentation]
socle_finType [in mxrepresentation]
socle_subCountType [in mxrepresentation]
socle_countType [in mxrepresentation]
socle_choiceType [in mxrepresentation]
socle_eqType [in mxrepresentation]
socle_subType [in mxrepresentation]
socle_val [in mxrepresentation]
socle_mult [in mxrepresentation]
socle_choiceMixin [in mxrepresentation]
socle_module [in mxrepresentation]
socle_finMixin [in mxrepresentation]
socle_countMixin [in mxrepresentation]
socle_enum [in mxrepresentation]
solG' [in hall]
solvable [in nilpotent]
sort [in path]
sorted [in path]
sort_of_simpl_pred [in ssrbool]
span [in vector]
span_mx [in vector]
special [in maximal]
split [in fintype]
splits_over [in gproduct]
split_diagA [in mxpoly]
ssetI [in finset]
ssGD [in action]
ssr_wlog [in ssreflect]
ssr_suff [in ssreflect]
ssr_have [in ssreflect]
stable_factor [in gseries]
subact [in action]
subaction [in action]
subact_dom [in action]
subact_dom_group [in action]
subBaseFinGroupType [in fingroup]
SubEqMixin [in eqtype]
subFinGroupMixin [in fingroup]
subFinGroupType [in fingroup]
SubFinMixin [in fintype]
SubFinMixin_for [in fintype]
subFinType_finType [in fintype]
subFinType_subCountType [in fintype]
subFin_mixin [in fintype]
subg [in fingroup]
subgroups [in fingroup]
subg_one [in fingroup]
subg_inv [in fingroup]
subg_subFinType [in fingroup]
subg_finType [in fingroup]
subg_subCountType [in fingroup]
subg_countType [in fingroup]
subg_choiceType [in fingroup]
subg_eqType [in fingroup]
subg_subType [in fingroup]
subg_morphism [in morphism]
subg_countMixin [in fingroup]
subg_mul [in fingroup]
subg_choiceMixin [in fingroup]
subg_eqMixin [in fingroup]
subg_finMixin [in fingroup]
subg_repr [in mxrepresentation]
submod_mx [in mxrepresentation]
submod_repr [in mxrepresentation]
submx [in mxalgebra]
submx_def [in mxalgebra]
subn [in ssrnat]
subnormal [in gseries]
subn_rec [in ssrnat]
subpred [in ssrbool]
subrel [in ssrbool]
subseq [in seq]
subseries_repr [in mxrepresentation]
SubsetDef.subset [in fintype]
SubsetDef.subsetEdef [in fintype]
subsetv [in vector]
subset_unlock [in fintype]
subvect_add [in vector]
subvect_lmodMixin [in vector]
subvect_zero [in vector]
subvect_choiceMixin [in vector]
subvect_opp [in vector]
subvect_eqMixin [in vector]
subvect_zmodMixin [in vector]
subvect_scale [in vector]
subvect_VectMixin [in vector]
subvect_v2rv [in vector]
subvect_vectType [in vector]
subvect_linear [in vector]
subvect_lmodType [in vector]
subvect_zmodType [in vector]
subvect_choiceType [in vector]
subvect_eqType [in vector]
subvect_subType [in vector]
sub_ord [in fintype]
sub_qidmx [in mxalgebra]
sub_enum [in fintype]
sub_mem [in ssrbool]
sub_choiceMixin [in choice]
sub_eqType [in eqtype]
sub_setIgr [in gseries]
sub_countType [in choice]
sub_choiceType [in choice]
sub_eqMixin [in eqtype]
sub_countMixin [in choice]
sub_choiceClass [in choice]
sumn [in seq]
sums_R [in mxrepresentation]
sumv_pi [in vector]
sum_eq [in eqtype]
sum_finType [in fintype]
sum_finMixin [in fintype]
sum_choiceMixin [in choice]
sum_enum [in fintype]
sum_eqType [in eqtype]
sum_eqMixin [in eqtype]
sum_countType [in choice]
sum_choiceType [in choice]
sum_countMixin [in choice]
sum_mxsum [in mxalgebra]
sum_addv [in vector]
support [in finfun]
sv_val [in vector]
swizzle_mx [in matrix]
swizzle_mx_scalable [in matrix]
swizzle_mx_additive [in matrix]
Syl [in pgroup]
Sylow [in pgroup]
Sylvester_mx [in mxpoly]
Sym [in alt]
symmetric [in ssrbool]
Sym_group [in alt]
sZA [in maximal]
sZH [in center]
sZK [in center]
sZS [in mxabelem]
s2val [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)