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)

L

LaGrange [lemma, in groups]
LaGrange [section, in groups]
LaGrangeI [lemma, in groups]
LaGrange.gT [variable, in groups]
LaGrange_index [lemma, in groups]
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]
lcoset [definition, in groups]
lcosetE [lemma, in groups]
lcosetM [lemma, in groups]
lcosetP [lemma, in groups]
lcosets [definition, in groups]
lcosetsP [lemma, in groups]
lcosets_invg [lemma, in groups]
lcoset_id [lemma, in groups]
lcoset_refl [lemma, in groups]
lcoset_sym [lemma, in groups]
lcoset_trans [lemma, in groups]
lcoset_transl [lemma, in groups]
lcoset_transr [lemma, in groups]
lcutmx [definition, in matrix]
lead_coef [definition, in poly]
lead_coefC [lemma, in poly]
lead_coefE [lemma, in poly]
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_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_inverse [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]
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_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_pdiv [lemma, in prime]
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 fintype]
liftK [lemma, in fintype]
lift0_mx [definition, in matrix]
lift0_mx_is_perm [lemma, in matrix]
lift0_mx_perm [lemma, in matrix]
lift0_perm [definition, in matrix]
lift0_permK [lemma, in matrix]
lift0_perm0 [lemma, in matrix]
lift0_perm_eq0 [lemma, in matrix]
lift0_perm_lift [lemma, in matrix]
lift_inj [lemma, in fintype]
lift_perm [definition, in matrix]
lift_permK [lemma, in matrix]
lift_permM [lemma, in matrix]
lift_permV [lemma, in matrix]
lift_perm1 [lemma, in matrix]
lift_perm_fun [definition, in matrix]
lift_perm_id [lemma, in matrix]
lift_perm_lift [lemma, in matrix]
lift_subproof [lemma, in fintype]
llsubmx [definition, in matrix]
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_exp [lemma, in prime]
logn_gauss [lemma, in prime]
logn_gt0 [lemma, in prime]
logn_mul [lemma, in prime]
logn_prime [lemma, in prime]
logn_rec [definition, in prime]
lone_subgroup_char [lemma, in automorphism]
looping [definition, in paths]
loopingP [lemma, in paths]
looping_order [lemma, in connect]
looping_uniq [lemma, in paths]
lrsubmx [definition, in matrix]
lshift [definition, in fintype]
lshift_ord1 [lemma, in zmodp]
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]
lt0p [definition, in zmodp]
lt1p [definition, in zmodp]
lt_irrelevance [lemma, 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 _ (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)