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

sameP [in ssrbool]
same_fconnect1 [in fingraph]
same_connect_rev [in fingraph]
same_connect_r [in fingraph]
same_fconnect_finv [in fingraph]
same_fconnect1_r [in fingraph]
same_cover_at [in finset]
same_connect [in fingraph]
scalar_mx_cent [in mxalgebra]
scalar_mx_comm [in matrix]
scalar_mx_is_multiplicative [in matrix]
scalar_mxC [in matrix]
scalar_mx_is_additive [in matrix]
scalar_mx_sum_delta [in matrix]
scalar_mx_block [in matrix]
scalar_mxM [in matrix]
scalar_mx_hom [in mxrepresentation]
scalar_mx_is_scalar [in matrix]
scalemxA [in matrix]
scalemxAl [in matrix]
scalemxAr [in matrix]
scalemx_sub [in mxalgebra]
scalemx_addr [in matrix]
scalemx_addl [in matrix]
scalemx_const [in matrix]
scalemx1 [in matrix]
scaler_eq0 [in poly]
scale_lapp_Ar [in vector]
scale_poly_addr [in poly]
scale_polyE [in poly]
scale_actE [in mxabelem]
scale_col_mx [in matrix]
scale_1poly [in poly]
scale_is_action [in mxabelem]
scale_scalar_mx [in matrix]
scale_lapp_Al [in vector]
scale_polyA [in poly]
scale_block_mx [in matrix]
scale_poly1 [in poly]
scale_lappE [in vector]
scale_is_groupAction [in mxabelem]
scale_row_mx [in matrix]
scale_poly_addl [in poly]
scale_poly_mull [in poly]
scale1mx [in matrix]
scalp_map [in poly]
scalp_Ineq0 [in poly]
scanlK [in seq]
scanl_tupleP [in tuple]
scanl_cat [in seq]
SchurZassenhaus_trans_actsol [in hall]
SchurZassenhaus_trans_sol [in hall]
SchurZassenhaus_split [in hall]
SCN_P [in maximal]
SCN_max [in maximal]
SCN_abelian [in maximal]
sdpairE [in gproduct]
sdpair_act [in gproduct]
sdpair_setact [in gproduct]
sdpair1_morphM [in gproduct]
sdpair2_morphM [in gproduct]
sdprodE [in gproduct]
sdprodEY [in gproduct]
sdprodg1 [in gproduct]
sdprodmE [in gproduct]
sdprodmEl [in gproduct]
sdprodmEr [in gproduct]
sdprodm_norm [in gproduct]
sdprodm_eqf [in gproduct]
sdprodm_sub [in gproduct]
sdprodP [in gproduct]
sdprod_recr [in gproduct]
sdprod_compl [in gproduct]
sdprod_mul_proof [in gproduct]
sdprod_inv_proof [in gproduct]
sdprod_card [in gproduct]
sdprod_normal_complP [in gproduct]
sdprod_Hall_p'coreP [in pgroup]
sdprod_normal_p'HallP [in pgroup]
sdprod_sdpair [in gproduct]
sdprod_modl [in gproduct]
sdprod_Hall_pcoreP [in pgroup]
sdprod_mulVg [in gproduct]
sdprod_mul1g [in gproduct]
sdprod_Hall [in pgroup]
sdprod_context [in gproduct]
sdprod_modr [in gproduct]
sdprod_recl [in gproduct]
sdprod_pcore_HallP [in pgroup]
sdprod_normal_pHallP [in pgroup]
sdprod_mulgA [in gproduct]
sdprod_p'core_HallP [in pgroup]
sdprod1g [in gproduct]
second_isog [in quotient]
second_isom [in quotient]
section_reprP [in jordanholder]
section_repr_isog [in jordanholder]
section_module [in mxrepresentation]
section_eqmx_add [in mxrepresentation]
section_eqmx [in mxrepresentation]
semidihedral_structure [in extremal]
semidihedral_classP [in extremal]
semiprime_regular [in frobenius]
semiregular_sym [in frobenius]
semiregular_prime [in frobenius]
semiregular1l [in frobenius]
semiregular1r [in frobenius]
semisimple_Socle [in mxrepresentation]
seq_of_tag_countK [in choice]
seq_polyXn [in poly]
seq_poly0 [in poly]
seq_of_optK [in choice]
seq_factor [in poly]
seq_mul_polyX [in poly]
seq_sub_pickleK [in fintype]
seq2_ofK [in choice]
series_sol [in nilpotent]
setactE [in action]
setactJ [in action]
setactVin [in action]
setact_orbit [in action]
setact_is_action [in action]
setCD [in finset]
setCI [in finset]
setCK [in finset]
setCP [in finset]
setCS [in finset]
setCT [in finset]
setCU [in finset]
setC_inj [in finset]
setC_bigcup [in finset]
setC_bigcap [in finset]
setC0 [in finset]
setC11 [in finset]
setDDl [in finset]
setDDr [in finset]
setDE [in finset]
SetDef.finsetE [in finset]
SetDef.pred_of_setE [in finset]
setDidPl [in finset]
setDIl [in finset]
setDIr [in finset]
setDP [in finset]
setDS [in finset]
setDSS [in finset]
setDT [in finset]
setDUl [in finset]
setDUr [in finset]
setDv [in finset]
setD_eq0 [in finset]
setD0 [in finset]
setD1K [in finset]
setD1P [in finset]
setD11 [in finset]
setIA [in finset]
setIAC [in finset]
setIC [in finset]
setICA [in finset]
setICr [in finset]
setID [in finset]
setIdE [in finset]
setIdP [in finset]
setIg1 [in fingroup]
setIid [in finset]
setIidPl [in finset]
setIidPr [in finset]
setIIl [in finset]
setIIr [in finset]
setIK [in finset]
setIP [in finset]
setIS [in finset]
setISS [in finset]
setIT [in finset]
setIUl [in finset]
setIUr [in finset]
setI_eq0 [in finset]
setI_normal_Hall [in pgroup]
setI_im_cpair [in center]
setI_subnormal [in gseries]
setI0 [in finset]
setI1g [in fingroup]
setKI [in finset]
setKU [in finset]
setP [in finset]
setSD [in finset]
setSI [in finset]
setSU [in finset]
setTD [in finset]
setTI [in finset]
setTU [in finset]
setUA [in finset]
setUAC [in finset]
setUC [in finset]
setUCA [in finset]
setUCr [in finset]
setUid [in finset]
setUidPl [in finset]
setUidPr [in finset]
setUIl [in finset]
setUIr [in finset]
setUK [in finset]
setUP [in finset]
setUS [in finset]
setUSS [in finset]
setUT [in finset]
setUUl [in finset]
setUUr [in finset]
setU_eq0 [in finset]
setU0 [in finset]
setU1K [in finset]
setU1P [in finset]
setU1r [in finset]
setU11 [in finset]
setXP [in finset]
setXS [in finset]
setX_gen [in gproduct]
setX_dprod [in gproduct]
setX_prod [in gproduct]
set_invgK [in fingroup]
set_partition_big [in finset]
set_mulgA [in fingroup]
set_set_nth [in seq]
set_0Vmem [in finset]
set_nth_nil [in seq]
set_nth_default [in seq]
set_invgM [in fingroup]
set_cons [in finset]
set_mul1g [in fingroup]
set0D [in finset]
set0I [in finset]
set0Pn [in finset]
set0U [in finset]
set1gE [in fingroup]
set1gP [in fingroup]
set1P [in finset]
set1Ul [in finset]
set1Ur [in finset]
set1_inj [in finset]
set11 [in finset]
set2P [in finset]
set21 [in finset]
set22 [in finset]
sgvalK [in fingroup]
sgvalM [in fingroup]
sgvalmK [in morphism]
sgval_sub [in morphism]
shortenP [in path]
sigW [in choice]
sig2W [in choice]
simpleP [in gseries]
simple_Socle [in mxrepresentation]
simple_sol_prime [in maximal]
simple_Alt_3 [in alt]
simple_maxnormal [in gseries]
simple_Alt5 [in alt]
simple_compsP [in jordanholder]
simple_Alt5_base [in alt]
simpl_predE [in ssrbool]
size_pairmap [in seq]
size_nseq [in seq]
size_ncons [in seq]
size_subseq [in seq]
size_eqp [in poly]
size_poly [in poly]
size_flatten [in seq]
size_scanl [in seq]
size_cat [in seq]
size_abelian_type [in abelian]
size_scaler [in poly]
size_sum [in poly]
size_polyC [in poly]
size_map_poly [in poly]
size_mkseq [in seq]
size_Xn_sub_1 [in poly]
size_is_basis [in vector]
size_add [in poly]
size_char_poly [in mxpoly]
size_zip [in seq]
size_amulX [in poly]
size_allpairs [in seq]
size_belast [in seq]
size_incr_nth [in seq]
size_mod_mxminpoly [in mxpoly]
size_poly_cons [in poly]
size_mxminpoly [in mxpoly]
size_poly1 [in poly]
size_poly_eq [in poly]
size_subseq_leqif [in seq]
size_mul_monic [in poly]
size_Poly [in poly]
size_pmap [in seq]
size_monic_mul [in poly]
size_takel [in seq]
size_drop [in seq]
size_mul_id [in poly]
size_rev [in seq]
size_sign_mul [in poly]
size_poly0 [in poly]
size_dvdp [in poly]
size_poly_eq0 [in poly]
size_sort [in path]
size_mask [in seq]
size_opp [in poly]
size_take [in seq]
size_basis [in vector]
size_exp [in poly]
size_dvdMp_leqif [in poly]
size_polyX [in poly]
size_eq0 [in seq]
size_set_nth [in seq]
size_prod_factors [in poly]
size_enum_ord [in fintype]
size_rotr [in seq]
size_merge [in path]
size_mul [in poly]
size_proper_mul [in poly]
size_undup [in seq]
size_map [in seq]
size_orbit [in fingraph]
size_traject [in path]
size_exp_id [in poly]
size_rot [in seq]
size_tuple [in tuple]
size_rcons [in seq]
size_behead [in seq]
size_polyC_mul [in poly]
size_polyXn [in poly]
size_addl [in poly]
size_pmap_sub [in seq]
size_iota [in seq]
size0nil [in seq]
size1_polyC [in poly]
size1_zip [in seq]
size2_zip [in seq]
small_nil_class [in sylow]
snd_morphM [in gproduct]
socleP [in mxrepresentation]
socle_finType_subproof [in mxrepresentation]
socle_mem [in mxrepresentation]
socle_exists [in mxrepresentation]
socle_irr [in mxrepresentation]
socle_rsimP [in mxrepresentation]
socle_simple [in mxrepresentation]
Socle_module [in mxrepresentation]
Socle_semisimple [in mxrepresentation]
Socle_direct [in mxrepresentation]
Socle_iso [in mxrepresentation]
solvableS [in nilpotent]
solvable_norm_abelem [in maximal]
solvable1 [in nilpotent]
sol_coprime_Sylow_trans [in hall]
sol_coprime_Sylow_exists [in hall]
sol_der1_proper [in nilpotent]
sol_prime_factor_exists [in maximal]
sol_coprime_Sylow_subset [in hall]
sorted_sort [in path]
sorted_divisors_ltn [in prime]
sorted_divisors [in prime]
sorted_rev [in path]
sorted_ltn_iota [in path]
sorted_ltn_uniq_leq [in path]
sorted_primes [in prime]
sorted_filter [in path]
sorted_uniq [in path]
sorted_merge [in path]
sorted_iota [in path]
sort_uniq [in path]
span_seq1 [in vector]
span_nil [in vector]
span_cons [in vector]
span_subsetl [in vector]
span_mx_row [in vector]
span_bigcat [in vector]
span_cat [in vector]
span_mulmx [in vector]
span_subset [in vector]
span_eq [in vector]
span_vs2mx [in vector]
splitK [in fintype]
splitP [in fintype]
splitP [in path]
splitPl [in path]
splitPr [in path]
splitP2r [in path]
splitsP [in gproduct]
splitting_cyclic_primitive_root [in mxrepresentation]
split_subproof [in fintype]
split1 [in zmodp]
split1_extraspecial [in maximal]
sqrn_inj [in ssrnat]
sqrn_sub [in ssrnat]
sqrn_distn [in ssrnat]
sqrn_add_sub [in ssrnat]
sqrn_add [in ssrnat]
sqrn_gt0 [in ssrnat]
ssr_congr_arrow [in ssreflect]
stable_rowg_mxK [in mxabelem]
stab_ntransitive [in primitive_action]
stab_semiprime [in frobenius]
stab_ntransitiveI [in primitive_action]
strict_adjunction [in fingraph]
strongest_coprime_quotient_cent [in hall]
StrongJordanHolderUniqueness [in jordanholder]
subact_is_action [in action]
subcentP [in center]
subcent_dprod [in gproduct]
subcent_sub [in center]
subcent_TImulg [in gproduct]
subcent_char [in center]
subcent_sdprod [in gproduct]
subcent_norm [in center]
subcent_normal [in center]
subcent1C [in center]
subcent1P [in center]
subcent1_cycle_norm [in center]
subcent1_extraspecial_maximal [in maximal]
subcent1_cycle_normal [in center]
subcent1_cycle_sub [in center]
subcent1_id [in center]
subcent1_sub [in center]
subCset [in finset]
subDset [in finset]
subD1set [in finset]
subEproper [in finset]
subgacentE [in action]
subgacent1E [in action]
subgK [in fingroup]
subgM [in fingroup]
subgmK [in morphism]
subgP [in fingroup]
subgroup_transitiveP [in action]
subgroup_transitivePin [in action]
subg_mx_repr [in mxrepresentation]
subg_mx_faithful [in mxrepresentation]
subg_invP [in fingroup]
subg_mulP [in fingroup]
subg_default [in fingroup]
subg_oneP [in fingroup]
subg_mx_abs_irr [in mxrepresentation]
subg_inj [in fingroup]
subg_mx_irr [in mxrepresentation]
subG1 [in fingroup]
subG1_contra [in fingroup]
subHall_Sylow [in pgroup]
subHall_Hall [in pgroup]
subIset [in finset]
SubK [in eqtype]
subKn [in ssrnat]
submod_mx_repr [in mxrepresentation]
submod_mx_faithful [in mxrepresentation]
submod_mx_irr [in mxrepresentation]
submxE [in mxalgebra]
submxElt [in mxalgebra]
submxK [in matrix]
submxMfree [in mxalgebra]
submxMl [in mxalgebra]
submxMr [in mxalgebra]
submxP [in mxalgebra]
submx_trans [in mxalgebra]
submx_full [in mxalgebra]
submx_key [in mxalgebra]
submx_refl [in mxalgebra]
submx0 [in mxalgebra]
submx0null [in mxalgebra]
submx1 [in mxalgebra]
subnAC [in ssrnat]
subnE [in ssrnat]
subnK [in ssrnat]
subnKC [in ssrnat]
subnn [in ssrnat]
subnormalEl [in gseries]
subnormalEr [in gseries]
subnormalEsupport [in gseries]
subnormalP [in gseries]
subnormal_trans [in gseries]
subnormal_sub [in gseries]
subnormal_refl [in gseries]
subn_add2l [in ssrnat]
subn_if_gt [in ssrnat]
subn_sub [in ssrnat]
subn_exp [in binomial]
subn_gt0 [in ssrnat]
subn_add2r [in ssrnat]
subn_sqr [in ssrnat]
subn_subA [in ssrnat]
subn_eq0 [in ssrnat]
subn0 [in ssrnat]
subn1 [in ssrnat]
subn2 [in ssrnat]
subon_bij [in ssrbool]
subon1 [in ssrbool]
subon1l [in ssrbool]
subon2 [in ssrbool]
SubP [in eqtype]
subrelUl [in ssrbool]
subrelUr [in ssrbool]
subseqP [in seq]
subseq_refl [in seq]
subseq_rcons [in seq]
subseq_cat [in seq]
subseq_order_path [in path]
subseq_cons [in seq]
subseq_seq1 [in seq]
subseq_trans [in seq]
subseq_sorted [in path]
subseq_uniq [in seq]
subseq0 [in seq]
subsetC [in finset]
subsetD [in finset]
subsetDl [in finset]
subsetDP [in finset]
subsetDr [in finset]
subsetD1 [in finset]
subsetD1P [in finset]
subsetE [in fintype]
subsetI [in finset]
subsetIidl [in finset]
subsetIidr [in finset]
subsetIl [in finset]
subsetIP [in finset]
subsetIr [in finset]
subsetP [in fintype]
subsetPn [in fintype]
subsets_disjoint [in finset]
subsetT [in finset]
subsetU [in finset]
subsetUl [in finset]
subsetUr [in finset]
subsetU1 [in finset]
subset_closure [in fingraph]
subset_cardP [in fintype]
subset_gen [in fingroup]
subset_dfs [in fingraph]
subset_predT [in fintype]
subset_all [in fintype]
subset_pred1 [in fintype]
subset_faithful [in action]
subset_trans [in fintype]
subset_disjoint [in fintype]
subset_eqP [in fintype]
subset_leqif_cards [in finset]
subset_leq_card [in fintype]
subset_leqif_card [in fintype]
subset0 [in finset]
subset1 [in finset]
subSnn [in ssrnat]
subSocle_module [in mxrepresentation]
subSocle_semisimple [in mxrepresentation]
subSocle_iso [in mxrepresentation]
subSocle_direct [in mxrepresentation]
subSS [in ssrnat]
subTset [in finset]
subUset [in finset]
subUsetP [in finset]
subvectP [in vector]
subvect_scale_addl [in vector]
subvect_inj [in vector]
subvect_add0 [in vector]
subvect_addA [in vector]
subvect_addC [in vector]
subvect_addN [in vector]
subvect_is_linear [in vector]
subvect_scaleA [in vector]
subvect_scale1 [in vector]
subvect_bij [in vector]
subvect_scale_addr [in vector]
subvf [in vector]
subvP [in vector]
subv_refl [in vector]
subv_anti [in vector]
subv_sumP [in vector]
subv_bigcapP [in vector]
subv_cap [in vector]
subv_trans [in vector]
subv_diffv0 [in vector]
subv_add [in vector]
subv0 [in vector]
subxx [in fintype]
subxx_hint [in fintype]
sub_isom [in morphism]
sub_cosetpre_quo [in quotient]
sub_normal_Hall [in pgroup]
sub_der1_norm [in commutator]
sub_in3 [in ssrbool]
sub_in21 [in ssrbool]
sub_in_bij [in ssrbool]
sub_der1_abelian [in commutator]
sub_quotient_pre [in quotient]
sub_in11 [in ssrbool]
sub_class_support [in fingroup]
sub_in2 [in ssrbool]
sub_abelem_rV_im [in mxabelem]
sub_center_normal [in center]
sub_in1 [in ssrbool]
sub_act_proof [in action]
sub_astabQ [in action]
sub_astab1 [in action]
sub_capmx [in mxalgebra]
sub_lcoset [in fingroup]
sub_morphim_pre [in morphism]
sub_cyclic_char [in cyclic]
sub_rcosetV [in fingroup]
sub_pcore [in pgroup]
sub_capmx_gen [in mxalgebra]
sub_im_coset [in quotient]
sub_in_pnat [in prime]
sub_morphpre_injm [in morphism]
sub_in111 [in ssrbool]
sub_proper_trans [in fintype]
sub_cosetpre [in quotient]
sub_rcoset [in fingroup]
sub_Hall_pcore [in pgroup]
sub_afixRs_norm [in action]
sub_im_abelem_rV [in mxabelem]
sub_astab1_in [in action]
sub_ordK [in fintype]
sub_lcosetV [in fingroup]
sub_sumsmxP [in mxalgebra]
sub_bigcapmxP [in mxalgebra]
sub_morphpre_im [in morphism]
sub_abelian_normal [in fingroup]
sub_in_constt [in pgroup]
sub_abelian_cent [in fingroup]
sub_in_pcore [in pgroup]
sub_rVP [in mxalgebra]
sub_isog [in morphism]
sub_conjg [in fingroup]
sub_rowg_mx [in mxabelem]
sub_afixRs_norms [in action]
sub_Ldiv [in abelian]
sub_abelian_cent2 [in fingroup]
sub_rVabelem [in mxabelem]
sub_pnat_coprime [in prime]
sub_abelian_norm [in fingroup]
sub_gen [in fingroup]
sub_addsmxP [in mxalgebra]
sub_nilpotent_cent2 [in sylow]
sub_in_partn [in prime]
sub_enum_uniq [in fintype]
sub_ltmx_trans [in mxalgebra]
sub_path [in path]
sub_in12 [in ssrbool]
sub_p_elt [in pgroup]
sub_pgroup [in pgroup]
sub_pHall [in pgroup]
sub_sub_minn [in ssrnat]
sub_daddsmx [in mxalgebra]
sub_conjgV [in fingroup]
sub_astabQR [in action]
sub_ord_proof [in fintype]
sub_rVabelem_im [in mxabelem]
sub_dsumsmx [in mxalgebra]
sub_der1_normal [in commutator]
sub_kermxP [in mxalgebra]
sub_cent1 [in fingroup]
sub_LdivT [in abelian]
sub_imset_pre [in finset]
sub0mx [in mxalgebra]
sub0n [in ssrnat]
sub0seq [in seq]
sub0set [in finset]
sub0v [in vector]
sub1b [in ssrnat]
sub1G [in fingroup]
sub1mx [in mxalgebra]
sub1set [in finset]
succnK [in ssrnat]
succn_inj [in ssrnat]
sumfv [in vector]
summxE [in matrix]
summx_sub_sums [in mxalgebra]
summx_sub [in mxalgebra]
sumn_nseq [in seq]
sumn_cat [in seq]
sumsmxMr [in mxalgebra]
sumsmxMr_gen [in mxalgebra]
sumsmxS [in mxalgebra]
sumsmx_subP [in mxalgebra]
sumsmx_module [in mxrepresentation]
sumsmx_semisimple [in mxrepresentation]
sumsmx_sup [in mxalgebra]
sumv_sum_pi [in vector]
sumv_sup [in vector]
sum_nat_dep_const [in finset]
sum_lappE [in vector]
sum_nat_const_nat [in bigop]
sum_phi_dvd [in cyclic]
sum_card_class [in action]
sum_irr_degree [in mxrepresentation]
sum_card_rcosets_pcycles [in finmodule]
sum_enum_uniq [in fintype]
sum_mxsimple_direct_compl [in mxrepresentation]
sum_nat_eq0 [in bigop]
sum_ncycle_phi [in cyclic]
sum_nat_const [in bigop]
sum_ffunE [in ssralg]
sum_eqE [in eqtype]
sum_mxsimple_direct_sub [in mxrepresentation]
sum_eqP [in eqtype]
sum0v [in vector]
sum1dep_card [in finset]
sum1_card [in bigop]
svalP [in eqtype]
swizzle_mx_is_additive [in matrix]
swizzle_mx_is_scalable [in matrix]
SylowJ [in pgroup]
SylowP [in pgroup]
Sylow_Jsub [in sylow]
Sylow_superset [in sylow]
Sylow_gen [in sylow]
Sylow_subJ [in sylow]
Sylow_transversal_gen [in sylow]
Sylow_subnorm [in sylow]
Sylow_setI_normal [in sylow]
Sylow_trans [in sylow]
Sylow_exists [in sylow]
Sylow's_theorem [in sylow]
Sylow1 [in pgroup]
Sylvester_mxE [in mxpoly]
Syl_trans [in sylow]
symmetric_from_pre [in ssrbool]
symplectic_type_group_structure [in extremal]
Sym_trans [in alt]
s2valP [in eqtype]
s2valP' [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)