| 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 (lemma)
-Lagrange [in mathcomp.fingroup.fingroup]-LagrangeI [in mathcomp.fingroup.fingroup]
-LagrangeMl [in mathcomp.fingroup.fingroup]
-LagrangeMr [in mathcomp.fingroup.fingroup]
-Lagrange_index [in mathcomp.fingroup.fingroup]
-large_field_PET [in mathcomp.field.separable]
-lastI [in mathcomp.ssreflect.seq]
-lastP [in mathcomp.ssreflect.seq]
-last_traject [in mathcomp.ssreflect.path]
-last_map [in mathcomp.ssreflect.seq]
-last_eq [in mathcomp.ssreflect.seq]
-last_nth [in mathcomp.ssreflect.seq]
-last_ind [in mathcomp.ssreflect.seq]
-last_rcons [in mathcomp.ssreflect.seq]
-last_cat [in mathcomp.ssreflect.seq]
-last_cons [in mathcomp.ssreflect.seq]
-lcmnA [in mathcomp.ssreflect.div]
-lcmnAC [in mathcomp.ssreflect.div]
-lcmnACA [in mathcomp.ssreflect.div]
-lcmnC [in mathcomp.ssreflect.div]
-lcmnCA [in mathcomp.ssreflect.div]
-lcmnMl [in mathcomp.ssreflect.div]
-lcmnMr [in mathcomp.ssreflect.div]
-lcmn_idPl [in mathcomp.ssreflect.div]
-lcmn_idPr [in mathcomp.ssreflect.div]
-lcmn_gt0 [in mathcomp.ssreflect.div]
-lcmn0 [in mathcomp.ssreflect.div]
-lcmn1 [in mathcomp.ssreflect.div]
-lcm0n [in mathcomp.ssreflect.div]
-lcm1n [in mathcomp.ssreflect.div]
-lcnE [in mathcomp.solvable.nilpotent]
-lcnP [in mathcomp.solvable.nilpotent]
-lcnS [in mathcomp.solvable.nilpotent]
-lcnSn [in mathcomp.solvable.nilpotent]
-lcnSnS [in mathcomp.solvable.nilpotent]
-lcn_cont [in mathcomp.solvable.nilpotent]
-lcn_nil_classP [in mathcomp.solvable.nilpotent]
-lcn_bigdprod [in mathcomp.solvable.nilpotent]
-lcn_bigcprod [in mathcomp.solvable.nilpotent]
-lcn_dprod [in mathcomp.solvable.nilpotent]
-lcn_cprod [in mathcomp.solvable.nilpotent]
-lcn_sub_leq [in mathcomp.solvable.nilpotent]
-lcn_central [in mathcomp.solvable.nilpotent]
-lcn_normalS [in mathcomp.solvable.nilpotent]
-lcn_subS [in mathcomp.solvable.nilpotent]
-lcn_norm [in mathcomp.solvable.nilpotent]
-lcn_sub [in mathcomp.solvable.nilpotent]
-lcn_normal [in mathcomp.solvable.nilpotent]
-lcn_char [in mathcomp.solvable.nilpotent]
-lcn_group_set [in mathcomp.solvable.nilpotent]
-lcn0 [in mathcomp.solvable.nilpotent]
-lcn1 [in mathcomp.solvable.nilpotent]
-lcn2 [in mathcomp.solvable.nilpotent]
-Lcorrect [in mathcomp.solvable.burnside_app]
-lcosetE [in mathcomp.fingroup.fingroup]
-lcosetK [in mathcomp.fingroup.fingroup]
-lcosetKV [in mathcomp.fingroup.fingroup]
-lcosetM [in mathcomp.fingroup.fingroup]
-lcosetP [in mathcomp.fingroup.fingroup]
-lcosetS [in mathcomp.fingroup.fingroup]
-lcosetsP [in mathcomp.fingroup.fingroup]
-lcoset_id [in mathcomp.fingroup.fingroup]
-lcoset_trans [in mathcomp.fingroup.fingroup]
-lcoset_transl [in mathcomp.fingroup.fingroup]
-lcoset_eqP [in mathcomp.fingroup.fingroup]
-lcoset_sym [in mathcomp.fingroup.fingroup]
-lcoset_refl [in mathcomp.fingroup.fingroup]
-lcoset_inj [in mathcomp.fingroup.fingroup]
-lcoset1 [in mathcomp.fingroup.fingroup]
-LdivJ [in mathcomp.solvable.abelian]
-LdivP [in mathcomp.solvable.abelian]
-LdivT_J [in mathcomp.solvable.abelian]
-lead_coef_poly_XaY [in mathcomp.algebra.polyXY]
-lead_coef_map [in mathcomp.algebra.poly]
-lead_coef_comp [in mathcomp.algebra.poly]
-lead_coef_exp [in mathcomp.algebra.poly]
-lead_coefZ [in mathcomp.algebra.poly]
-lead_coefM [in mathcomp.algebra.poly]
-lead_coef_map_eq [in mathcomp.algebra.poly]
-lead_coef_map_inj [in mathcomp.algebra.poly]
-lead_coef_map_id0 [in mathcomp.algebra.poly]
-lead_coef_lreg [in mathcomp.algebra.poly]
-lead_coef_Mmonic [in mathcomp.algebra.poly]
-lead_coef_monicM [in mathcomp.algebra.poly]
-lead_coefXn [in mathcomp.algebra.poly]
-lead_coefMX [in mathcomp.algebra.poly]
-lead_coefXsubC [in mathcomp.algebra.poly]
-lead_coefX [in mathcomp.algebra.poly]
-lead_coef_proper_mul [in mathcomp.algebra.poly]
-lead_coef1 [in mathcomp.algebra.poly]
-lead_coefDr [in mathcomp.algebra.poly]
-lead_coefDl [in mathcomp.algebra.poly]
-lead_coef_opp [in mathcomp.algebra.poly]
-lead_coef_eq0 [in mathcomp.algebra.poly]
-lead_coef0 [in mathcomp.algebra.poly]
-lead_coef_poly [in mathcomp.algebra.poly]
-lead_coefC [in mathcomp.algebra.poly]
-lead_coefE [in mathcomp.algebra.poly]
-left_arc [in mathcomp.ssreflect.path]
-left_trans [in mathcomp.ssreflect.generic_quotient]
-leNz_nat [in mathcomp.algebra.ssrint]
-leP [in mathcomp.ssreflect.ssrnat]
-leqifP [in mathcomp.ssreflect.ssrnat]
-leqif_mul [in mathcomp.ssreflect.ssrnat]
-leqif_add [in mathcomp.ssreflect.ssrnat]
-leqif_eq [in mathcomp.ssreflect.ssrnat]
-leqif_geq [in mathcomp.ssreflect.ssrnat]
-leqif_trans [in mathcomp.ssreflect.ssrnat]
-leqif_refl [in mathcomp.ssreflect.ssrnat]
-leqif_sum [in mathcomp.ssreflect.bigop]
-leqNgt [in mathcomp.ssreflect.ssrnat]
-leqnn [in mathcomp.ssreflect.ssrnat]
-leqnSn [in mathcomp.ssreflect.ssrnat]
-leqn0 [in mathcomp.ssreflect.ssrnat]
-leqP [in mathcomp.ssreflect.ssrnat]
-leqSpred [in mathcomp.ssreflect.ssrnat]
-leqW [in mathcomp.ssreflect.ssrnat]
-leqW_nmono_in [in mathcomp.ssreflect.ssrnat]
-leqW_mono_in [in mathcomp.ssreflect.ssrnat]
-leqW_nmono [in mathcomp.ssreflect.ssrnat]
-leqW_mono [in mathcomp.ssreflect.ssrnat]
-leq_quotient [in mathcomp.fingroup.quotient]
-leq_bin2l [in mathcomp.ssreflect.binomial]
-leq_index [in mathcomp.ssreflect.path]
-leq_divLR [in mathcomp.ssreflect.div]
-leq_divDl [in mathcomp.ssreflect.div]
-leq_div2l [in mathcomp.ssreflect.div]
-leq_div2r [in mathcomp.ssreflect.div]
-leq_divRL [in mathcomp.ssreflect.div]
-leq_div [in mathcomp.ssreflect.div]
-leq_mod [in mathcomp.ssreflect.div]
-leq_trunc_div [in mathcomp.ssreflect.div]
-leq_size_uniq [in mathcomp.ssreflect.seq]
-leq_ord [in mathcomp.ssreflect.fintype]
-leq_bump2 [in mathcomp.ssreflect.fintype]
-leq_bump [in mathcomp.ssreflect.fintype]
-leq_image_card [in mathcomp.ssreflect.fintype]
-leq_nmono_in [in mathcomp.ssreflect.ssrnat]
-leq_mono_in [in mathcomp.ssreflect.ssrnat]
-leq_nmono [in mathcomp.ssreflect.ssrnat]
-leq_mono [in mathcomp.ssreflect.ssrnat]
-leq_sqr [in mathcomp.ssreflect.ssrnat]
-leq_Sdouble [in mathcomp.ssreflect.ssrnat]
-leq_double [in mathcomp.ssreflect.ssrnat]
-leq_b1 [in mathcomp.ssreflect.ssrnat]
-leq_exp2r [in mathcomp.ssreflect.ssrnat]
-leq_pexp2l [in mathcomp.ssreflect.ssrnat]
-leq_exp2l [in mathcomp.ssreflect.ssrnat]
-leq_pmul2r [in mathcomp.ssreflect.ssrnat]
-leq_pmul2l [in mathcomp.ssreflect.ssrnat]
-leq_mul [in mathcomp.ssreflect.ssrnat]
-leq_mul2r [in mathcomp.ssreflect.ssrnat]
-leq_mul2l [in mathcomp.ssreflect.ssrnat]
-leq_pmulr [in mathcomp.ssreflect.ssrnat]
-leq_pmull [in mathcomp.ssreflect.ssrnat]
-leq_min [in mathcomp.ssreflect.ssrnat]
-leq_maxr [in mathcomp.ssreflect.ssrnat]
-leq_maxl [in mathcomp.ssreflect.ssrnat]
-leq_max [in mathcomp.ssreflect.ssrnat]
-leq_sub [in mathcomp.ssreflect.ssrnat]
-leq_sub2l [in mathcomp.ssreflect.ssrnat]
-leq_sub2r [in mathcomp.ssreflect.ssrnat]
-leq_subr [in mathcomp.ssreflect.ssrnat]
-leq_subLR [in mathcomp.ssreflect.ssrnat]
-leq_addl [in mathcomp.ssreflect.ssrnat]
-leq_addr [in mathcomp.ssreflect.ssrnat]
-leq_add [in mathcomp.ssreflect.ssrnat]
-leq_add2r [in mathcomp.ssreflect.ssrnat]
-leq_add2l [in mathcomp.ssreflect.ssrnat]
-leq_total [in mathcomp.ssreflect.ssrnat]
-leq_ltn_trans [in mathcomp.ssreflect.ssrnat]
-leq_trans [in mathcomp.ssreflect.ssrnat]
-leq_eqVlt [in mathcomp.ssreflect.ssrnat]
-leq_gtF [in mathcomp.ssreflect.ssrnat]
-leq_pred [in mathcomp.ssreflect.ssrnat]
-leq_sizeP [in mathcomp.algebra.poly]
-leq_bigmax [in mathcomp.ssreflect.bigop]
-leq_bigmax_cond [in mathcomp.ssreflect.bigop]
-leq_sum [in mathcomp.ssreflect.bigop]
-leq_homg [in mathcomp.fingroup.morphism]
-leq_morphim [in mathcomp.fingroup.morphism]
-leq_card_cover [in mathcomp.ssreflect.finset]
-leq_card_setU [in mathcomp.ssreflect.finset]
-leq_imset_card [in mathcomp.ssreflect.finset]
-leq0n [in mathcomp.ssreflect.ssrnat]
-lerq0 [in mathcomp.algebra.rat]
-lersifF [in mathcomp.algebra.interval]
-lersifN [in mathcomp.algebra.interval]
-lersifNF [in mathcomp.algebra.interval]
-lersifS [in mathcomp.algebra.interval]
-lersifT [in mathcomp.algebra.interval]
-lersifW [in mathcomp.algebra.interval]
-lersifxx [in mathcomp.algebra.interval]
-lersif_in_itv [in mathcomp.algebra.interval]
-lersif_ndivr_mull [in mathcomp.algebra.interval]
-lersif_ndivl_mull [in mathcomp.algebra.interval]
-lersif_ndivr_mulr [in mathcomp.algebra.interval]
-lersif_ndivl_mulr [in mathcomp.algebra.interval]
-lersif_pdivr_mull [in mathcomp.algebra.interval]
-lersif_pdivl_mull [in mathcomp.algebra.interval]
-lersif_pdivr_mulr [in mathcomp.algebra.interval]
-lersif_pdivl_mulr [in mathcomp.algebra.interval]
-lersif_maxl [in mathcomp.algebra.interval]
-lersif_maxr [in mathcomp.algebra.interval]
-lersif_minl [in mathcomp.algebra.interval]
-lersif_minr [in mathcomp.algebra.interval]
-lersif_distl [in mathcomp.algebra.interval]
-lersif_normr [in mathcomp.algebra.interval]
-lersif_norml [in mathcomp.algebra.interval]
-lersif_nnormr [in mathcomp.algebra.interval]
-lersif_nmul2r [in mathcomp.algebra.interval]
-lersif_nmul2l [in mathcomp.algebra.interval]
-lersif_pmul2r [in mathcomp.algebra.interval]
-lersif_pmul2l [in mathcomp.algebra.interval]
-lersif_imply [in mathcomp.algebra.interval]
-lersif_orb [in mathcomp.algebra.interval]
-lersif_andb [in mathcomp.algebra.interval]
-lersif_subr_addl [in mathcomp.algebra.interval]
-lersif_subl_addl [in mathcomp.algebra.interval]
-lersif_subr_addr [in mathcomp.algebra.interval]
-lersif_subl_addr [in mathcomp.algebra.interval]
-lersif_add2r [in mathcomp.algebra.interval]
-lersif_add2l [in mathcomp.algebra.interval]
-lersif_opp2 [in mathcomp.algebra.interval]
-lersif_oppr0 [in mathcomp.algebra.interval]
-lersif_0oppr [in mathcomp.algebra.interval]
-lersif_oppr [in mathcomp.algebra.interval]
-lersif_oppl [in mathcomp.algebra.interval]
-lersif_anti [in mathcomp.algebra.interval]
-lersif_trans [in mathcomp.algebra.interval]
-lersif01 [in mathcomp.algebra.interval]
-lerz0 [in mathcomp.algebra.ssrint]
-lerz1 [in mathcomp.algebra.ssrint]
-ler_rat [in mathcomp.algebra.rat]
-ler_in_itv [in mathcomp.algebra.interval]
-ler_nexpz2r [in mathcomp.algebra.ssrint]
-ler_pexpz2r [in mathcomp.algebra.ssrint]
-ler_wnexpz2r [in mathcomp.algebra.ssrint]
-ler_wpexpz2r [in mathcomp.algebra.ssrint]
-ler_eexpz2l [in mathcomp.algebra.ssrint]
-ler_niexpz2l [in mathcomp.algebra.ssrint]
-ler_piexpz2l [in mathcomp.algebra.ssrint]
-ler_weexpz2l [in mathcomp.algebra.ssrint]
-ler_wneexpz2l [in mathcomp.algebra.ssrint]
-ler_wpeexpz2l [in mathcomp.algebra.ssrint]
-ler_wniexpz2l [in mathcomp.algebra.ssrint]
-ler_wpiexpz2l [in mathcomp.algebra.ssrint]
-ler_int [in mathcomp.algebra.ssrint]
-ler_nmulz2l [in mathcomp.algebra.ssrint]
-ler_pmulz2l [in mathcomp.algebra.ssrint]
-ler_wnmulz2l [in mathcomp.algebra.ssrint]
-ler_wpmulz2l [in mathcomp.algebra.ssrint]
-ler_wnmulz2r [in mathcomp.algebra.ssrint]
-ler_wpmulz2r [in mathcomp.algebra.ssrint]
-ler_nmulz2r [in mathcomp.algebra.ssrint]
-ler_pmulz2r [in mathcomp.algebra.ssrint]
-ler0q [in mathcomp.algebra.rat]
-ler0z [in mathcomp.algebra.ssrint]
-ler1z [in mathcomp.algebra.ssrint]
-lezN_nat [in mathcomp.algebra.ssrint]
-lez_divLR [in mathcomp.algebra.intdiv]
-lez_divRL [in mathcomp.algebra.intdiv]
-lez_div [in mathcomp.algebra.intdiv]
-lez_floor [in mathcomp.algebra.intdiv]
-lez_addr1 [in mathcomp.algebra.ssrint]
-lez_add1r [in mathcomp.algebra.ssrint]
-lez_nat [in mathcomp.algebra.ssrint]
-lez0_abs [in mathcomp.algebra.ssrint]
-lez0_nat [in mathcomp.algebra.ssrint]
-le_rat_total [in mathcomp.algebra.rat]
-le_rat0_anti [in mathcomp.algebra.rat]
-le_rat0M [in mathcomp.algebra.rat]
-le_rat0D [in mathcomp.algebra.rat]
-le_rat0 [in mathcomp.algebra.rat]
-le_boundr_total [in mathcomp.algebra.interval]
-le_boundl_total [in mathcomp.algebra.interval]
-le_boundr_anti [in mathcomp.algebra.interval]
-le_boundl_anti [in mathcomp.algebra.interval]
-le_boundr_bb [in mathcomp.algebra.interval]
-le_boundl_bb [in mathcomp.algebra.interval]
-le_boundr_trans [in mathcomp.algebra.interval]
-le_boundl_trans [in mathcomp.algebra.interval]
-le_boundr_refl [in mathcomp.algebra.interval]
-le_boundl_refl [in mathcomp.algebra.interval]
-le_irrelevance [in mathcomp.ssreflect.ssrnat]
-le0z_nat [in mathcomp.algebra.ssrint]
-lfunE [in mathcomp.algebra.vector]
-lfunP [in mathcomp.algebra.vector]
-lfunPn [in mathcomp.algebra.vector]
-lfun_vect_iso [in mathcomp.algebra.vector]
-lfun_scaleDl [in mathcomp.algebra.vector]
-lfun_scaleDr [in mathcomp.algebra.vector]
-lfun_scale1 [in mathcomp.algebra.vector]
-lfun_scaleA [in mathcomp.algebra.vector]
-lfun_addN [in mathcomp.algebra.vector]
-lfun_add0 [in mathcomp.algebra.vector]
-lfun_addC [in mathcomp.algebra.vector]
-lfun_addA [in mathcomp.algebra.vector]
-lfun_is_linear [in mathcomp.algebra.vector]
-lfun_img_key [in mathcomp.algebra.vector]
-lfun_key [in mathcomp.algebra.vector]
-lfun1_neq0 [in mathcomp.algebra.vector]
-lfun1_poly [in mathcomp.field.falgebra]
-liftK [in mathcomp.ssreflect.fintype]
-lift_permV [in mathcomp.fingroup.perm]
-lift_perm1 [in mathcomp.fingroup.perm]
-lift_permM [in mathcomp.fingroup.perm]
-lift_perm_lift [in mathcomp.fingroup.perm]
-lift_perm_id [in mathcomp.fingroup.perm]
-lift_permK [in mathcomp.fingroup.perm]
-lift_max [in mathcomp.ssreflect.fintype]
-lift_inj [in mathcomp.ssreflect.fintype]
-lift_subproof [in mathcomp.ssreflect.fintype]
-lift0 [in mathcomp.ssreflect.fintype]
-lift0_mx_is_perm [in mathcomp.algebra.matrix]
-lift0_mx_perm [in mathcomp.algebra.matrix]
-lift0_perm_eq0 [in mathcomp.algebra.matrix]
-lift0_permK [in mathcomp.algebra.matrix]
-lift0_perm_lift [in mathcomp.algebra.matrix]
-lift0_perm0 [in mathcomp.algebra.matrix]
-limgS [in mathcomp.algebra.vector]
-limg_gal [in mathcomp.field.galois]
-limg_proj [in mathcomp.algebra.vector]
-limg_comp [in mathcomp.algebra.vector]
-limg_ker0 [in mathcomp.algebra.vector]
-limg_basis_of [in mathcomp.algebra.vector]
-limg_dim_eq [in mathcomp.algebra.vector]
-limg_ker_dim [in mathcomp.algebra.vector]
-limg_ker_compl [in mathcomp.algebra.vector]
-limg_lfunVK [in mathcomp.algebra.vector]
-limg_span [in mathcomp.algebra.vector]
-limg_bigcap [in mathcomp.algebra.vector]
-limg_cap [in mathcomp.algebra.vector]
-limg_sum [in mathcomp.algebra.vector]
-limg_add [in mathcomp.algebra.vector]
-limg_line [in mathcomp.algebra.vector]
-limg_amulr [in mathcomp.field.falgebra]
-limg0 [in mathcomp.algebra.vector]
-lim0g [in mathcomp.algebra.vector]
-lim1g [in mathcomp.algebra.vector]
-linearMn [in mathcomp.algebra.ssrint]
-linear_irr_comp [in mathcomp.character.mxrepresentation]
-linear_mxsimple [in mathcomp.character.mxrepresentation]
-linear_mx_abs_irr [in mathcomp.character.mxrepresentation]
-linear_of_free [in mathcomp.algebra.vector]
-linear_char_divr [in mathcomp.character.character]
-linear_char_key [in mathcomp.character.character]
-linfun_is_ahom [in mathcomp.field.falgebra]
-lin_mul_row_is_linear [in mathcomp.algebra.matrix]
-lin_mulmx_is_linear [in mathcomp.algebra.matrix]
-lin_mulmxr_is_linear [in mathcomp.algebra.matrix]
-lin_char_group [in mathcomp.character.character]
-lin_irr_der1 [in mathcomp.character.character]
-lin_Res_IirrE [in mathcomp.character.character]
-lin_char_der1 [in mathcomp.character.character]
-lin_char_unitr [in mathcomp.character.character]
-lin_char_irr [in mathcomp.character.character]
-lin_charV_conj [in mathcomp.character.character]
-lin_char_unity_root [in mathcomp.character.character]
-lin_charX [in mathcomp.character.character]
-lin_charV [in mathcomp.character.character]
-lin_char_neq0 [in mathcomp.character.character]
-lin_char_prod [in mathcomp.character.character]
-lin_charM [in mathcomp.character.character]
-lin_charW [in mathcomp.character.character]
-lin_char1 [in mathcomp.character.character]
-lin1_mx_key [in mathcomp.algebra.matrix]
-lkerE [in mathcomp.algebra.vector]
-lker_proj [in mathcomp.algebra.vector]
-lker0P [in mathcomp.algebra.vector]
-lker0_compfVK [in mathcomp.algebra.vector]
-lker0_compfK [in mathcomp.algebra.vector]
-lker0_compKf [in mathcomp.algebra.vector]
-lker0_compVKf [in mathcomp.algebra.vector]
-lker0_compfV [in mathcomp.algebra.vector]
-lker0_lfunVK [in mathcomp.algebra.vector]
-lker0_limgf [in mathcomp.algebra.vector]
-lker0_compVf [in mathcomp.algebra.vector]
-lker0_lfunK [in mathcomp.algebra.vector]
-lker0_amulr [in mathcomp.field.falgebra]
-lker0_amull [in mathcomp.field.falgebra]
-lognE [in mathcomp.ssreflect.prime]
-lognM [in mathcomp.ssreflect.prime]
-lognSg [in mathcomp.fingroup.fingroup]
-lognX [in mathcomp.ssreflect.prime]
-logn_quotient_cent_cyclic_pgroup [in mathcomp.solvable.pgroup]
-logn_morphim [in mathcomp.fingroup.quotient]
-logn_fact [in mathcomp.ssreflect.binomial]
-logn_part [in mathcomp.ssreflect.prime]
-logn_count_dvd [in mathcomp.ssreflect.prime]
-logn_div [in mathcomp.ssreflect.prime]
-logn_Gauss [in mathcomp.ssreflect.prime]
-logn_prime [in mathcomp.ssreflect.prime]
-logn_gt0 [in mathcomp.ssreflect.prime]
-logn_quotient [in mathcomp.solvable.abelian]
-logn_le_p_rank [in mathcomp.solvable.abelian]
-logn_card_GL_p [in mathcomp.algebra.mxalgebra]
-logn0 [in mathcomp.ssreflect.prime]
-logn1 [in mathcomp.ssreflect.prime]
-lone_subgroup_char [in mathcomp.fingroup.automorphism]
-loopingP [in mathcomp.ssreflect.path]
-looping_uniq [in mathcomp.ssreflect.path]
-looping_order [in mathcomp.ssreflect.fingraph]
-lpreimK [in mathcomp.algebra.vector]
-lpreimS [in mathcomp.algebra.vector]
-lpreim_cap_limg [in mathcomp.algebra.vector]
-lpreim0 [in mathcomp.algebra.vector]
-lreg_polyZ_eq0 [in mathcomp.algebra.poly]
-lreg_size [in mathcomp.algebra.poly]
-lreg_lead0 [in mathcomp.algebra.poly]
-lreg_lead [in mathcomp.algebra.poly]
-lshift_subproof [in mathcomp.ssreflect.fintype]
-lshift0 [in mathcomp.algebra.zmodp]
-lsubmx_key [in mathcomp.algebra.matrix]
-ltmxE [in mathcomp.algebra.mxalgebra]
-ltmxEneq [in mathcomp.algebra.mxalgebra]
-ltmxErank [in mathcomp.algebra.mxalgebra]
-ltmxW [in mathcomp.algebra.mxalgebra]
-ltmx_irrefl [in mathcomp.algebra.mxalgebra]
-ltmx_trans [in mathcomp.algebra.mxalgebra]
-ltmx_sub_trans [in mathcomp.algebra.mxalgebra]
-ltmx0 [in mathcomp.algebra.mxalgebra]
-ltmx1 [in mathcomp.algebra.mxalgebra]
-ltngtP [in mathcomp.ssreflect.ssrnat]
-ltnn [in mathcomp.ssreflect.ssrnat]
-ltnNge [in mathcomp.ssreflect.ssrnat]
-ltnP [in mathcomp.ssreflect.ssrnat]
-ltnS [in mathcomp.ssreflect.ssrnat]
-ltnSn [in mathcomp.ssreflect.ssrnat]
-ltnW [in mathcomp.ssreflect.ssrnat]
-ltnW_nhomo_in [in mathcomp.ssreflect.ssrnat]
-ltnW_homo_in [in mathcomp.ssreflect.ssrnat]
-ltnW_nhomo [in mathcomp.ssreflect.ssrnat]
-ltnW_homo [in mathcomp.ssreflect.ssrnat]
-ltNz_nat [in mathcomp.algebra.ssrint]
-ltn_log_quotient [in mathcomp.solvable.pgroup]
-ltn_quotient [in mathcomp.fingroup.quotient]
-ltn_index [in mathcomp.ssreflect.path]
-ltn_sorted_uniq_leq [in mathcomp.ssreflect.path]
-ltn_odd_Frobenius_ker [in mathcomp.solvable.frobenius]
-ltn_logl [in mathcomp.ssreflect.prime]
-ltn_log0 [in mathcomp.ssreflect.prime]
-ltn_pdiv2_prime [in mathcomp.ssreflect.prime]
-ltn_divRL [in mathcomp.ssreflect.div]
-ltn_Pdiv [in mathcomp.ssreflect.div]
-ltn_divLR [in mathcomp.ssreflect.div]
-ltn_ceil [in mathcomp.ssreflect.div]
-ltn_pmod [in mathcomp.ssreflect.div]
-ltn_mod [in mathcomp.ssreflect.div]
-ltn_size_undup [in mathcomp.ssreflect.seq]
-ltn_unsplit [in mathcomp.ssreflect.fintype]
-ltn_ord [in mathcomp.ssreflect.fintype]
-ltn_leqif [in mathcomp.ssreflect.ssrnat]
-ltn_sqr [in mathcomp.ssreflect.ssrnat]
-ltn_Sdouble [in mathcomp.ssreflect.ssrnat]
-ltn_double [in mathcomp.ssreflect.ssrnat]
-ltn_exp2r [in mathcomp.ssreflect.ssrnat]
-ltn_pexp2l [in mathcomp.ssreflect.ssrnat]
-ltn_exp2l [in mathcomp.ssreflect.ssrnat]
-ltn_expl [in mathcomp.ssreflect.ssrnat]
-ltn_mul [in mathcomp.ssreflect.ssrnat]
-ltn_Pmulr [in mathcomp.ssreflect.ssrnat]
-ltn_Pmull [in mathcomp.ssreflect.ssrnat]
-ltn_pmul2r [in mathcomp.ssreflect.ssrnat]
-ltn_pmul2l [in mathcomp.ssreflect.ssrnat]
-ltn_mul2r [in mathcomp.ssreflect.ssrnat]
-ltn_mul2l [in mathcomp.ssreflect.ssrnat]
-ltn_subRL [in mathcomp.ssreflect.ssrnat]
-ltn_sub2l [in mathcomp.ssreflect.ssrnat]
-ltn_sub2r [in mathcomp.ssreflect.ssrnat]
-ltn_addl [in mathcomp.ssreflect.ssrnat]
-ltn_addr [in mathcomp.ssreflect.ssrnat]
-ltn_add2r [in mathcomp.ssreflect.ssrnat]
-ltn_add2l [in mathcomp.ssreflect.ssrnat]
-ltn_trans [in mathcomp.ssreflect.ssrnat]
-ltn_neqAle [in mathcomp.ssreflect.ssrnat]
-ltn_geF [in mathcomp.ssreflect.ssrnat]
-ltn_eqF [in mathcomp.ssreflect.ssrnat]
-ltn_predK [in mathcomp.ssreflect.ssrnat]
-ltn_morphim [in mathcomp.fingroup.morphism]
-ltn0 [in mathcomp.ssreflect.ssrnat]
-ltn0Sn [in mathcomp.ssreflect.ssrnat]
-ltP [in mathcomp.ssreflect.ssrnat]
-ltrq0 [in mathcomp.algebra.rat]
-ltrW_lersif [in mathcomp.algebra.interval]
-ltrz0 [in mathcomp.algebra.ssrint]
-ltrz1 [in mathcomp.algebra.ssrint]
-ltr_rat [in mathcomp.algebra.rat]
-ltr_in_itv [in mathcomp.algebra.interval]
-ltr_nexpz2r [in mathcomp.algebra.ssrint]
-ltr_pexpz2r [in mathcomp.algebra.ssrint]
-ltr_eexpz2l [in mathcomp.algebra.ssrint]
-ltr_niexpz2l [in mathcomp.algebra.ssrint]
-ltr_piexpz2l [in mathcomp.algebra.ssrint]
-ltr_int [in mathcomp.algebra.ssrint]
-ltr_nmulz2l [in mathcomp.algebra.ssrint]
-ltr_pmulz2l [in mathcomp.algebra.ssrint]
-ltr_nmulz2r [in mathcomp.algebra.ssrint]
-ltr_pmulz2r [in mathcomp.algebra.ssrint]
-ltr0q [in mathcomp.algebra.rat]
-ltr0z [in mathcomp.algebra.ssrint]
-ltr0_sgz [in mathcomp.algebra.ssrint]
-ltr1z [in mathcomp.algebra.ssrint]
-ltzN_nat [in mathcomp.algebra.ssrint]
-ltz_divRL [in mathcomp.algebra.intdiv]
-ltz_divLR [in mathcomp.algebra.intdiv]
-ltz_ceil [in mathcomp.algebra.intdiv]
-ltz_mod [in mathcomp.algebra.intdiv]
-ltz_pmod [in mathcomp.algebra.intdiv]
-ltz_addr1 [in mathcomp.algebra.ssrint]
-ltz_add1r [in mathcomp.algebra.ssrint]
-ltz_nat [in mathcomp.algebra.ssrint]
-ltz0_abs [in mathcomp.algebra.ssrint]
-lt_rat_def [in mathcomp.algebra.rat]
-lt_rat0 [in mathcomp.algebra.rat]
-lt_irrelevance [in mathcomp.ssreflect.ssrnat]
-lt_size_deriv [in mathcomp.algebra.poly]
-lt_eqmx [in mathcomp.algebra.mxalgebra]
-lt0b [in mathcomp.ssreflect.ssrnat]
-lt0mx [in mathcomp.algebra.mxalgebra]
-lt0n [in mathcomp.ssreflect.ssrnat]
-lt0n_neq0 [in mathcomp.ssreflect.ssrnat]
-lt1mx [in mathcomp.algebra.mxalgebra]
-LUP_card_GL [in mathcomp.algebra.mxalgebra]
-L_iso [in mathcomp.solvable.burnside_app]
-
| 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) | -