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 _ (5434 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 _ (89 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 _ (58 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 _ (2752 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 _ (233 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 _ (145 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 _ (139 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 _ (50 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 _ (1267 entries)
Moduleid 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 _ (47 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 _ (24 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 _ (609 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 _ (21 entries)

L (lemma)

lastI [in seq]
lastP [in seq]
last_cat [in seq]
last_cons [in seq]
last_ind [in seq]
last_map [in seq]
last_nth [in seq]
last_rcons [in seq]
last_traject [in paths]
lcmnA [in div]
lcmnC [in div]
lcmn0 [in div]
lcmn1 [in div]
lcmn_gt0 [in div]
lcm0n [in div]
lcm1n [in div]
lead_coefC [in poly]
lead_coefE [in poly]
lead_coefTP [in closedfields]
lead_coefT_qf [in closedfields]
lead_coefX [in poly]
lead_coefXn [in poly]
lead_coef0 [in poly]
lead_coef1 [in poly]
lead_coef_addl [in poly]
lead_coef_eq0 [in poly]
lead_coef_map [in poly]
lead_coef_map_eq [in poly]
lead_coef_monic_mul [in poly]
lead_coef_mulX [in poly]
lead_coef_mul_id [in poly]
lead_coef_mul_monic [in poly]
lead_coef_opp [in poly]
lead_coef_poly [in poly]
lead_coef_proper_mul [in poly]
left_arc [in paths]
leP [in ssrnat]
leqifP [in ssrnat]
leqif_add [in ssrnat]
leqif_eq [in ssrnat]
leqif_geq [in ssrnat]
leqif_mul [in ssrnat]
leqif_refl [in ssrnat]
leqif_trans [in ssrnat]
leqNgt [in ssrnat]
leqnn [in ssrnat]
leqnSn [in ssrnat]
leqn0 [in ssrnat]
leqn1 [in polydiv]
leqn2 [in polydiv]
leqP [in ssrnat]
leqSpred [in ssrnat]
leqW [in ssrnat]
leq0n [in ssrnat]
leq_add [in ssrnat]
leq_addl [in ssrnat]
leq_addr [in ssrnat]
leq_add2l [in ssrnat]
leq_add2r [in ssrnat]
leq_bigmax [in bigops]
leq_bigmax_cond [in bigops]
leq_bump [in fintype]
leq_bump2 [in fintype]
leq_b1 [in ssrnat]
leq_card_cover [in finset]
leq_card_setU [in finset]
leq_coef_size [in poly]
leq_div [in div]
leq_divl [in div]
leq_divr [in div]
leq_double [in ssrnat]
leq_eqVlt [in ssrnat]
leq_exp2l [in ssrnat]
leq_exp2r [in ssrnat]
leq_floor [in div]
leq_image_card [in fintype]
leq_imset_card [in finset]
leq_ltn_trans [in ssrnat]
leq_maxl [in ssrnat]
leq_maxr [in ssrnat]
leq_minl [in ssrnat]
leq_minr [in ssrnat]
leq_mod [in div]
leq_mul [in ssrnat]
leq_mul2l [in ssrnat]
leq_mul2r [in ssrnat]
leq_ord [in fintype]
leq_pexp2l [in ssrnat]
leq_pmull [in ssrnat]
leq_pmulr [in ssrnat]
leq_pmul2l [in ssrnat]
leq_pmul2r [in ssrnat]
leq_pred [in ssrnat]
leq_Sdouble [in ssrnat]
leq_size_coef [in poly]
leq_size_perm [in seq]
leq_size_uniq [in seq]
leq_sqr [in ssrnat]
leq_subr [in ssrnat]
leq_subS [in ssrnat]
leq_sub2 [in ssrnat]
leq_sub2l [in ssrnat]
leq_sub2r [in ssrnat]
leq_sub_add [in ssrnat]
leq_total [in ssrnat]
leq_trans [in ssrnat]
le_irrelevance [in ssrnat]
liftK [in fintype]
lift_inj [in fintype]
lift_subproof [in fintype]
lock [in ssreflect]
lognE [in prime]
logn0 [in prime]
logn1 [in prime]
logn_div [in prime]
logn_exp [in prime]
logn_gauss [in prime]
logn_gt0 [in prime]
logn_mul [in prime]
logn_part [in prime]
logn_prime [in prime]
loopingP [in paths]
looping_order [in connect]
looping_uniq [in paths]
lshift_subproof [in fintype]
ltngtP [in ssrnat]
ltnn [in ssrnat]
ltnNge [in ssrnat]
ltnP [in ssrnat]
ltnS [in ssrnat]
ltnSn [in ssrnat]
ltnW [in ssrnat]
ltn0 [in ssrnat]
ltn0Sn [in ssrnat]
ltn_addl [in ssrnat]
ltn_addr [in ssrnat]
ltn_add2l [in ssrnat]
ltn_add2r [in ssrnat]
ltn_add_sub [in ssrnat]
ltn_ceil [in div]
ltn_divl [in div]
ltn_divr [in div]
ltn_double [in ssrnat]
ltn_expl [in ssrnat]
ltn_exp2l [in ssrnat]
ltn_exp2r [in ssrnat]
ltn_log0 [in prime]
ltn_mod [in div]
ltn_mul [in ssrnat]
ltn_mul2l [in ssrnat]
ltn_mul2r [in ssrnat]
ltn_neqAle [in ssrnat]
ltn_ord [in fintype]
ltn_Pdiv [in div]
ltn_pdiv2_prime [in prime]
ltn_pexp2l [in ssrnat]
ltn_pmod [in div]
ltn_Pmull [in ssrnat]
ltn_Pmulr [in ssrnat]
ltn_pmul2l [in ssrnat]
ltn_pmul2r [in ssrnat]
ltn_predK [in ssrnat]
ltn_Sdouble [in ssrnat]
ltn_size_undup [in seq]
ltn_sqr [in ssrnat]
ltn_subS [in ssrnat]
ltn_sub2l [in ssrnat]
ltn_sub2r [in ssrnat]
ltn_trans [in ssrnat]
ltn_unsplit [in fintype]
ltP [in ssrnat]
lt0n [in ssrnat]
lt0n_neq0 [in ssrnat]
lt_irrelevance [in ssrnat]



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 _ (5434 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 _ (89 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 _ (58 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 _ (2752 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 _ (233 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 _ (145 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 _ (139 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 _ (50 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 _ (1267 entries)
Moduleid 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 _ (47 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 _ (24 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 _ (609 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 _ (21 entries)