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

last [definition, in seq]
lastI [lemma, in seq]
LastNil [constructor, in seq]
lastP [lemma, in seq]
LastRcons [constructor, in seq]
last_cat [lemma, in seq]
last_cons [lemma, in seq]
last_ind [lemma, in seq]
last_map [lemma, in seq]
last_nth [lemma, in seq]
last_rcons [lemma, in seq]
last_spec [inductive, in seq]
last_traject [lemma, in paths]
lcmn [definition, in div]
lcmnA [lemma, in div]
lcmnC [lemma, in div]
lcmn0 [lemma, in div]
lcmn1 [lemma, in div]
lcmn_addoid [definition, in bigops]
lcmn_comoid [definition, in bigops]
lcmn_gt0 [lemma, in div]
lcmn_monoid [definition, in bigops]
lcm0n [lemma, in div]
lcm1n [lemma, in div]
lead_coef [definition, in poly]
lead_coefC [lemma, in poly]
lead_coefE [lemma, in poly]
lead_coefT [definition, in closedfields]
lead_coefTP [lemma, in closedfields]
lead_coefT_qf [lemma, in closedfields]
lead_coefX [lemma, in poly]
lead_coefXn [lemma, in poly]
lead_coef0 [lemma, in poly]
lead_coef1 [lemma, in poly]
lead_coef_addl [lemma, in poly]
lead_coef_eq0 [lemma, in poly]
lead_coef_map [lemma, in poly]
lead_coef_map_eq [lemma, in poly]
lead_coef_monic_mul [lemma, in poly]
lead_coef_mulX [lemma, in poly]
lead_coef_mul_id [lemma, in poly]
lead_coef_mul_monic [lemma, in poly]
lead_coef_opp [lemma, in poly]
lead_coef_poly [lemma, in poly]
lead_coef_proper_mul [lemma, in poly]
left_arc [lemma, in paths]
left_commutative [definition, in ssrfun]
left_distributive [definition, in ssrfun]
left_id [definition, in ssrfun]
left_injective [definition, in ssrfun]
left_inverse [definition, in ssrfun]
left_loop [definition, in ssrfun]
left_transitive [definition, in ssrbool]
left_zero [definition, in ssrfun]
leP [lemma, in ssrnat]
leq [definition, in ssrnat]
leqif [definition, in ssrnat]
leqifP [lemma, in ssrnat]
leqif_add [lemma, in ssrnat]
leqif_eq [lemma, in ssrnat]
leqif_geq [lemma, in ssrnat]
leqif_mul [lemma, in ssrnat]
leqif_refl [lemma, in ssrnat]
leqif_trans [lemma, in ssrnat]
leqNgt [lemma, in ssrnat]
leqnn [lemma, in ssrnat]
LeqNotGtn [constructor, in ssrnat]
leqnSn [lemma, in ssrnat]
leqn0 [lemma, in ssrnat]
leqn1 [lemma, in polydiv]
leqn2 [lemma, in polydiv]
leqP [lemma, in ssrnat]
leqSpred [lemma, in ssrnat]
leqW [lemma, in ssrnat]
leq0n [lemma, in ssrnat]
leq_add [lemma, in ssrnat]
leq_addl [lemma, in ssrnat]
leq_addr [lemma, in ssrnat]
leq_add2l [lemma, in ssrnat]
leq_add2r [lemma, in ssrnat]
leq_bigmax [lemma, in bigops]
leq_bigmax_cond [lemma, in bigops]
leq_bump [lemma, in fintype]
leq_bump2 [lemma, in fintype]
leq_b1 [lemma, in ssrnat]
leq_card_cover [lemma, in finset]
leq_card_setU [lemma, in finset]
leq_coef_size [lemma, in poly]
leq_div [lemma, in div]
leq_divl [lemma, in div]
leq_divr [lemma, in div]
leq_double [lemma, in ssrnat]
leq_eqVlt [lemma, in ssrnat]
leq_exp2l [lemma, in ssrnat]
leq_exp2r [lemma, in ssrnat]
leq_floor [lemma, in div]
leq_image_card [lemma, in fintype]
leq_imset_card [lemma, in finset]
leq_ltn_trans [lemma, in ssrnat]
leq_maxl [lemma, in ssrnat]
leq_maxr [lemma, in ssrnat]
leq_minl [lemma, in ssrnat]
leq_minr [lemma, in ssrnat]
leq_mod [lemma, in div]
leq_mul [lemma, in ssrnat]
leq_mul2l [lemma, in ssrnat]
leq_mul2r [lemma, in ssrnat]
leq_of_leqif [definition, in ssrnat]
leq_ord [lemma, in fintype]
leq_pexp2l [lemma, in ssrnat]
leq_pmull [lemma, in ssrnat]
leq_pmulr [lemma, in ssrnat]
leq_pmul2l [lemma, in ssrnat]
leq_pmul2r [lemma, in ssrnat]
leq_pred [lemma, in ssrnat]
leq_Sdouble [lemma, in ssrnat]
leq_size_coef [lemma, in poly]
leq_size_perm [lemma, in seq]
leq_size_uniq [lemma, in seq]
leq_sqr [lemma, in ssrnat]
leq_subr [lemma, in ssrnat]
leq_subS [lemma, in ssrnat]
leq_sub2 [lemma, in ssrnat]
leq_sub2l [lemma, in ssrnat]
leq_sub2r [lemma, in ssrnat]
leq_sub_add [lemma, in ssrnat]
leq_total [lemma, in ssrnat]
leq_trans [lemma, in ssrnat]
leq_xor_gtn [inductive, in ssrnat]
le_irrelevance [lemma, in ssrnat]
lift [definition, in closedfields]
lift [definition, in fintype]
liftK [lemma, in fintype]
lift_inj [lemma, in fintype]
lift_subproof [lemma, in fintype]
LmodMixin [abbreviation, in ssralg]
lmodType [abbreviation, in ssralg]
LmodType [abbreviation, in ssralg]
Lmodule [moduleid, in ssralg]
LocalGlobal [section, in ssrbool]
LocalGlobal.D1 [variable, in ssrbool]
LocalGlobal.d1 [variable, in ssrbool]
LocalGlobal.d1' [variable, in ssrbool]
LocalGlobal.d2 [variable, in ssrbool]
LocalGlobal.D2 [variable, in ssrbool]
LocalGlobal.d2' [variable, in ssrbool]
LocalGlobal.D3 [variable, in ssrbool]
LocalGlobal.d3 [variable, in ssrbool]
LocalGlobal.d3' [variable, in ssrbool]
LocalGlobal.f [variable, in ssrbool]
LocalGlobal.f' [variable, in ssrbool]
LocalGlobal.g [variable, in ssrbool]
LocalGlobal.h [variable, in ssrbool]
LocalGlobal.P1 [variable, in ssrbool]
LocalGlobal.P2 [variable, in ssrbool]
LocalGlobal.P3 [variable, in ssrbool]
LocalGlobal.Q1 [variable, in ssrbool]
LocalGlobal.Q1l [variable, in ssrbool]
LocalGlobal.Q2 [variable, in ssrbool]
LocalGlobal.sub1 [variable, in ssrbool]
LocalGlobal.sub2 [variable, in ssrbool]
LocalGlobal.sub3 [variable, in ssrbool]
LocalGlobal.T1 [variable, in ssrbool]
LocalGlobal.T2 [variable, in ssrbool]
LocalGlobal.T3 [variable, in ssrbool]
LocalProperties [section, in ssrbool]
LocalProperties.d1 [variable, in ssrbool]
LocalProperties.d2 [variable, in ssrbool]
LocalProperties.d3 [variable, in ssrbool]
LocalProperties.f [variable, in ssrbool]
LocalProperties.T1 [variable, in ssrbool]
LocalProperties.T2 [variable, in ssrbool]
LocalProperties.T3 [variable, in ssrbool]
lock [lemma, in ssreflect]
locked [definition, in ssreflect]
logn [definition, in prime]
lognE [lemma, in prime]
logn0 [lemma, in prime]
logn1 [lemma, in prime]
logn_div [lemma, in prime]
logn_exp [lemma, in prime]
logn_gauss [lemma, in prime]
logn_gt0 [lemma, in prime]
logn_mul [lemma, in prime]
logn_part [lemma, in prime]
logn_prime [lemma, in prime]
logn_rec [definition, in prime]
looping [definition, in paths]
loopingP [lemma, in paths]
looping_order [lemma, in connect]
looping_uniq [lemma, in paths]
lshift [definition, in fintype]
lshift_subproof [lemma, in fintype]
ltn [definition, in ssrnat]
ltngtP [lemma, in ssrnat]
ltnn [lemma, in ssrnat]
ltnNge [lemma, in ssrnat]
LtnNotGeq [constructor, in ssrnat]
ltnP [lemma, in ssrnat]
ltnS [lemma, in ssrnat]
ltnSn [lemma, in ssrnat]
ltnW [lemma, in ssrnat]
ltn0 [lemma, in ssrnat]
ltn0Sn [lemma, in ssrnat]
ltn_addl [lemma, in ssrnat]
ltn_addr [lemma, in ssrnat]
ltn_add2l [lemma, in ssrnat]
ltn_add2r [lemma, in ssrnat]
ltn_add_sub [lemma, in ssrnat]
ltn_ceil [lemma, in div]
ltn_divl [lemma, in div]
ltn_divr [lemma, in div]
ltn_double [lemma, in ssrnat]
ltn_expl [lemma, in ssrnat]
ltn_exp2l [lemma, in ssrnat]
ltn_exp2r [lemma, in ssrnat]
ltn_log0 [lemma, in prime]
ltn_mod [lemma, in div]
ltn_mul [lemma, in ssrnat]
ltn_mul2l [lemma, in ssrnat]
ltn_mul2r [lemma, in ssrnat]
ltn_neqAle [lemma, in ssrnat]
ltn_ord [lemma, in fintype]
ltn_Pdiv [lemma, in div]
ltn_pdiv2_prime [lemma, in prime]
ltn_pexp2l [lemma, in ssrnat]
ltn_pmod [lemma, in div]
ltn_Pmull [lemma, in ssrnat]
ltn_Pmulr [lemma, in ssrnat]
ltn_pmul2l [lemma, in ssrnat]
ltn_pmul2r [lemma, in ssrnat]
ltn_predK [lemma, in ssrnat]
ltn_Sdouble [lemma, in ssrnat]
ltn_size_undup [lemma, in seq]
ltn_sqr [lemma, in ssrnat]
ltn_subS [lemma, in ssrnat]
ltn_sub2l [lemma, in ssrnat]
ltn_sub2r [lemma, in ssrnat]
ltn_trans [lemma, in ssrnat]
ltn_unsplit [lemma, in fintype]
ltn_xor_geq [inductive, in ssrnat]
ltP [lemma, in ssrnat]
lt0n [lemma, in ssrnat]
lt0n_neq0 [lemma, in ssrnat]
lt_irrelevance [lemma, in ssrnat]
lt_sizeT [definition, in closedfields]



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)