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

LaGrange [section, in fingroup]
LaGrange [lemma, in fingroup]
LaGrangeI [lemma, in fingroup]
LaGrangeMl [lemma, in fingroup]
LaGrangeMr [lemma, in fingroup]
LaGrange_index [lemma, in fingroup]
LaGrange.gT [variable, in fingroup]
Lalgebra [module, in ssralg]
Lalgebra [module, in finalg]
LAlgLinearApp [section, in vector]
LAlgLinearApp.R [variable, in vector]
LAlgLinearApp.T [variable, in vector]
LAlgLinearApp.V [variable, in vector]
LAlgLinearApp.W [variable, in vector]
LAlgLinearApp.Z [variable, in vector]
LApp [module, in vector]
lappE [definition, in vector]
lapp_rep [definition, in vector]
lapp_addl [lemma, in vector]
lapp_add0 [lemma, in vector]
lapp_choiceMixin [definition, in vector]
lapp_of_fun [definition, in vector]
lapp_scale1 [lemma, in vector]
lapp_zmodMixin [definition, in vector]
lapp_of_funK [lemma, in vector]
lapp_rep_bij [lemma, in vector]
lapp_addr [lemma, in vector]
lapp_addA [lemma, in vector]
lapp_rep_is_linear [definition, in vector]
lapp_scaleA [lemma, in vector]
lapp_addC [lemma, in vector]
lapp_addN [lemma, in vector]
lapp_lmodMixin [definition, in vector]
lapp_rep_linear [definition, in vector]
lapp_lmodType [definition, in vector]
lapp_zmodType [definition, in vector]
lapp_choiceType [definition, in vector]
lapp_eqType [definition, in vector]
lapp_eqMixin [definition, in vector]
LApp.algType [definition, in vector]
LApp.lalgType [definition, in vector]
LApp.LinearAppStruct [section, in vector]
LApp.LinearAppStruct.dim_nz [variable, in vector]
LApp.LinearAppStruct.R [variable, in vector]
LApp.LinearAppStruct.V [variable, in vector]
LApp.revRingType [definition, in vector]
LApp.ringMixin [definition, in vector]
LApp.ringType [definition, in vector]
last [definition, in seq]
lastI [lemma, in seq]
LastNil [constructor, in seq]
lastP [lemma, in seq]
LastRcons [constructor, in seq]
last_spec [inductive, in seq]
last_rcons [lemma, in seq]
last_mod [definition, in mxrepresentation]
last_ind [lemma, in seq]
last_cat [lemma, in seq]
last_traject [lemma, in path]
last_nth [lemma, in seq]
last_map [lemma, in seq]
last_cons [lemma, in seq]
lcmn [definition, in div]
lcmnA [lemma, in div]
lcmnC [lemma, in div]
lcmn_exp [lemma, in div]
lcmn_addoid [definition, in bigop]
lcmn_comoid [definition, in bigop]
lcmn_monoid [definition, in bigop]
lcmn_mulr [lemma, in div]
lcmn_gt0 [lemma, in div]
lcmn_mull [lemma, in div]
lcmn0 [lemma, in div]
lcmn1 [lemma, in div]
lcm0n [lemma, in div]
lcm1n [lemma, in div]
lcnE [lemma, in nilpotent]
lcnP [lemma, in nilpotent]
lcnS [lemma, in nilpotent]
lcnSn [lemma, in nilpotent]
lcnSnS [lemma, in nilpotent]
lcn_char [lemma, in nilpotent]
lcn_subS [lemma, in nilpotent]
lcn_normalS [lemma, in nilpotent]
lcn_sub_leq [lemma, in nilpotent]
lcn_norm [lemma, in nilpotent]
lcn_normal [lemma, in nilpotent]
lcn_cprod [lemma, in nilpotent]
lcn_nil_classP [lemma, in nilpotent]
lcn_cont [lemma, in nilpotent]
lcn_central [lemma, in nilpotent]
lcn_sub [lemma, in nilpotent]
lcn_mgFun [definition, in nilpotent]
lcn_gFun [definition, in nilpotent]
lcn_igFun [definition, in nilpotent]
lcn_group_set [lemma, in nilpotent]
lcn0 [lemma, in nilpotent]
lcn1 [lemma, in nilpotent]
lcn2 [lemma, in nilpotent]
lcoset [definition, in fingroup]
lcosetE [lemma, in fingroup]
lcosetK [lemma, in fingroup]
lcosetKV [lemma, in fingroup]
lcosetM [lemma, in fingroup]
lcosetP [lemma, in fingroup]
lcosets [definition, in fingroup]
lcosetS [lemma, in fingroup]
lcosetsP [lemma, in fingroup]
lcosets_invg [lemma, in fingroup]
lcoset_trans [lemma, in fingroup]
lcoset_transr [lemma, in fingroup]
lcoset_transl [lemma, in fingroup]
lcoset_refl [lemma, in fingroup]
lcoset_id [lemma, in fingroup]
lcoset_inj [lemma, in fingroup]
lcoset_sym [lemma, in fingroup]
lcoset1 [lemma, in fingroup]
Ldiv [definition, in abelian]
LdivJ [lemma, in abelian]
LdivP [lemma, in abelian]
LdivT_J [lemma, in abelian]
lead_coef_exp_id [lemma, in poly]
lead_coef_map [lemma, in poly]
lead_coefE [lemma, in poly]
lead_coef_map_eq [lemma, in poly]
lead_coef_addl [lemma, in poly]
lead_coef_opp [lemma, in poly]
lead_coef0 [lemma, in poly]
lead_coef_eq0 [lemma, in poly]
lead_coef_Imul [lemma, in poly]
lead_coefC [lemma, in poly]
lead_coef_proper_mul [lemma, in poly]
lead_coef1 [lemma, in poly]
lead_coef_mul_monic [lemma, in poly]
lead_coefXn [lemma, in poly]
lead_coefX [lemma, in poly]
lead_coef_mulX [lemma, in poly]
lead_coef_monic_mul [lemma, in poly]
lead_coef_poly [lemma, in poly]
lead_coef [definition, in poly]
left_injective [definition, in ssrfun]
left_transitive [definition, in ssrbool]
left_arc [lemma, in path]
left_id [definition, in ssrfun]
left_loop [definition, in ssrfun]
left_inverse [definition, in ssrfun]
left_distributive [definition, in ssrfun]
left_mx_ideal [definition, in mxalgebra]
left_commutative [definition, in ssrfun]
left_zero [definition, in ssrfun]
leP [lemma, in ssrnat]
leq [definition, in ssrnat]
leqif [definition, in ssrnat]
leqifP [lemma, in ssrnat]
leqif_refl [lemma, in ssrnat]
leqif_sum [lemma, in bigop]
leqif_eq [lemma, in ssrnat]
leqif_add [lemma, in ssrnat]
leqif_trans [lemma, in ssrnat]
leqif_geq [lemma, in ssrnat]
leqif_mul [lemma, in ssrnat]
leqif_add_distn [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]
leq_div [lemma, in div]
leq_trans [lemma, in ssrnat]
leq_bigmax [lemma, in bigop]
leq_homg [lemma, in morphism]
leq_pred [lemma, in ssrnat]
leq_bump [lemma, in fintype]
leq_add2l [lemma, in ssrnat]
leq_add2r [lemma, in ssrnat]
leq_maxl [lemma, in ssrnat]
leq_pmul2l [lemma, in ssrnat]
leq_pmul2r [lemma, in ssrnat]
leq_add_distn [lemma, in ssrnat]
leq_sub_add [lemma, in ssrnat]
leq_mul2r [lemma, in ssrnat]
leq_size_perm [lemma, in seq]
leq_xor_gtn [inductive, in ssrnat]
leq_subS [lemma, in ssrnat]
leq_pmulr [lemma, in ssrnat]
leq_exp2r [lemma, in ssrnat]
leq_pexp2l [lemma, in ssrnat]
leq_of_leqif [definition, in ssrnat]
leq_size_uniq [lemma, in seq]
leq_divl [lemma, in div]
leq_Sdouble [lemma, in ssrnat]
leq_total [lemma, in ssrnat]
leq_mul [lemma, in ssrnat]
leq_sub2l [lemma, in ssrnat]
leq_addl [lemma, in ssrnat]
leq_card_setU [lemma, in finset]
leq_image_card [lemma, in fintype]
leq_sqr [lemma, in ssrnat]
leq_imset_card [lemma, in finset]
leq_quotient [lemma, in quotient]
leq_size_coef [lemma, in poly]
leq_morphim [lemma, in morphism]
leq_b1 [lemma, in ssrnat]
leq_double [lemma, in ssrnat]
leq_mul2l [lemma, in ssrnat]
leq_divr [lemma, in div]
leq_card_cover [lemma, in finset]
leq_bigmax_cond [lemma, in bigop]
leq_ord [lemma, in fintype]
leq_floor [lemma, in div]
leq_mod [lemma, in div]
leq_bin2l [lemma, in binomial]
leq_subr [lemma, in ssrnat]
leq_add [lemma, in ssrnat]
leq_maxr [lemma, in ssrnat]
leq_coef_size [lemma, in poly]
leq_sub2 [lemma, in ssrnat]
leq_eqVlt [lemma, in ssrnat]
leq_exp2l [lemma, in ssrnat]
leq_pmull [lemma, in ssrnat]
leq_addr [lemma, in ssrnat]
leq_bump2 [lemma, in fintype]
leq_ltn_trans [lemma, in ssrnat]
leq_minl [lemma, in ssrnat]
leq_sub2r [lemma, in ssrnat]
leq_minr [lemma, in ssrnat]
leq0n [lemma, in ssrnat]
le_irrelevance [lemma, in ssrnat]
lift [definition, in fintype]
liftK [lemma, in fintype]
LiftPerm [section, in perm]
LiftPerm.n [variable, in perm]
lift_permK [lemma, in perm]
lift_perm [definition, in perm]
lift_perm_lift [lemma, in perm]
lift_perm_id [lemma, in perm]
lift_subproof [lemma, in fintype]
lift_inj [lemma, in fintype]
lift_permV [lemma, in perm]
lift_perm_fun [definition, in perm]
lift_max [lemma, in fintype]
lift_perm1 [lemma, in perm]
lift_permM [lemma, in perm]
lift0 [lemma, in fintype]
lift0_mx [definition, in matrix]
lift0_perm_lift [lemma, in matrix]
lift0_permK [lemma, in matrix]
lift0_perm0 [lemma, in matrix]
lift0_perm [definition, in matrix]
lift0_perm_eq0 [lemma, in matrix]
lift0_mx_perm [lemma, in matrix]
lift0_mx_is_perm [lemma, in matrix]
limg [definition, in vector]
limgE [lemma, in vector]
limg_add [lemma, in vector]
limg_cap [lemma, in vector]
limg_proj [lemma, in vector]
limg_sum [lemma, in vector]
limg_monotone [lemma, in vector]
limg_ker0 [lemma, in vector]
limg_dim_eq [lemma, in vector]
limg_bigcap [lemma, in vector]
limg_comp [lemma, in vector]
limg_ker_dim [lemma, in vector]
limg_ker_compl [lemma, in vector]
limg_span [lemma, in vector]
limg_is_basis [lemma, in vector]
limg_inj [lemma, in vector]
limg0 [lemma, in vector]
lim0g [lemma, in vector]
lim1g [lemma, in vector]
Linear [module, in ssralg]
LinearApp [constructor, in vector]
linearApp [inductive, in vector]
LinearApp [section, in vector]
linearApp_subType [definition, in vector]
LinearApp.phV [variable, in vector]
LinearApp.phW [variable, in vector]
LinearApp.R [variable, in vector]
LinearApp.V [variable, in vector]
LinearApp.W [variable, in vector]
LinearImage [section, in vector]
LinearImage.K [variable, in vector]
LinearImage.V [variable, in vector]
LinearImage.W [variable, in vector]
linearMixin [definition, in vector]
LinearPreImage [section, in vector]
LinearPreImage.K [variable, in vector]
LinearPreImage.V [variable, in vector]
LinearPreImage.W [variable, in vector]
linearVect [definition, in vector]
linear_irr_comp [lemma, in mxrepresentation]
linear_irr [definition, in mxrepresentation]
linear_mxsimple [lemma, in mxrepresentation]
linear_mx_abs_irr [lemma, in mxrepresentation]
lin_mulmx [definition, in matrix]
lin_mulmx_is_linear [lemma, in matrix]
lin_mulmxr [definition, in matrix]
lin_mul_row_is_linear [lemma, in matrix]
lin_mul_row [definition, in matrix]
lin_mul_row_linear [definition, in matrix]
lin_mul_row_additive [definition, in matrix]
lin_mulmx_linear [definition, in matrix]
lin_mulmx_additive [definition, in matrix]
lin_mulmxr_linear [definition, in matrix]
lin_mulmxr_additive [definition, in matrix]
lin_mx [definition, in matrix]
lin_mulmxr_is_linear [lemma, in matrix]
lin1_mx [definition, in matrix]
lker [definition, in vector]
lkerE [lemma, in vector]
lker_proj [lemma, in vector]
lker0P [lemma, in vector]
Lmodule [module, in finalg]
Lmodule [module, 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]
lognSg [lemma, in fingroup]
logn_quotient_cent_cyclic_pgroup [lemma, in pgroup]
logn_mul [lemma, in prime]
logn_exp [lemma, in prime]
logn_quotient [lemma, in abelian]
logn_card_GL_p [lemma, in mxalgebra]
logn_morphim [lemma, in quotient]
logn_rec [definition, in prime]
logn_le_p_rank [lemma, in abelian]
logn_div [lemma, in prime]
logn_quotient_pnElem [lemma, in abelian]
logn_part [lemma, in prime]
logn_gt0 [lemma, in prime]
logn_gauss [lemma, in prime]
logn_prime [lemma, in prime]
logn0 [lemma, in prime]
logn1 [lemma, in prime]
lone_subgroup_char [lemma, in automorphism]
loop [definition, in vector]
looping [definition, in path]
loopingP [lemma, in path]
looping_order [lemma, in fingraph]
looping_uniq [lemma, in path]
LowerCentral [section, in nilpotent]
LowerCentral.gT [variable, in nilpotent]
lower_central_at_group [definition, in nilpotent]
lower_central_at [definition, in nilpotent]
lower_central_at_rec [definition, in nilpotent]
lpre_img [definition, in vector]
lpre_img_monotone [lemma, in vector]
lpre_img_full [lemma, in vector]
lpre_imgK [lemma, in vector]
lpre_img0 [lemma, in vector]
lpre_imgE [lemma, in vector]
lreg [definition, in poly]
lregM [lemma, in poly]
lregP [lemma, in poly]
lregX [lemma, in poly]
lreg_scale0 [lemma, in poly]
lreg_lead0 [lemma, in poly]
lreg_lead [lemma, in poly]
lreg_size [lemma, in poly]
lreg0 [lemma, in poly]
lreg1 [lemma, in poly]
LRMorphism [module, in ssralg]
lshift [definition, in fintype]
lshift_subproof [lemma, in fintype]
lshift0 [lemma, in zmodp]
lsubmx [definition, in matrix]
lsubmx_linear [definition, in matrix]
lsubmx_additive [definition, in matrix]
ltmx [definition, in mxalgebra]
ltmxE [lemma, in mxalgebra]
ltmxEneq [lemma, in mxalgebra]
ltmxErank [lemma, in mxalgebra]
ltmxW [lemma, in mxalgebra]
ltmx_trans [lemma, in mxalgebra]
ltmx_sub_trans [lemma, in mxalgebra]
ltmx_irrefl [lemma, in mxalgebra]
ltmx0 [lemma, in mxalgebra]
ltmx1 [lemma, in mxalgebra]
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]
ltn_addl [lemma, in ssrnat]
ltn_addr [lemma, in ssrnat]
ltn_ord [lemma, in fintype]
ltn_predK [lemma, in ssrnat]
ltn_add2l [lemma, in ssrnat]
ltn_leqif [lemma, in ssrnat]
ltn_expl [lemma, in ssrnat]
ltn_divl [lemma, in div]
ltn_mul2l [lemma, in ssrnat]
ltn_quotient [lemma, in quotient]
ltn_subS [lemma, in ssrnat]
ltn_sqr [lemma, in ssrnat]
ltn_log0 [lemma, in prime]
ltn_Pmull [lemma, in ssrnat]
ltn_exp2l [lemma, in ssrnat]
ltn_add2r [lemma, in ssrnat]
ltn_pexp2l [lemma, in ssrnat]
ltn_log_quotient [lemma, in pgroup]
ltn_mod [lemma, in div]
ltn_mul2r [lemma, in ssrnat]
ltn_sub2r [lemma, in ssrnat]
ltn_pmul2r [lemma, in ssrnat]
ltn_mul [lemma, in ssrnat]
ltn_neqAle [lemma, in ssrnat]
ltn_xor_geq [inductive, in ssrnat]
ltn_trans [lemma, in ssrnat]
ltn_unsplit [lemma, in fintype]
ltn_morphim [lemma, in morphism]
ltn_pmod [lemma, in div]
ltn_ceil [lemma, in div]
ltn_sub2l [lemma, in ssrnat]
ltn_pmul2l [lemma, in ssrnat]
ltn_size_undup [lemma, in seq]
ltn_add_sub [lemma, in ssrnat]
ltn_exp2r [lemma, in ssrnat]
ltn_Sdouble [lemma, in ssrnat]
ltn_divr [lemma, in div]
ltn_pdiv2_prime [lemma, in prime]
ltn_Pdiv [lemma, in div]
ltn_double [lemma, in ssrnat]
ltn_Pmulr [lemma, in ssrnat]
ltn0 [lemma, in ssrnat]
ltn0Sn [lemma, in ssrnat]
ltP [lemma, in ssrnat]
ltqm [definition, in extremal]
ltrq [definition, in extremal]
lt_eqmx [lemma, in mxalgebra]
lt_irrelevance [lemma, in ssrnat]
lt0mx [lemma, in mxalgebra]
lt0n [lemma, in ssrnat]
lt0n_neq0 [lemma, in ssrnat]
lt1mx [lemma, in mxalgebra]
LUP_card_GL [lemma, in mxalgebra]
LUr [definition, in mxalgebra]
l2ev [definition, in vector]
l2ev_cons [lemma, 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)