| 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 | +(23233 entries) | +
| Notation 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 | +(1373 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 | +(213 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 | +(3475 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 | +(89 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 | +(11853 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 | +(359 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 | +(47 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 | +(103 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 | +(266 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 | +(1118 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 | +(691 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 | +(3461 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 | +(185 entries) | +
L
+Lagrange [lemma, in mathcomp.fingroup.fingroup]+Lagrange [section, in mathcomp.fingroup.fingroup]
+LagrangeI [lemma, in mathcomp.fingroup.fingroup]
+LagrangeMl [lemma, in mathcomp.fingroup.fingroup]
+LagrangeMr [lemma, in mathcomp.fingroup.fingroup]
+Lagrange_index [lemma, in mathcomp.fingroup.fingroup]
+Lagrange.gT [variable, in mathcomp.fingroup.fingroup]
+large_field_PET [lemma, in mathcomp.field.separable]
+last [definition, in mathcomp.ssreflect.seq]
+lastI [lemma, in mathcomp.ssreflect.seq]
+LastNil [constructor, in mathcomp.ssreflect.seq]
+lastP [lemma, in mathcomp.ssreflect.seq]
+LastRcons [constructor, in mathcomp.ssreflect.seq]
+last_traject [lemma, in mathcomp.ssreflect.path]
+last_map [lemma, in mathcomp.ssreflect.seq]
+last_nth [lemma, in mathcomp.ssreflect.seq]
+last_ind [lemma, in mathcomp.ssreflect.seq]
+last_spec [inductive, in mathcomp.ssreflect.seq]
+last_rcons [lemma, in mathcomp.ssreflect.seq]
+last_cat [lemma, in mathcomp.ssreflect.seq]
+last_cons [lemma, in mathcomp.ssreflect.seq]
+lcmn [definition, in mathcomp.ssreflect.div]
+lcmnA [lemma, in mathcomp.ssreflect.div]
+lcmnAC [lemma, in mathcomp.ssreflect.div]
+lcmnACA [lemma, in mathcomp.ssreflect.div]
+lcmnC [lemma, in mathcomp.ssreflect.div]
+lcmnCA [lemma, in mathcomp.ssreflect.div]
+lcmnMl [lemma, in mathcomp.ssreflect.div]
+lcmnMr [lemma, in mathcomp.ssreflect.div]
+lcmn_idPl [lemma, in mathcomp.ssreflect.div]
+lcmn_idPr [lemma, in mathcomp.ssreflect.div]
+lcmn_gt0 [lemma, in mathcomp.ssreflect.div]
+lcmn0 [lemma, in mathcomp.ssreflect.div]
+lcmn1 [lemma, in mathcomp.ssreflect.div]
+lcm0n [lemma, in mathcomp.ssreflect.div]
+lcm1n [lemma, in mathcomp.ssreflect.div]
+lcnE [lemma, in mathcomp.solvable.nilpotent]
+lcnP [lemma, in mathcomp.solvable.nilpotent]
+lcnS [lemma, in mathcomp.solvable.nilpotent]
+lcnSn [lemma, in mathcomp.solvable.nilpotent]
+lcnSnS [lemma, in mathcomp.solvable.nilpotent]
+lcn_neq0 [abbreviation, in mathcomp.field.separable]
+lcn_cont [lemma, in mathcomp.solvable.nilpotent]
+lcn_nil_classP [lemma, in mathcomp.solvable.nilpotent]
+lcn_bigdprod [lemma, in mathcomp.solvable.nilpotent]
+lcn_bigcprod [lemma, in mathcomp.solvable.nilpotent]
+lcn_dprod [lemma, in mathcomp.solvable.nilpotent]
+lcn_cprod [lemma, in mathcomp.solvable.nilpotent]
+lcn_sub_leq [lemma, in mathcomp.solvable.nilpotent]
+lcn_central [lemma, in mathcomp.solvable.nilpotent]
+lcn_normalS [lemma, in mathcomp.solvable.nilpotent]
+lcn_subS [lemma, in mathcomp.solvable.nilpotent]
+lcn_norm [lemma, in mathcomp.solvable.nilpotent]
+lcn_sub [lemma, in mathcomp.solvable.nilpotent]
+lcn_normal [lemma, in mathcomp.solvable.nilpotent]
+lcn_char [lemma, in mathcomp.solvable.nilpotent]
+lcn_group_set [lemma, in mathcomp.solvable.nilpotent]
+lcn0 [lemma, in mathcomp.solvable.nilpotent]
+lcn1 [lemma, in mathcomp.solvable.nilpotent]
+lcn2 [lemma, in mathcomp.solvable.nilpotent]
+Lcorrect [lemma, in mathcomp.solvable.burnside_app]
+lcoset [definition, in mathcomp.fingroup.fingroup]
+lcosetE [lemma, in mathcomp.fingroup.fingroup]
+lcosetK [lemma, in mathcomp.fingroup.fingroup]
+lcosetKV [lemma, in mathcomp.fingroup.fingroup]
+lcosetM [lemma, in mathcomp.fingroup.fingroup]
+lcosetP [lemma, in mathcomp.fingroup.fingroup]
+lcosetS [lemma, in mathcomp.fingroup.fingroup]
+lcosets [definition, in mathcomp.fingroup.fingroup]
+lcosetsP [lemma, in mathcomp.fingroup.fingroup]
+lcoset_id [lemma, in mathcomp.fingroup.fingroup]
+lcoset_trans [lemma, in mathcomp.fingroup.fingroup]
+lcoset_transl [lemma, in mathcomp.fingroup.fingroup]
+lcoset_eqP [lemma, in mathcomp.fingroup.fingroup]
+lcoset_sym [lemma, in mathcomp.fingroup.fingroup]
+lcoset_refl [lemma, in mathcomp.fingroup.fingroup]
+lcoset_inj [lemma, in mathcomp.fingroup.fingroup]
+lcoset1 [lemma, in mathcomp.fingroup.fingroup]
+Ldiv [definition, in mathcomp.solvable.abelian]
+LdivJ [lemma, in mathcomp.solvable.abelian]
+LdivP [lemma, in mathcomp.solvable.abelian]
+LdivT_J [lemma, in mathcomp.solvable.abelian]
+lead_coef_poly_XaY [lemma, in mathcomp.algebra.polyXY]
+lead_coef_map [lemma, in mathcomp.algebra.poly]
+lead_coef_comp [lemma, in mathcomp.algebra.poly]
+lead_coef_exp [lemma, in mathcomp.algebra.poly]
+lead_coefZ [lemma, in mathcomp.algebra.poly]
+lead_coefM [lemma, in mathcomp.algebra.poly]
+lead_coef_map_eq [lemma, in mathcomp.algebra.poly]
+lead_coef_map_inj [lemma, in mathcomp.algebra.poly]
+lead_coef_map_id0 [lemma, in mathcomp.algebra.poly]
+lead_coef_lreg [lemma, in mathcomp.algebra.poly]
+lead_coef_Mmonic [lemma, in mathcomp.algebra.poly]
+lead_coef_monicM [lemma, in mathcomp.algebra.poly]
+lead_coefXn [lemma, in mathcomp.algebra.poly]
+lead_coefMX [lemma, in mathcomp.algebra.poly]
+lead_coefXsubC [lemma, in mathcomp.algebra.poly]
+lead_coefX [lemma, in mathcomp.algebra.poly]
+lead_coef_proper_mul [lemma, in mathcomp.algebra.poly]
+lead_coef1 [lemma, in mathcomp.algebra.poly]
+lead_coefDl [lemma, in mathcomp.algebra.poly]
+lead_coef_opp [lemma, in mathcomp.algebra.poly]
+lead_coef_eq0 [lemma, in mathcomp.algebra.poly]
+lead_coef0 [lemma, in mathcomp.algebra.poly]
+lead_coef_poly [lemma, in mathcomp.algebra.poly]
+lead_coefC [lemma, in mathcomp.algebra.poly]
+lead_coefE [lemma, in mathcomp.algebra.poly]
+lead_coef [definition, in mathcomp.algebra.poly]
+lead_coefT_qf [lemma, in mathcomp.field.closed_field]
+lead_coefTP [lemma, in mathcomp.field.closed_field]
+lead_coefT [definition, in mathcomp.field.closed_field]
+leC_nat [definition, in mathcomp.field.algC]
+left_arc [lemma, in mathcomp.ssreflect.path]
+left_trans [lemma, in mathcomp.ssreflect.generic_quotient]
+left_mx_ideal [definition, in mathcomp.algebra.mxalgebra]
+leNz_nat [lemma, in mathcomp.algebra.ssrint]
+leP [lemma, in mathcomp.ssreflect.ssrnat]
+leq [definition, in mathcomp.ssreflect.ssrnat]
+leqif [definition, in mathcomp.ssreflect.ssrnat]
+leqifP [lemma, in mathcomp.ssreflect.ssrnat]
+leqif_mul [lemma, in mathcomp.ssreflect.ssrnat]
+leqif_add [lemma, in mathcomp.ssreflect.ssrnat]
+leqif_eq [lemma, in mathcomp.ssreflect.ssrnat]
+leqif_geq [lemma, in mathcomp.ssreflect.ssrnat]
+leqif_trans [lemma, in mathcomp.ssreflect.ssrnat]
+leqif_refl [lemma, in mathcomp.ssreflect.ssrnat]
+leqif_sum [lemma, in mathcomp.ssreflect.bigop]
+leqNgt [lemma, in mathcomp.ssreflect.ssrnat]
+leqnn [lemma, in mathcomp.ssreflect.ssrnat]
+LeqNotGtn [constructor, in mathcomp.ssreflect.ssrnat]
+leqnSn [lemma, in mathcomp.ssreflect.ssrnat]
+leqn0 [lemma, in mathcomp.ssreflect.ssrnat]
+leqP [lemma, in mathcomp.ssreflect.ssrnat]
+leqSpred [lemma, in mathcomp.ssreflect.ssrnat]
+leqW [lemma, in mathcomp.ssreflect.ssrnat]
+leq_quotient [lemma, in mathcomp.fingroup.quotient]
+leq_bin2l [lemma, in mathcomp.ssreflect.binomial]
+leq_divLR [lemma, in mathcomp.ssreflect.div]
+leq_divDl [lemma, in mathcomp.ssreflect.div]
+leq_div2l [lemma, in mathcomp.ssreflect.div]
+leq_div2r [lemma, in mathcomp.ssreflect.div]
+leq_divRL [lemma, in mathcomp.ssreflect.div]
+leq_div [lemma, in mathcomp.ssreflect.div]
+leq_mod [lemma, in mathcomp.ssreflect.div]
+leq_trunc_div [lemma, in mathcomp.ssreflect.div]
+leq_size_perm [lemma, in mathcomp.ssreflect.seq]
+leq_size_uniq [lemma, in mathcomp.ssreflect.seq]
+leq_ord [lemma, in mathcomp.ssreflect.fintype]
+leq_bump2 [lemma, in mathcomp.ssreflect.fintype]
+leq_bump [lemma, in mathcomp.ssreflect.fintype]
+leq_image_card [lemma, in mathcomp.ssreflect.fintype]
+leq_sqr [lemma, in mathcomp.ssreflect.ssrnat]
+leq_Sdouble [lemma, in mathcomp.ssreflect.ssrnat]
+leq_double [lemma, in mathcomp.ssreflect.ssrnat]
+leq_b1 [lemma, in mathcomp.ssreflect.ssrnat]
+leq_exp2r [lemma, in mathcomp.ssreflect.ssrnat]
+leq_pexp2l [lemma, in mathcomp.ssreflect.ssrnat]
+leq_exp2l [lemma, in mathcomp.ssreflect.ssrnat]
+leq_pmul2r [lemma, in mathcomp.ssreflect.ssrnat]
+leq_pmul2l [lemma, in mathcomp.ssreflect.ssrnat]
+leq_mul [lemma, in mathcomp.ssreflect.ssrnat]
+leq_mul2r [lemma, in mathcomp.ssreflect.ssrnat]
+leq_mul2l [lemma, in mathcomp.ssreflect.ssrnat]
+leq_pmulr [lemma, in mathcomp.ssreflect.ssrnat]
+leq_pmull [lemma, in mathcomp.ssreflect.ssrnat]
+leq_min [lemma, in mathcomp.ssreflect.ssrnat]
+leq_maxr [lemma, in mathcomp.ssreflect.ssrnat]
+leq_maxl [lemma, in mathcomp.ssreflect.ssrnat]
+leq_max [lemma, in mathcomp.ssreflect.ssrnat]
+leq_sub [lemma, in mathcomp.ssreflect.ssrnat]
+leq_sub2l [lemma, in mathcomp.ssreflect.ssrnat]
+leq_sub2r [lemma, in mathcomp.ssreflect.ssrnat]
+leq_subr [lemma, in mathcomp.ssreflect.ssrnat]
+leq_subLR [lemma, in mathcomp.ssreflect.ssrnat]
+leq_addl [lemma, in mathcomp.ssreflect.ssrnat]
+leq_addr [lemma, in mathcomp.ssreflect.ssrnat]
+leq_add [lemma, in mathcomp.ssreflect.ssrnat]
+leq_add2r [lemma, in mathcomp.ssreflect.ssrnat]
+leq_add2l [lemma, in mathcomp.ssreflect.ssrnat]
+leq_xor_gtn [inductive, in mathcomp.ssreflect.ssrnat]
+leq_total [lemma, in mathcomp.ssreflect.ssrnat]
+leq_ltn_trans [lemma, in mathcomp.ssreflect.ssrnat]
+leq_trans [lemma, in mathcomp.ssreflect.ssrnat]
+leq_eqVlt [lemma, in mathcomp.ssreflect.ssrnat]
+leq_pred [lemma, in mathcomp.ssreflect.ssrnat]
+leq_sizeP [lemma, in mathcomp.algebra.poly]
+leq_bigmax [lemma, in mathcomp.ssreflect.bigop]
+leq_bigmax_cond [lemma, in mathcomp.ssreflect.bigop]
+leq_sum [lemma, in mathcomp.ssreflect.bigop]
+leq_homg [lemma, in mathcomp.fingroup.morphism]
+leq_morphim [lemma, in mathcomp.fingroup.morphism]
+leq_card_cover [lemma, in mathcomp.ssreflect.finset]
+leq_card_setU [lemma, in mathcomp.ssreflect.finset]
+leq_imset_card [lemma, in mathcomp.ssreflect.finset]
+leq0n [lemma, in mathcomp.ssreflect.ssrnat]
+lerq0 [lemma, in mathcomp.algebra.rat]
+lersif [definition, in mathcomp.algebra.interval]
+lersifF [lemma, in mathcomp.algebra.interval]
+lersifN [lemma, in mathcomp.algebra.interval]
+lersifNF [lemma, in mathcomp.algebra.interval]
+lersifS [lemma, in mathcomp.algebra.interval]
+lersifT [lemma, in mathcomp.algebra.interval]
+lersifW [lemma, in mathcomp.algebra.interval]
+lersifxx [lemma, in mathcomp.algebra.interval]
+lersif_in_itv [lemma, in mathcomp.algebra.interval]
+lersif_trans [lemma, in mathcomp.algebra.interval]
+lerz0 [lemma, in mathcomp.algebra.ssrint]
+lerz1 [lemma, in mathcomp.algebra.ssrint]
+ler_rat [lemma, in mathcomp.algebra.rat]
+ler_in_itv [lemma, in mathcomp.algebra.interval]
+ler_nexpz2r [lemma, in mathcomp.algebra.ssrint]
+ler_pexpz2r [lemma, in mathcomp.algebra.ssrint]
+ler_wnexpz2r [lemma, in mathcomp.algebra.ssrint]
+ler_wpexpz2r [lemma, in mathcomp.algebra.ssrint]
+ler_eexpz2l [lemma, in mathcomp.algebra.ssrint]
+ler_niexpz2l [lemma, in mathcomp.algebra.ssrint]
+ler_piexpz2l [lemma, in mathcomp.algebra.ssrint]
+ler_weexpz2l [lemma, in mathcomp.algebra.ssrint]
+ler_wneexpz2l [lemma, in mathcomp.algebra.ssrint]
+ler_wpeexpz2l [lemma, in mathcomp.algebra.ssrint]
+ler_wniexpz2l [lemma, in mathcomp.algebra.ssrint]
+ler_wpiexpz2l [lemma, in mathcomp.algebra.ssrint]
+ler_int [lemma, in mathcomp.algebra.ssrint]
+ler_nmulz2l [lemma, in mathcomp.algebra.ssrint]
+ler_pmulz2l [lemma, in mathcomp.algebra.ssrint]
+ler_wnmulz2l [lemma, in mathcomp.algebra.ssrint]
+ler_wpmulz2l [lemma, in mathcomp.algebra.ssrint]
+ler_wnmulz2r [lemma, in mathcomp.algebra.ssrint]
+ler_wpmulz2r [lemma, in mathcomp.algebra.ssrint]
+ler_nmulz2r [lemma, in mathcomp.algebra.ssrint]
+ler_pmulz2r [lemma, in mathcomp.algebra.ssrint]
+ler0q [lemma, in mathcomp.algebra.rat]
+ler0z [lemma, in mathcomp.algebra.ssrint]
+ler1z [lemma, in mathcomp.algebra.ssrint]
+lezN_nat [lemma, in mathcomp.algebra.ssrint]
+lez_divLR [lemma, in mathcomp.algebra.intdiv]
+lez_divRL [lemma, in mathcomp.algebra.intdiv]
+lez_div [lemma, in mathcomp.algebra.intdiv]
+lez_floor [lemma, in mathcomp.algebra.intdiv]
+lez_addr1 [lemma, in mathcomp.algebra.ssrint]
+lez_add1r [lemma, in mathcomp.algebra.ssrint]
+lez_nat [lemma, in mathcomp.algebra.ssrint]
+lez0_abs [lemma, in mathcomp.algebra.ssrint]
+lez0_nat [lemma, in mathcomp.algebra.ssrint]
+le_rat_total [lemma, in mathcomp.algebra.rat]
+le_rat0_anti [lemma, in mathcomp.algebra.rat]
+le_rat0M [lemma, in mathcomp.algebra.rat]
+le_rat0D [lemma, in mathcomp.algebra.rat]
+le_rat0 [lemma, in mathcomp.algebra.rat]
+le_rat [definition, in mathcomp.algebra.rat]
+le_boundr_bb [lemma, in mathcomp.algebra.interval]
+le_boundl_bb [lemma, in mathcomp.algebra.interval]
+le_boundl_refl [lemma, in mathcomp.algebra.interval]
+le_boundr_refl [lemma, in mathcomp.algebra.interval]
+le_boundr [definition, in mathcomp.algebra.interval]
+le_boundl [definition, in mathcomp.algebra.interval]
+le_irrelevance [lemma, in mathcomp.ssreflect.ssrnat]
+le0z_nat [lemma, in mathcomp.algebra.ssrint]
+LfunAlgebra [section, in mathcomp.algebra.vector]
+LfunAlgebra.R [variable, in mathcomp.algebra.vector]
+LfunAlgebra.vT [variable, in mathcomp.algebra.vector]
+LfunAlgebra.vT_proper [variable, in mathcomp.algebra.vector]
+LfunDefs [section, in mathcomp.algebra.vector]
+LfunDefs.R [variable, in mathcomp.algebra.vector]
+lfunE [lemma, in mathcomp.algebra.vector]
+lfunP [lemma, in mathcomp.algebra.vector]
+lfunPn [lemma, in mathcomp.algebra.vector]
+LfunVectType [section, in mathcomp.algebra.vector]
+LfunVectType.aT [variable, in mathcomp.algebra.vector]
+LfunVectType.R [variable, in mathcomp.algebra.vector]
+LfunVectType.rT [variable, in mathcomp.algebra.vector]
+_ *:l _ [notation, in mathcomp.algebra.vector]
+LfunVspaceDefs [section, in mathcomp.algebra.vector]
+LfunVspaceDefs.K [variable, in mathcomp.algebra.vector]
+LfunZmodType [section, in mathcomp.algebra.vector]
+LfunZmodType.aT [variable, in mathcomp.algebra.vector]
+LfunZmodType.R [variable, in mathcomp.algebra.vector]
+LfunZmodType.rT [variable, in mathcomp.algebra.vector]
+lfun_algType [definition, in mathcomp.algebra.vector]
+lfun_lalgType [definition, in mathcomp.algebra.vector]
+lfun_ringType [definition, in mathcomp.algebra.vector]
+lfun_ringMixin [definition, in mathcomp.algebra.vector]
+lfun_comp_ringType [definition, in mathcomp.algebra.vector]
+lfun_comp_ringMixin [definition, in mathcomp.algebra.vector]
+lfun_simp [definition, in mathcomp.algebra.vector]
+lfun_vectMixin [definition, in mathcomp.algebra.vector]
+lfun_vect_iso [lemma, in mathcomp.algebra.vector]
+lfun_lmodMixin [definition, in mathcomp.algebra.vector]
+lfun_scaleDl [lemma, in mathcomp.algebra.vector]
+lfun_scaleDr [lemma, in mathcomp.algebra.vector]
+lfun_scale1 [lemma, in mathcomp.algebra.vector]
+lfun_scaleA [lemma, in mathcomp.algebra.vector]
+lfun_zmodMixin [definition, in mathcomp.algebra.vector]
+lfun_addN [lemma, in mathcomp.algebra.vector]
+lfun_add0 [lemma, in mathcomp.algebra.vector]
+lfun_addC [lemma, in mathcomp.algebra.vector]
+lfun_addA [lemma, in mathcomp.algebra.vector]
+lfun_is_linear [lemma, in mathcomp.algebra.vector]
+lfun_choiceMixin [definition, in mathcomp.algebra.vector]
+lfun_preim [definition, in mathcomp.algebra.vector]
+lfun_img [definition, in mathcomp.algebra.vector]
+lfun_img_def [definition, in mathcomp.algebra.vector]
+lfun_img_key [lemma, in mathcomp.algebra.vector]
+lfun_key [lemma, in mathcomp.algebra.vector]
+lfun1_neq0 [lemma, in mathcomp.algebra.vector]
+lfun1_poly [lemma, in mathcomp.field.falgebra]
+lift [definition, in mathcomp.ssreflect.fintype]
+lift [definition, in mathcomp.field.closed_field]
+liftK [lemma, in mathcomp.ssreflect.fintype]
+LiftPerm [section, in mathcomp.fingroup.perm]
+LiftPerm.n [variable, in mathcomp.fingroup.perm]
+lift_permV [lemma, in mathcomp.fingroup.perm]
+lift_perm1 [lemma, in mathcomp.fingroup.perm]
+lift_permM [lemma, in mathcomp.fingroup.perm]
+lift_perm_lift [lemma, in mathcomp.fingroup.perm]
+lift_perm_id [lemma, in mathcomp.fingroup.perm]
+lift_perm [definition, in mathcomp.fingroup.perm]
+lift_permK [lemma, in mathcomp.fingroup.perm]
+lift_perm_fun [definition, in mathcomp.fingroup.perm]
+lift_embed [abbreviation, in mathcomp.ssreflect.generic_quotient]
+lift_cst [abbreviation, in mathcomp.ssreflect.generic_quotient]
+lift_op11 [abbreviation, in mathcomp.ssreflect.generic_quotient]
+lift_fun2 [abbreviation, in mathcomp.ssreflect.generic_quotient]
+lift_fun1 [abbreviation, in mathcomp.ssreflect.generic_quotient]
+lift_op2 [abbreviation, in mathcomp.ssreflect.generic_quotient]
+lift_op1 [abbreviation, in mathcomp.ssreflect.generic_quotient]
+lift_max [lemma, in mathcomp.ssreflect.fintype]
+lift_inj [lemma, in mathcomp.ssreflect.fintype]
+lift_subproof [lemma, in mathcomp.ssreflect.fintype]
+lift0 [lemma, in mathcomp.ssreflect.fintype]
+lift0_mx_is_perm [lemma, in mathcomp.algebra.matrix]
+lift0_mx_perm [lemma, in mathcomp.algebra.matrix]
+lift0_mx [definition, in mathcomp.algebra.matrix]
+lift0_perm_eq0 [lemma, in mathcomp.algebra.matrix]
+lift0_permK [lemma, in mathcomp.algebra.matrix]
+lift0_perm_lift [lemma, in mathcomp.algebra.matrix]
+lift0_perm0 [lemma, in mathcomp.algebra.matrix]
+lift0_perm [definition, in mathcomp.algebra.matrix]
+limg [abbreviation, in mathcomp.algebra.vector]
+limgS [lemma, in mathcomp.algebra.vector]
+limg_gal [lemma, in mathcomp.field.galois]
+limg_proj [lemma, in mathcomp.algebra.vector]
+limg_comp [lemma, in mathcomp.algebra.vector]
+limg_ker0 [lemma, in mathcomp.algebra.vector]
+limg_basis_of [lemma, in mathcomp.algebra.vector]
+limg_dim_eq [lemma, in mathcomp.algebra.vector]
+limg_ker_dim [lemma, in mathcomp.algebra.vector]
+limg_ker_compl [lemma, in mathcomp.algebra.vector]
+limg_lfunVK [lemma, in mathcomp.algebra.vector]
+limg_span [lemma, in mathcomp.algebra.vector]
+limg_bigcap [lemma, in mathcomp.algebra.vector]
+limg_cap [lemma, in mathcomp.algebra.vector]
+limg_sum [lemma, in mathcomp.algebra.vector]
+limg_add [lemma, in mathcomp.algebra.vector]
+limg_line [lemma, in mathcomp.algebra.vector]
+limg_amulr [lemma, in mathcomp.field.falgebra]
+limg0 [lemma, in mathcomp.algebra.vector]
+lim0g [lemma, in mathcomp.algebra.vector]
+lim1g [lemma, in mathcomp.algebra.vector]
+LinAut [section, in mathcomp.algebra.vector]
+LinAut.f [variable, in mathcomp.algebra.vector]
+LinAut.K [variable, in mathcomp.algebra.vector]
+LinAut.kerf0 [variable, in mathcomp.algebra.vector]
+LinAut.vT [variable, in mathcomp.algebra.vector]
+Linear [section, in mathcomp.algebra.rat]
+Linear [section, in mathcomp.character.character]
+LinearImage [section, in mathcomp.algebra.vector]
+LinearImageComp [section, in mathcomp.algebra.vector]
+LinearImageComp.aT [variable, in mathcomp.algebra.vector]
+LinearImageComp.K [variable, in mathcomp.algebra.vector]
+LinearImageComp.rT [variable, in mathcomp.algebra.vector]
+LinearImageComp.vT [variable, in mathcomp.algebra.vector]
+LinearImage.aT [variable, in mathcomp.algebra.vector]
+LinearImage.K [variable, in mathcomp.algebra.vector]
+LinearImage.rT [variable, in mathcomp.algebra.vector]
+linearMn [lemma, in mathcomp.algebra.ssrint]
+LinearPreimage [section, in mathcomp.algebra.vector]
+LinearPreimage.aT [variable, in mathcomp.algebra.vector]
+LinearPreimage.K [variable, in mathcomp.algebra.vector]
+LinearPreimage.rT [variable, in mathcomp.algebra.vector]
+linear_irr_comp [lemma, in mathcomp.character.mxrepresentation]
+linear_irr [definition, in mathcomp.character.mxrepresentation]
+linear_mxsimple [lemma, in mathcomp.character.mxrepresentation]
+linear_mx_abs_irr [lemma, in mathcomp.character.mxrepresentation]
+linear_of_free [lemma, in mathcomp.algebra.vector]
+linear_char_divr [lemma, in mathcomp.character.character]
+linear_char_key [lemma, in mathcomp.character.character]
+linear_char [definition, in mathcomp.character.character]
+Linear.G [variable, in mathcomp.character.character]
+Linear.gT [variable, in mathcomp.character.character]
+Linear.OneChar [section, in mathcomp.character.character]
+Linear.OneChar.CFxi [variable, in mathcomp.character.character]
+Linear.OneChar.xi [variable, in mathcomp.character.character]
+Linear.OneChar.xiMV [variable, in mathcomp.character.character]
+linfun [definition, in mathcomp.algebra.vector]
+linfun_def [definition, in mathcomp.algebra.vector]
+linfun_is_ahom [lemma, in mathcomp.field.falgebra]
+lin_mul_row_is_linear [lemma, in mathcomp.algebra.matrix]
+lin_mul_row [definition, in mathcomp.algebra.matrix]
+lin_mulmx_is_linear [lemma, in mathcomp.algebra.matrix]
+lin_mulmx [definition, in mathcomp.algebra.matrix]
+lin_mulmxr_is_linear [lemma, in mathcomp.algebra.matrix]
+lin_mulmxr [definition, in mathcomp.algebra.matrix]
+lin_mx [definition, in mathcomp.algebra.matrix]
+lin_char_group [lemma, in mathcomp.character.character]
+lin_irr_der1 [lemma, in mathcomp.character.character]
+lin_Res_IirrE [lemma, in mathcomp.character.character]
+lin_char_der1 [lemma, in mathcomp.character.character]
+lin_char_unitr [lemma, in mathcomp.character.character]
+lin_char_irr [lemma, in mathcomp.character.character]
+lin_charV_conj [lemma, in mathcomp.character.character]
+lin_char_unity_root [lemma, in mathcomp.character.character]
+lin_charX [lemma, in mathcomp.character.character]
+lin_charV [lemma, in mathcomp.character.character]
+lin_char_neq0 [lemma, in mathcomp.character.character]
+lin_char_prod [lemma, in mathcomp.character.character]
+lin_charM [lemma, in mathcomp.character.character]
+lin_charW [lemma, in mathcomp.character.character]
+lin_char1 [lemma, in mathcomp.character.character]
+lin1_mx [definition, in mathcomp.algebra.matrix]
+lin1_mx_key [lemma, in mathcomp.algebra.matrix]
+lker [definition, in mathcomp.algebra.vector]
+lkerE [lemma, in mathcomp.algebra.vector]
+lker_proj [lemma, in mathcomp.algebra.vector]
+lker0P [lemma, in mathcomp.algebra.vector]
+lker0_compfVK [lemma, in mathcomp.algebra.vector]
+lker0_compfK [lemma, in mathcomp.algebra.vector]
+lker0_compKf [lemma, in mathcomp.algebra.vector]
+lker0_compVKf [lemma, in mathcomp.algebra.vector]
+lker0_compfV [lemma, in mathcomp.algebra.vector]
+lker0_lfunVK [lemma, in mathcomp.algebra.vector]
+lker0_limgf [lemma, in mathcomp.algebra.vector]
+lker0_compVf [lemma, in mathcomp.algebra.vector]
+lker0_lfunK [lemma, in mathcomp.algebra.vector]
+lker0_amulr [lemma, in mathcomp.field.falgebra]
+lker0_amull [lemma, in mathcomp.field.falgebra]
+LMod [section, in mathcomp.algebra.ssrint]
+LMod.R [variable, in mathcomp.algebra.ssrint]
+LMod.V [variable, in mathcomp.algebra.ssrint]
+logn [definition, in mathcomp.ssreflect.prime]
+lognE [lemma, in mathcomp.ssreflect.prime]
+lognM [lemma, in mathcomp.ssreflect.prime]
+lognSg [lemma, in mathcomp.fingroup.fingroup]
+lognX [lemma, in mathcomp.ssreflect.prime]
+logn_quotient_cent_cyclic_pgroup [lemma, in mathcomp.solvable.pgroup]
+logn_morphim [lemma, in mathcomp.fingroup.quotient]
+logn_fact [lemma, in mathcomp.ssreflect.binomial]
+logn_part [lemma, in mathcomp.ssreflect.prime]
+logn_count_dvd [lemma, in mathcomp.ssreflect.prime]
+logn_div [lemma, in mathcomp.ssreflect.prime]
+logn_Gauss [lemma, in mathcomp.ssreflect.prime]
+logn_prime [lemma, in mathcomp.ssreflect.prime]
+logn_gt0 [lemma, in mathcomp.ssreflect.prime]
+logn_rec [definition, in mathcomp.ssreflect.prime]
+logn_quotient [lemma, in mathcomp.solvable.abelian]
+logn_le_p_rank [lemma, in mathcomp.solvable.abelian]
+logn_card_GL_p [lemma, in mathcomp.algebra.mxalgebra]
+logn0 [lemma, in mathcomp.ssreflect.prime]
+logn1 [lemma, in mathcomp.ssreflect.prime]
+lone_subgroup_char [lemma, in mathcomp.fingroup.automorphism]
+looping [definition, in mathcomp.ssreflect.path]
+loopingP [lemma, in mathcomp.ssreflect.path]
+looping_uniq [lemma, in mathcomp.ssreflect.path]
+looping_order [lemma, in mathcomp.ssreflect.fingraph]
+LowerCentral [section, in mathcomp.solvable.nilpotent]
+LowerCentral.gT [variable, in mathcomp.solvable.nilpotent]
+lower_central_at [definition, in mathcomp.solvable.nilpotent]
+lower_central_at_rec [definition, in mathcomp.solvable.nilpotent]
+lpreimK [lemma, in mathcomp.algebra.vector]
+lpreimS [lemma, in mathcomp.algebra.vector]
+lpreim_cap_limg [lemma, in mathcomp.algebra.vector]
+lpreim0 [lemma, in mathcomp.algebra.vector]
+lreg_polyZ_eq0 [lemma, in mathcomp.algebra.poly]
+lreg_size [lemma, in mathcomp.algebra.poly]
+lreg_lead0 [lemma, in mathcomp.algebra.poly]
+lreg_lead [lemma, in mathcomp.algebra.poly]
+lshift [definition, in mathcomp.ssreflect.fintype]
+lshift_subproof [lemma, in mathcomp.ssreflect.fintype]
+lshift0 [lemma, in mathcomp.algebra.zmodp]
+lsubmx [definition, in mathcomp.algebra.matrix]
+lsubmx_key [lemma, in mathcomp.algebra.matrix]
+ltC_nat [definition, in mathcomp.field.algC]
+lteNz_nat [definition, in mathcomp.algebra.ssrint]
+ltezN_nat [definition, in mathcomp.algebra.ssrint]
+ltez_natE [definition, in mathcomp.algebra.ssrint]
+ltez_nat [definition, in mathcomp.algebra.ssrint]
+ltmx [definition, in mathcomp.algebra.mxalgebra]
+ltmxE [lemma, in mathcomp.algebra.mxalgebra]
+ltmxEneq [lemma, in mathcomp.algebra.mxalgebra]
+ltmxErank [lemma, in mathcomp.algebra.mxalgebra]
+ltmxW [lemma, in mathcomp.algebra.mxalgebra]
+ltmx_irrefl [lemma, in mathcomp.algebra.mxalgebra]
+ltmx_trans [lemma, in mathcomp.algebra.mxalgebra]
+ltmx_sub_trans [lemma, in mathcomp.algebra.mxalgebra]
+ltmx0 [lemma, in mathcomp.algebra.mxalgebra]
+ltmx1 [lemma, in mathcomp.algebra.mxalgebra]
+ltn [definition, in mathcomp.ssreflect.ssrnat]
+ltngtP [lemma, in mathcomp.ssreflect.ssrnat]
+ltnn [lemma, in mathcomp.ssreflect.ssrnat]
+ltnNge [lemma, in mathcomp.ssreflect.ssrnat]
+LtnNotGeq [constructor, in mathcomp.ssreflect.ssrnat]
+ltnP [lemma, in mathcomp.ssreflect.ssrnat]
+ltnS [lemma, in mathcomp.ssreflect.ssrnat]
+ltnSn [lemma, in mathcomp.ssreflect.ssrnat]
+ltnW [lemma, in mathcomp.ssreflect.ssrnat]
+ltNz_nat [lemma, in mathcomp.algebra.ssrint]
+ltn_log_quotient [lemma, in mathcomp.solvable.pgroup]
+ltn_quotient [lemma, in mathcomp.fingroup.quotient]
+ltn_sorted_uniq_leq [lemma, in mathcomp.ssreflect.path]
+ltn_odd_Frobenius_ker [lemma, in mathcomp.solvable.frobenius]
+ltn_logl [lemma, in mathcomp.ssreflect.prime]
+ltn_log0 [lemma, in mathcomp.ssreflect.prime]
+ltn_pdiv2_prime [lemma, in mathcomp.ssreflect.prime]
+ltn_divRL [lemma, in mathcomp.ssreflect.div]
+ltn_Pdiv [lemma, in mathcomp.ssreflect.div]
+ltn_divLR [lemma, in mathcomp.ssreflect.div]
+ltn_ceil [lemma, in mathcomp.ssreflect.div]
+ltn_pmod [lemma, in mathcomp.ssreflect.div]
+ltn_mod [lemma, in mathcomp.ssreflect.div]
+ltn_size_undup [lemma, in mathcomp.ssreflect.seq]
+ltn_unsplit [lemma, in mathcomp.ssreflect.fintype]
+ltn_ord [lemma, in mathcomp.ssreflect.fintype]
+ltn_leqif [lemma, in mathcomp.ssreflect.ssrnat]
+ltn_sqr [lemma, in mathcomp.ssreflect.ssrnat]
+ltn_Sdouble [lemma, in mathcomp.ssreflect.ssrnat]
+ltn_double [lemma, in mathcomp.ssreflect.ssrnat]
+ltn_exp2r [lemma, in mathcomp.ssreflect.ssrnat]
+ltn_pexp2l [lemma, in mathcomp.ssreflect.ssrnat]
+ltn_exp2l [lemma, in mathcomp.ssreflect.ssrnat]
+ltn_expl [lemma, in mathcomp.ssreflect.ssrnat]
+ltn_mul [lemma, in mathcomp.ssreflect.ssrnat]
+ltn_Pmulr [lemma, in mathcomp.ssreflect.ssrnat]
+ltn_Pmull [lemma, in mathcomp.ssreflect.ssrnat]
+ltn_pmul2r [lemma, in mathcomp.ssreflect.ssrnat]
+ltn_pmul2l [lemma, in mathcomp.ssreflect.ssrnat]
+ltn_mul2r [lemma, in mathcomp.ssreflect.ssrnat]
+ltn_mul2l [lemma, in mathcomp.ssreflect.ssrnat]
+ltn_subRL [lemma, in mathcomp.ssreflect.ssrnat]
+ltn_sub2l [lemma, in mathcomp.ssreflect.ssrnat]
+ltn_sub2r [lemma, in mathcomp.ssreflect.ssrnat]
+ltn_addl [lemma, in mathcomp.ssreflect.ssrnat]
+ltn_addr [lemma, in mathcomp.ssreflect.ssrnat]
+ltn_add2r [lemma, in mathcomp.ssreflect.ssrnat]
+ltn_add2l [lemma, in mathcomp.ssreflect.ssrnat]
+ltn_xor_geq [inductive, in mathcomp.ssreflect.ssrnat]
+ltn_trans [lemma, in mathcomp.ssreflect.ssrnat]
+ltn_neqAle [lemma, in mathcomp.ssreflect.ssrnat]
+ltn_eqF [lemma, in mathcomp.ssreflect.ssrnat]
+ltn_predK [lemma, in mathcomp.ssreflect.ssrnat]
+ltn_morphim [lemma, in mathcomp.fingroup.morphism]
+ltn0 [lemma, in mathcomp.ssreflect.ssrnat]
+ltn0Sn [lemma, in mathcomp.ssreflect.ssrnat]
+ltP [lemma, in mathcomp.ssreflect.ssrnat]
+ltrq0 [lemma, in mathcomp.algebra.rat]
+ltrz0 [lemma, in mathcomp.algebra.ssrint]
+ltrz1 [lemma, in mathcomp.algebra.ssrint]
+ltr_rat [lemma, in mathcomp.algebra.rat]
+ltr_in_itv [lemma, in mathcomp.algebra.interval]
+ltr_nexpz2r [lemma, in mathcomp.algebra.ssrint]
+ltr_pexpz2r [lemma, in mathcomp.algebra.ssrint]
+ltr_eexpz2l [lemma, in mathcomp.algebra.ssrint]
+ltr_niexpz2l [lemma, in mathcomp.algebra.ssrint]
+ltr_piexpz2l [lemma, in mathcomp.algebra.ssrint]
+ltr_int [lemma, in mathcomp.algebra.ssrint]
+ltr_nmulz2l [lemma, in mathcomp.algebra.ssrint]
+ltr_pmulz2l [lemma, in mathcomp.algebra.ssrint]
+ltr_nmulz2r [lemma, in mathcomp.algebra.ssrint]
+ltr_pmulz2r [lemma, in mathcomp.algebra.ssrint]
+ltr0q [lemma, in mathcomp.algebra.rat]
+ltr0z [lemma, in mathcomp.algebra.ssrint]
+ltr0_sgz [lemma, in mathcomp.algebra.ssrint]
+ltr1z [lemma, in mathcomp.algebra.ssrint]
+ltzN_nat [lemma, in mathcomp.algebra.ssrint]
+ltz_divRL [lemma, in mathcomp.algebra.intdiv]
+ltz_divLR [lemma, in mathcomp.algebra.intdiv]
+ltz_ceil [lemma, in mathcomp.algebra.intdiv]
+ltz_mod [lemma, in mathcomp.algebra.intdiv]
+ltz_pmod [lemma, in mathcomp.algebra.intdiv]
+ltz_addr1 [lemma, in mathcomp.algebra.ssrint]
+ltz_add1r [lemma, in mathcomp.algebra.ssrint]
+ltz_nat [lemma, in mathcomp.algebra.ssrint]
+ltz0_abs [lemma, in mathcomp.algebra.ssrint]
+lt_rat_def [lemma, in mathcomp.algebra.rat]
+lt_rat0 [lemma, in mathcomp.algebra.rat]
+lt_rat [definition, in mathcomp.algebra.rat]
+lt_irrelevance [lemma, in mathcomp.ssreflect.ssrnat]
+lt_size_deriv [lemma, in mathcomp.algebra.poly]
+lt_sizeT [definition, in mathcomp.field.closed_field]
+lt_eqmx [lemma, in mathcomp.algebra.mxalgebra]
+lt0b [lemma, in mathcomp.ssreflect.ssrnat]
+lt0mx [lemma, in mathcomp.algebra.mxalgebra]
+lt0n [lemma, in mathcomp.ssreflect.ssrnat]
+lt0n_neq0 [lemma, in mathcomp.ssreflect.ssrnat]
+lt1mx [lemma, in mathcomp.algebra.mxalgebra]
+LUP_card_GL [lemma, in mathcomp.algebra.mxalgebra]
+L_F [abbreviation, in mathcomp.field.fieldext]
+L_iso [lemma, in mathcomp.solvable.burnside_app]
+L0 [abbreviation, in mathcomp.field.fieldext]
+
| 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 | +(23233 entries) | +
| Notation 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 | +(1373 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 | +(213 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 | +(3475 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 | +(89 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 | +(11853 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 | +(359 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 | +(47 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 | +(103 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 | +(266 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 | +(1118 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 | +(691 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 | +(3461 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 | +(185 entries) | +