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 _ (6599 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 _ (86 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 _ (57 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 _ (3455 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 _ (290 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 _ (147 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 _ (148 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 _ (53 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 _ (1466 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 _ (28 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 _ (53 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 _ (788 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 _ (28 entries)

S (lemma)

sameP [in ssrbool]
same_connect [in connect]
same_connect_r [in connect]
same_connect_rev [in connect]
same_cover_at [in finset]
same_fconnect1 [in connect]
same_fconnect1_r [in connect]
same_fconnect_finv [in connect]
scalar_mx0 [in matrix]
scalar_mx_add [in matrix]
scalar_mx_comm [in matrix]
scalar_mx_mul [in matrix]
scalar_mx_opp [in matrix]
scalemxA [in matrix]
scalemxAl [in matrix]
scalemxAr [in matrix]
scalemxN [in matrix]
scalemx0 [in matrix]
scalemx_add [in matrix]
scalemx_addl [in matrix]
scalemx_addr [in matrix]
scalemx_block [in matrix]
scalemx_paste [in matrix]
scalemx_subl [in matrix]
scalemx_subr [in matrix]
scaleNmx [in matrix]
scale0mx [in matrix]
scale1mx [in matrix]
scalp_id [in poly]
scalp_spec [in poly]
scanlK [in seq]
scanl_tupleP [in tuple]
second_isog [in normal]
second_isom [in normal]
seq2_ofK [in choice]
seq_factor [in poly]
seq_mul_polyX [in poly]
seq_of_optK [in choice]
seq_polyXn [in poly]
seq_poly0 [in poly]
seq_sub_pickleK [in fintype]
setCD [in finset]
setCI [in finset]
setCK [in finset]
setCP [in finset]
setCS [in finset]
setCT [in finset]
setCU [in finset]
setC0 [in finset]
setC11 [in finset]
setC_bigcap [in finset]
setC_bigcup [in finset]
setC_inj [in finset]
setDDl [in finset]
setDDr [in finset]
setDE [in finset]
SetDef.finsetE [in finset]
SetDef.pred_of_setE [in finset]
setDeq0 [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]
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]
setIdP [in finset]
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]
setI0 [in finset]
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]
setU0 [in finset]
setU1K [in finset]
setU1P [in finset]
setU1r [in finset]
setU11 [in finset]
setXP [in finset]
setXS [in finset]
set0D [in finset]
set0I [in finset]
set0Pn [in finset]
set0U [in finset]
set1gE [in groups]
set1gP [in groups]
set1P [in finset]
set1Ul [in finset]
set1Ur [in finset]
set11 [in finset]
set2P [in finset]
set21 [in finset]
set22 [in finset]
set_cons [in finset]
set_invgK [in groups]
set_invgM [in groups]
set_mulgA [in groups]
set_mul1g [in groups]
set_nth_default [in seq]
set_nth_nil [in seq]
set_partition_big [in finset]
set_set_nth [in seq]
set_0Vmem [in finset]
sgvalEdom [in morphisms]
sgvalK [in groups]
sgvalM [in groups]
sgvalmK [in morphisms]
sgval_sub [in morphisms]
shortenP [in paths]
sieve0 [in seq]
sieve1 [in seq]
sieve_cat [in seq]
sieve_cons [in seq]
sieve_false [in seq]
sieve_rot [in seq]
sieve_true [in seq]
sieve_uniq [in seq]
simpl_predE [in ssrbool]
size0nil [in seq]
size1_polyC [in poly]
size1_zip [in seq]
size2_zip [in seq]
size_add [in poly]
size_addl [in poly]
size_behead [in seq]
size_belast [in seq]
size_cat [in seq]
size_drop [in seq]
size_dvdp [in poly]
size_enum_ord [in fintype]
size_eqp [in poly]
size_eq0 [in seq]
size_exp [in poly]
size_flatten [in seq]
size_incr_nth [in seq]
size_iota [in seq]
size_map [in seq]
size_merge [in paths]
size_mkseq [in seq]
size_monic_mul [in poly]
size_mul [in poly]
size_mul_id [in poly]
size_mul_monic [in poly]
size_ncons [in seq]
size_nseq [in seq]
size_opp [in poly]
size_orbit [in connect]
size_pairmap [in seq]
size_pmap [in seq]
size_pmap_sub [in seq]
size_Poly [in poly]
size_poly [in poly]
size_polyC [in poly]
size_polyC_mul [in poly]
size_polyX [in poly]
size_polyXn [in poly]
size_poly0 [in poly]
size_poly1 [in poly]
size_poly_cons [in poly]
size_poly_eq [in poly]
size_poly_eq0 [in poly]
size_proper_mul [in poly]
size_rcons [in seq]
size_rev [in seq]
size_rot [in seq]
size_rotr [in seq]
size_scanl [in seq]
size_set_nth [in seq]
size_sieve [in seq]
size_sort [in paths]
size_sum [in poly]
size_take [in seq]
size_takel [in seq]
size_traject [in paths]
size_tuple [in tuple]
size_undup [in seq]
sorted_divisors [in prime]
sorted_divisors_ltn [in prime]
sorted_filter [in paths]
sorted_iota [in paths]
sorted_ltn_iota [in paths]
sorted_ltn_uniq_leq [in paths]
sorted_merge [in paths]
sorted_primes [in prime]
sorted_sort [in paths]
sorted_uniq [in paths]
sort_uniq [in paths]
splitK [in fintype]
splitP [in paths]
splitP [in fintype]
splitPl [in paths]
splitPr [in paths]
splitP2r [in paths]
split1 [in matrix]
split_subproof [in fintype]
sqrn_add [in ssrnat]
sqrn_add_sub [in ssrnat]
sqrn_gt0 [in ssrnat]
sqrn_inj [in ssrnat]
sqrn_sub [in ssrnat]
strict_adjunction [in connect]
subDset [in finset]
subEproper [in finset]
subgEdom [in morphisms]
subgK [in groups]
subgM [in groups]
subgmK [in morphisms]
subgP [in groups]
subG1 [in groups]
subg_default [in groups]
subg_inj [in groups]
subg_invP [in groups]
subg_mulP [in groups]
subg_oneP [in groups]
subIset [in finset]
SubK [in eqtype]
subKn [in ssrnat]
submxK [in matrix]
subnE [in ssrnat]
subnK [in ssrnat]
subnKC [in ssrnat]
subnn [in ssrnat]
subn0 [in ssrnat]
subn1 [in ssrnat]
subn_add2l [in ssrnat]
subn_add2r [in ssrnat]
subn_eq0 [in ssrnat]
subn_gt0 [in ssrnat]
subn_if_gt [in ssrnat]
subn_sqr [in ssrnat]
subn_sub [in ssrnat]
subn_subA [in ssrnat]
subon1 [in ssrbool]
subon1l [in ssrbool]
subon2 [in ssrbool]
subon_bij [in ssrbool]
SubP [in eqtype]
subrelUl [in ssrbool]
subrelUr [in ssrbool]
subsetD [in finset]
subsetDl [in finset]
subsetDr [in finset]
subsetD1 [in finset]
subsetE [in fintype]
subsetI [in finset]
subsetIl [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]
subset0 [in finset]
subset1 [in finset]
subset_all [in fintype]
subset_cardP [in fintype]
subset_closure [in connect]
subset_dfs [in connect]
subset_disjoint [in fintype]
subset_eqP [in fintype]
subset_gen [in groups]
subset_leqif_card [in fintype]
subset_leq_card [in fintype]
subset_predT [in fintype]
subset_pred1 [in fintype]
subset_trans [in fintype]
subSnn [in ssrnat]
subSS [in ssrnat]
subTset [in finset]
subUset [in finset]
subxx [in fintype]
subxx_hint [in fintype]
sub0n [in ssrnat]
sub0set [in finset]
sub1G [in groups]
sub1set [in finset]
sub_conjg [in groups]
sub_conjgV [in groups]
sub_cosetpre [in normal]
sub_cosetpre_quo [in normal]
sub_enum_uniq [in fintype]
sub_gen [in groups]
sub_in1 [in ssrbool]
sub_in11 [in ssrbool]
sub_in111 [in ssrbool]
sub_in12 [in ssrbool]
sub_in2 [in ssrbool]
sub_in21 [in ssrbool]
sub_in3 [in ssrbool]
sub_in_bij [in ssrbool]
sub_in_partn [in prime]
sub_in_pnat [in prime]
sub_isog [in morphisms]
sub_isom [in morphisms]
sub_morphim_pre [in morphisms]
sub_morphpre_im [in morphisms]
sub_morphpre_injm [in morphisms]
sub_ordK [in fintype]
sub_path [in paths]
sub_proper_trans [in fintype]
sub_quotient_pre [in normal]
sub_sub_minn [in ssrnat]
succnK [in ssrnat]
succn_inj [in ssrnat]
summxE [in matrix]
sumn_cat [in seq]
sumn_nseq [in seq]
sum1dep_card [in finset]
sum1_card [in bigops]
sum_enum_uniq [in fintype]
sum_eqE [in eqtype]
sum_eqP [in eqtype]
sum_nat_const [in bigops]
sum_nat_const_nat [in bigops]
sum_nat_dep_const [in finset]
sum_ncycle_phi [in cyclic]
sum_of_tagK [in choice]
sum_phi_dvd [in cyclic]
svalP [in eqtype]
symmetric_from_pre [in ssrbool]
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 _ (6599 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 _ (86 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 _ (57 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 _ (3455 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 _ (290 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 _ (147 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 _ (148 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 _ (53 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 _ (1466 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 _ (28 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 _ (53 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 _ (788 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 _ (28 entries)