| 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 | -(23836 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 | -(1409 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 | -(221 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 | -(3574 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 | -(90 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 | -(12096 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 | -(368 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 | -(45 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 | -(107 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 | -(273 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 | -(1140 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 | -(728 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 | -(3596 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 | -(189 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_eq [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_coefDr [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]
-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]
-leqW_nmono_in [lemma, in mathcomp.ssreflect.ssrnat]
-leqW_mono_in [lemma, in mathcomp.ssreflect.ssrnat]
-leqW_nmono [lemma, in mathcomp.ssreflect.ssrnat]
-leqW_mono [lemma, in mathcomp.ssreflect.ssrnat]
-leq_quotient [lemma, in mathcomp.fingroup.quotient]
-leq_bin2l [lemma, in mathcomp.ssreflect.binomial]
-leq_index [lemma, in mathcomp.ssreflect.path]
-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 [abbreviation, 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_nmono_in [lemma, in mathcomp.ssreflect.ssrnat]
-leq_mono_in [lemma, in mathcomp.ssreflect.ssrnat]
-leq_nmono [lemma, in mathcomp.ssreflect.ssrnat]
-leq_mono [lemma, in mathcomp.ssreflect.ssrnat]
-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_gtF [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]
-LersifField [section, in mathcomp.algebra.interval]
-LersifField.b [variable, in mathcomp.algebra.interval]
-LersifField.F [variable, in mathcomp.algebra.interval]
-LersifField.x [variable, in mathcomp.algebra.interval]
-LersifField.y [variable, in mathcomp.algebra.interval]
-LersifField.z [variable, in mathcomp.algebra.interval]
-lersifN [lemma, in mathcomp.algebra.interval]
-lersifNF [lemma, in mathcomp.algebra.interval]
-LersifOrdered [section, in mathcomp.algebra.interval]
-LersifOrdered.b [variable, in mathcomp.algebra.interval]
-LersifOrdered.e [variable, in mathcomp.algebra.interval]
-LersifOrdered.R [variable, in mathcomp.algebra.interval]
-LersifOrdered.x [variable, in mathcomp.algebra.interval]
-LersifOrdered.y [variable, in mathcomp.algebra.interval]
-LersifOrdered.z [variable, in mathcomp.algebra.interval]
-LersifPo [section, in mathcomp.algebra.interval]
-LersifPo.R [variable, in mathcomp.algebra.interval]
-_ <= _ ?< if _ (ring_scope) [notation, 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_ndivr_mull [lemma, in mathcomp.algebra.interval]
-lersif_ndivl_mull [lemma, in mathcomp.algebra.interval]
-lersif_ndivr_mulr [lemma, in mathcomp.algebra.interval]
-lersif_ndivl_mulr [lemma, in mathcomp.algebra.interval]
-lersif_pdivr_mull [lemma, in mathcomp.algebra.interval]
-lersif_pdivl_mull [lemma, in mathcomp.algebra.interval]
-lersif_pdivr_mulr [lemma, in mathcomp.algebra.interval]
-lersif_pdivl_mulr [lemma, in mathcomp.algebra.interval]
-lersif_maxl [lemma, in mathcomp.algebra.interval]
-lersif_maxr [lemma, in mathcomp.algebra.interval]
-lersif_minl [lemma, in mathcomp.algebra.interval]
-lersif_minr [lemma, in mathcomp.algebra.interval]
-lersif_distl [lemma, in mathcomp.algebra.interval]
-lersif_normr [lemma, in mathcomp.algebra.interval]
-lersif_norml [lemma, in mathcomp.algebra.interval]
-lersif_nnormr [lemma, in mathcomp.algebra.interval]
-lersif_nmul2r [lemma, in mathcomp.algebra.interval]
-lersif_nmul2l [lemma, in mathcomp.algebra.interval]
-lersif_pmul2r [lemma, in mathcomp.algebra.interval]
-lersif_pmul2l [lemma, in mathcomp.algebra.interval]
-lersif_imply [lemma, in mathcomp.algebra.interval]
-lersif_orb [lemma, in mathcomp.algebra.interval]
-lersif_andb [lemma, in mathcomp.algebra.interval]
-lersif_sub_addl [definition, in mathcomp.algebra.interval]
-lersif_subr_addl [lemma, in mathcomp.algebra.interval]
-lersif_subl_addl [lemma, in mathcomp.algebra.interval]
-lersif_sub_addr [definition, in mathcomp.algebra.interval]
-lersif_subr_addr [lemma, in mathcomp.algebra.interval]
-lersif_subl_addr [lemma, in mathcomp.algebra.interval]
-lersif_add2 [definition, in mathcomp.algebra.interval]
-lersif_add2r [lemma, in mathcomp.algebra.interval]
-lersif_add2l [lemma, in mathcomp.algebra.interval]
-lersif_oppE [definition, in mathcomp.algebra.interval]
-lersif_opp2 [lemma, in mathcomp.algebra.interval]
-lersif_oppr0 [lemma, in mathcomp.algebra.interval]
-lersif_0oppr [lemma, in mathcomp.algebra.interval]
-lersif_oppr [lemma, in mathcomp.algebra.interval]
-lersif_oppl [lemma, in mathcomp.algebra.interval]
-lersif_anti [lemma, in mathcomp.algebra.interval]
-lersif_trans [lemma, in mathcomp.algebra.interval]
-lersif01 [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_total [lemma, in mathcomp.algebra.interval]
-le_boundl_total [lemma, in mathcomp.algebra.interval]
-le_boundr_anti [lemma, in mathcomp.algebra.interval]
-le_boundl_anti [lemma, in mathcomp.algebra.interval]
-le_boundr_bb [lemma, in mathcomp.algebra.interval]
-le_boundl_bb [lemma, in mathcomp.algebra.interval]
-le_boundr_trans [lemma, in mathcomp.algebra.interval]
-le_boundl_trans [lemma, in mathcomp.algebra.interval]
-le_boundr_refl [lemma, in mathcomp.algebra.interval]
-le_boundl_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_eqMixin [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]
-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]
-ltnW_nhomo_in [lemma, in mathcomp.ssreflect.ssrnat]
-ltnW_homo_in [lemma, in mathcomp.ssreflect.ssrnat]
-ltnW_nhomo [lemma, in mathcomp.ssreflect.ssrnat]
-ltnW_homo [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_index [lemma, in mathcomp.ssreflect.path]
-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_geF [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]
-ltrW_lersif [lemma, in mathcomp.algebra.interval]
-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_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 | -(23836 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 | -(1409 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 | -(221 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 | -(3574 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 | -(90 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 | -(12096 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 | -(368 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 | -(45 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 | -(107 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 | -(273 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 | -(1140 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 | -(728 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 | -(3596 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 | -(189 entries) | -