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)

L (lemma)

LaGrange [in fingroup]
LaGrangeI [in fingroup]
LaGrangeMl [in fingroup]
LaGrangeMr [in fingroup]
LaGrange_index [in fingroup]
lapp_addl [in vector]
lapp_add0 [in vector]
lapp_scale1 [in vector]
lapp_of_funK [in vector]
lapp_rep_bij [in vector]
lapp_addr [in vector]
lapp_addA [in vector]
lapp_scaleA [in vector]
lapp_addC [in vector]
lapp_addN [in vector]
lastI [in seq]
lastP [in seq]
last_rcons [in seq]
last_ind [in seq]
last_cat [in seq]
last_traject [in path]
last_nth [in seq]
last_map [in seq]
last_cons [in seq]
lcmnA [in div]
lcmnC [in div]
lcmn_exp [in div]
lcmn_mulr [in div]
lcmn_gt0 [in div]
lcmn_mull [in div]
lcmn0 [in div]
lcmn1 [in div]
lcm0n [in div]
lcm1n [in div]
lcnE [in nilpotent]
lcnP [in nilpotent]
lcnS [in nilpotent]
lcnSn [in nilpotent]
lcnSnS [in nilpotent]
lcn_char [in nilpotent]
lcn_subS [in nilpotent]
lcn_normalS [in nilpotent]
lcn_sub_leq [in nilpotent]
lcn_norm [in nilpotent]
lcn_normal [in nilpotent]
lcn_cprod [in nilpotent]
lcn_nil_classP [in nilpotent]
lcn_cont [in nilpotent]
lcn_central [in nilpotent]
lcn_sub [in nilpotent]
lcn_group_set [in nilpotent]
lcn0 [in nilpotent]
lcn1 [in nilpotent]
lcn2 [in nilpotent]
lcosetE [in fingroup]
lcosetK [in fingroup]
lcosetKV [in fingroup]
lcosetM [in fingroup]
lcosetP [in fingroup]
lcosetS [in fingroup]
lcosetsP [in fingroup]
lcosets_invg [in fingroup]
lcoset_trans [in fingroup]
lcoset_transr [in fingroup]
lcoset_transl [in fingroup]
lcoset_refl [in fingroup]
lcoset_id [in fingroup]
lcoset_inj [in fingroup]
lcoset_sym [in fingroup]
lcoset1 [in fingroup]
LdivJ [in abelian]
LdivP [in abelian]
LdivT_J [in abelian]
lead_coef_exp_id [in poly]
lead_coef_map [in poly]
lead_coefE [in poly]
lead_coef_map_eq [in poly]
lead_coef_addl [in poly]
lead_coef_opp [in poly]
lead_coef0 [in poly]
lead_coef_eq0 [in poly]
lead_coef_Imul [in poly]
lead_coefC [in poly]
lead_coef_proper_mul [in poly]
lead_coef1 [in poly]
lead_coef_mul_monic [in poly]
lead_coefXn [in poly]
lead_coefX [in poly]
lead_coef_mulX [in poly]
lead_coef_monic_mul [in poly]
lead_coef_poly [in poly]
left_arc [in path]
leP [in ssrnat]
leqifP [in ssrnat]
leqif_refl [in ssrnat]
leqif_sum [in bigop]
leqif_eq [in ssrnat]
leqif_add [in ssrnat]
leqif_trans [in ssrnat]
leqif_geq [in ssrnat]
leqif_mul [in ssrnat]
leqif_add_distn [in ssrnat]
leqNgt [in ssrnat]
leqnn [in ssrnat]
leqnSn [in ssrnat]
leqn0 [in ssrnat]
leqP [in ssrnat]
leqSpred [in ssrnat]
leqW [in ssrnat]
leq_div [in div]
leq_trans [in ssrnat]
leq_bigmax [in bigop]
leq_homg [in morphism]
leq_pred [in ssrnat]
leq_bump [in fintype]
leq_add2l [in ssrnat]
leq_add2r [in ssrnat]
leq_maxl [in ssrnat]
leq_pmul2l [in ssrnat]
leq_pmul2r [in ssrnat]
leq_add_distn [in ssrnat]
leq_sub_add [in ssrnat]
leq_mul2r [in ssrnat]
leq_size_perm [in seq]
leq_subS [in ssrnat]
leq_pmulr [in ssrnat]
leq_exp2r [in ssrnat]
leq_pexp2l [in ssrnat]
leq_size_uniq [in seq]
leq_divl [in div]
leq_Sdouble [in ssrnat]
leq_total [in ssrnat]
leq_mul [in ssrnat]
leq_sub2l [in ssrnat]
leq_addl [in ssrnat]
leq_card_setU [in finset]
leq_image_card [in fintype]
leq_sqr [in ssrnat]
leq_imset_card [in finset]
leq_quotient [in quotient]
leq_size_coef [in poly]
leq_morphim [in morphism]
leq_b1 [in ssrnat]
leq_double [in ssrnat]
leq_mul2l [in ssrnat]
leq_divr [in div]
leq_card_cover [in finset]
leq_bigmax_cond [in bigop]
leq_ord [in fintype]
leq_floor [in div]
leq_mod [in div]
leq_bin2l [in binomial]
leq_subr [in ssrnat]
leq_add [in ssrnat]
leq_maxr [in ssrnat]
leq_coef_size [in poly]
leq_sub2 [in ssrnat]
leq_eqVlt [in ssrnat]
leq_exp2l [in ssrnat]
leq_pmull [in ssrnat]
leq_addr [in ssrnat]
leq_bump2 [in fintype]
leq_ltn_trans [in ssrnat]
leq_minl [in ssrnat]
leq_sub2r [in ssrnat]
leq_minr [in ssrnat]
leq0n [in ssrnat]
le_irrelevance [in ssrnat]
liftK [in fintype]
lift_permK [in perm]
lift_perm_lift [in perm]
lift_perm_id [in perm]
lift_subproof [in fintype]
lift_inj [in fintype]
lift_permV [in perm]
lift_max [in fintype]
lift_perm1 [in perm]
lift_permM [in perm]
lift0 [in fintype]
lift0_perm_lift [in matrix]
lift0_permK [in matrix]
lift0_perm0 [in matrix]
lift0_perm_eq0 [in matrix]
lift0_mx_perm [in matrix]
lift0_mx_is_perm [in matrix]
limgE [in vector]
limg_add [in vector]
limg_cap [in vector]
limg_proj [in vector]
limg_sum [in vector]
limg_monotone [in vector]
limg_ker0 [in vector]
limg_dim_eq [in vector]
limg_bigcap [in vector]
limg_comp [in vector]
limg_ker_dim [in vector]
limg_ker_compl [in vector]
limg_span [in vector]
limg_is_basis [in vector]
limg_inj [in vector]
limg0 [in vector]
lim0g [in vector]
lim1g [in vector]
linear_irr_comp [in mxrepresentation]
linear_mxsimple [in mxrepresentation]
linear_mx_abs_irr [in mxrepresentation]
lin_mulmx_is_linear [in matrix]
lin_mul_row_is_linear [in matrix]
lin_mulmxr_is_linear [in matrix]
lkerE [in vector]
lker_proj [in vector]
lker0P [in vector]
lock [in ssreflect]
lognE [in prime]
lognSg [in fingroup]
logn_quotient_cent_cyclic_pgroup [in pgroup]
logn_mul [in prime]
logn_exp [in prime]
logn_quotient [in abelian]
logn_card_GL_p [in mxalgebra]
logn_morphim [in quotient]
logn_le_p_rank [in abelian]
logn_div [in prime]
logn_quotient_pnElem [in abelian]
logn_part [in prime]
logn_gt0 [in prime]
logn_gauss [in prime]
logn_prime [in prime]
logn0 [in prime]
logn1 [in prime]
lone_subgroup_char [in automorphism]
loopingP [in path]
looping_order [in fingraph]
looping_uniq [in path]
lpre_img_monotone [in vector]
lpre_img_full [in vector]
lpre_imgK [in vector]
lpre_img0 [in vector]
lpre_imgE [in vector]
lregM [in poly]
lregP [in poly]
lregX [in poly]
lreg_scale0 [in poly]
lreg_lead0 [in poly]
lreg_lead [in poly]
lreg_size [in poly]
lreg0 [in poly]
lreg1 [in poly]
lshift_subproof [in fintype]
lshift0 [in zmodp]
ltmxE [in mxalgebra]
ltmxEneq [in mxalgebra]
ltmxErank [in mxalgebra]
ltmxW [in mxalgebra]
ltmx_trans [in mxalgebra]
ltmx_sub_trans [in mxalgebra]
ltmx_irrefl [in mxalgebra]
ltmx0 [in mxalgebra]
ltmx1 [in mxalgebra]
ltngtP [in ssrnat]
ltnn [in ssrnat]
ltnNge [in ssrnat]
ltnP [in ssrnat]
ltnS [in ssrnat]
ltnSn [in ssrnat]
ltnW [in ssrnat]
ltn_addl [in ssrnat]
ltn_addr [in ssrnat]
ltn_ord [in fintype]
ltn_predK [in ssrnat]
ltn_add2l [in ssrnat]
ltn_leqif [in ssrnat]
ltn_expl [in ssrnat]
ltn_divl [in div]
ltn_mul2l [in ssrnat]
ltn_quotient [in quotient]
ltn_subS [in ssrnat]
ltn_sqr [in ssrnat]
ltn_log0 [in prime]
ltn_Pmull [in ssrnat]
ltn_exp2l [in ssrnat]
ltn_add2r [in ssrnat]
ltn_pexp2l [in ssrnat]
ltn_log_quotient [in pgroup]
ltn_mod [in div]
ltn_mul2r [in ssrnat]
ltn_sub2r [in ssrnat]
ltn_pmul2r [in ssrnat]
ltn_mul [in ssrnat]
ltn_neqAle [in ssrnat]
ltn_trans [in ssrnat]
ltn_unsplit [in fintype]
ltn_morphim [in morphism]
ltn_pmod [in div]
ltn_ceil [in div]
ltn_sub2l [in ssrnat]
ltn_pmul2l [in ssrnat]
ltn_size_undup [in seq]
ltn_add_sub [in ssrnat]
ltn_exp2r [in ssrnat]
ltn_Sdouble [in ssrnat]
ltn_divr [in div]
ltn_pdiv2_prime [in prime]
ltn_Pdiv [in div]
ltn_double [in ssrnat]
ltn_Pmulr [in ssrnat]
ltn0 [in ssrnat]
ltn0Sn [in ssrnat]
ltP [in ssrnat]
lt_eqmx [in mxalgebra]
lt_irrelevance [in ssrnat]
lt0mx [in mxalgebra]
lt0n [in ssrnat]
lt0n_neq0 [in ssrnat]
lt1mx [in mxalgebra]
LUP_card_GL [in mxalgebra]
l2ev_cons [in vector]



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)