L (Global Index)
| Files | 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 | _ |
| Definitions | 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 | _ |
| Lemmas | 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 | _ |
| Abbreviations | 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 | _ |
| 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 | _ |
| Notations |
L
L0 [abbrev, in mathcomp.field.fieldext]L0 [abbrev, in mathcomp.field.fieldext]
l0 [abbrev, in mathcomp.algebra.matrix]
L_F [abbrev, in mathcomp.field.fieldext]
L_iso [prf, in mathcomp.solvable.burnside_app]
Lagrange [prf, in mathcomp.finite_group.fingroup]
lagrange [def, in mathcomp.algebra.qpoly]
lagrange_ [abbrev, in mathcomp.algebra.qpoly]
lagrange_coords [prf, in mathcomp.algebra.qpoly]
lagrange_def [abbrev, in mathcomp.algebra.qpoly]
lagrange_free [prf, in mathcomp.algebra.qpoly]
lagrange_full [prf, in mathcomp.algebra.qpoly]
lagrange_gen [prf, in mathcomp.algebra.qpoly]
Lagrange_index [prf, in mathcomp.finite_group.fingroup]
lagrange_key [prf, in mathcomp.algebra.qpoly]
lagrange_sample [prf, in mathcomp.algebra.qpoly]
lagrangeE [prf, in mathcomp.algebra.qpoly]
LagrangeI [prf, in mathcomp.finite_group.fingroup]
LagrangeMl [prf, in mathcomp.finite_group.fingroup]
LagrangeMr [prf, in mathcomp.finite_group.fingroup]
lalgType [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
large_field_PET [prf, in mathcomp.field.separable]
last [def, in mathcomp.boot.seq]
last_cat [prf, in mathcomp.boot.seq]
last_cons [prf, in mathcomp.boot.seq]
last_drop [prf, in mathcomp.boot.seq]
last_eq [prf, in mathcomp.boot.seq]
last_ind [prf, in mathcomp.boot.seq]
last_map [prf, in mathcomp.boot.seq]
last_nth [prf, in mathcomp.boot.seq]
last_rcons [prf, in mathcomp.boot.seq]
last_spec [ind, in mathcomp.boot.seq]
last_take [prf, in mathcomp.boot.seq]
last_traject [prf, in mathcomp.boot.path]
lastI [prf, in mathcomp.boot.seq]
LastNil [constr, in mathcomp.boot.seq]
lastP [prf, in mathcomp.boot.seq]
LastRcons [constr, in mathcomp.boot.seq]
lcm0n [prf, in mathcomp.boot.div]
lcm0z [prf, in mathcomp.algebra.intdiv]
lcm1n [prf, in mathcomp.boot.div]
lcmn [def, in mathcomp.boot.div]
lcmn0 [prf, in mathcomp.boot.div]
lcmn1 [prf, in mathcomp.boot.div]
lcmn_gt0 [prf, in mathcomp.boot.div]
lcmn_idPl [prf, in mathcomp.boot.div]
lcmn_idPr [prf, in mathcomp.boot.div]
lcmnA [prf, in mathcomp.boot.div]
lcmnAC [prf, in mathcomp.boot.div]
lcmnACA [prf, in mathcomp.boot.div]
lcmnC [prf, in mathcomp.boot.div]
lcmnCA [prf, in mathcomp.boot.div]
lcmnMl [prf, in mathcomp.boot.div]
lcmnMr [prf, in mathcomp.boot.div]
lcmz [def, in mathcomp.algebra.intdiv]
lcmz0 [prf, in mathcomp.algebra.intdiv]
lcmz_ge0 [prf, in mathcomp.algebra.intdiv]
lcmz_neq0 [prf, in mathcomp.algebra.intdiv]
lcmzC [prf, in mathcomp.algebra.intdiv]
lcn0 [prf, in mathcomp.solvable.nilpotent]
lcn1 [prf, in mathcomp.solvable.nilpotent]
lcn2 [prf, in mathcomp.solvable.nilpotent]
lcn_bigcprod [prf, in mathcomp.solvable.nilpotent]
lcn_bigdprod [prf, in mathcomp.solvable.nilpotent]
lcn_central [prf, in mathcomp.solvable.nilpotent]
lcn_char [prf, in mathcomp.solvable.nilpotent]
lcn_cont [prf, in mathcomp.solvable.nilpotent]
lcn_cprod [prf, in mathcomp.solvable.nilpotent]
lcn_dprod [prf, in mathcomp.solvable.nilpotent]
lcn_gFun [def, in mathcomp.solvable.nilpotent]
lcn_group_set [prf, in mathcomp.solvable.nilpotent]
lcn_igFun [def, in mathcomp.solvable.nilpotent]
lcn_mgFun [def, in mathcomp.solvable.nilpotent]
lcn_neq0 [abbrev, in mathcomp.field.separable]
lcn_nil_classP [prf, in mathcomp.solvable.nilpotent]
lcn_norm [prf, in mathcomp.solvable.nilpotent]
lcn_normal [prf, in mathcomp.solvable.nilpotent]
lcn_normalS [prf, in mathcomp.solvable.nilpotent]
lcn_sub [prf, in mathcomp.solvable.nilpotent]
lcn_sub_leq [prf, in mathcomp.solvable.nilpotent]
lcn_subS [prf, in mathcomp.solvable.nilpotent]
lcnE [prf, in mathcomp.solvable.nilpotent]
lcnP [prf, in mathcomp.solvable.nilpotent]
lcnS [prf, in mathcomp.solvable.nilpotent]
lcnSn [prf, in mathcomp.solvable.nilpotent]
lcnSnS [prf, in mathcomp.solvable.nilpotent]
Lcorrect [prf, in mathcomp.solvable.burnside_app]
lcoset [def, in mathcomp.finite_group.fingroup]
lcoset1 [prf, in mathcomp.finite_group.fingroup]
lcoset_eqP [prf, in mathcomp.finite_group.fingroup]
lcoset_id [prf, in mathcomp.finite_group.fingroup]
lcoset_inj [prf, in mathcomp.finite_group.fingroup]
lcoset_refl [prf, in mathcomp.finite_group.fingroup]
lcoset_sym [prf, in mathcomp.finite_group.fingroup]
lcoset_trans [prf, in mathcomp.finite_group.fingroup]
lcoset_transl [prf, in mathcomp.finite_group.fingroup]
lcosetE [prf, in mathcomp.finite_group.fingroup]
lcosetK [prf, in mathcomp.finite_group.fingroup]
lcosetKV [prf, in mathcomp.finite_group.fingroup]
lcosetM [prf, in mathcomp.finite_group.fingroup]
lcosetP [prf, in mathcomp.finite_group.fingroup]
lcosetS [prf, in mathcomp.finite_group.fingroup]
lcosets [def, in mathcomp.finite_group.fingroup]
lcosetsP [prf, in mathcomp.finite_group.fingroup]
Ldiv [def, in mathcomp.solvable.abelian]
LdivJ [prf, in mathcomp.solvable.abelian]
LdivP [prf, in mathcomp.solvable.abelian]
LdivT_J [prf, in mathcomp.solvable.abelian]
le0 [prf, in mathcomp.algebra.interval_inference]
le0F [prf, in mathcomp.algebra.interval_inference]
le0z_nat [prf, in mathcomp.algebra.ssrint]
le1 [prf, in mathcomp.algebra.interval_inference]
le_big_nat [prf, in mathcomp.boot.bigop]
le_big_nat_cond [prf, in mathcomp.boot.bigop]
le_big_ord [prf, in mathcomp.boot.bigop]
le_big_ord_cond [prf, in mathcomp.boot.bigop]
le_bound [def, in mathcomp.algebra.interval]
le_bound_anti [prf, in mathcomp.algebra.interval]
le_bound_refl [prf, in mathcomp.algebra.interval]
le_bound_trans [prf, in mathcomp.algebra.interval]
le_fix_order [prf, in mathcomp.boot.finset]
le_irrelevance [prf, in mathcomp.boot.ssrnat]
le_ninfty [prf, in mathcomp.algebra.interval]
le_num_itv_bound [prf, in mathcomp.algebra.interval_inference]
le_rat [def, in mathcomp.algebra.rat]
le_rat0 [prf, in mathcomp.algebra.rat]
le_rat0_anti [prf, in mathcomp.algebra.rat]
le_rat0D [prf, in mathcomp.algebra.rat]
le_rat0M [prf, in mathcomp.algebra.rat]
le_rat_total [prf, in mathcomp.algebra.rat]
le_ratE [prf, in mathcomp.algebra.rat]
lead_coef [def, in mathcomp.algebra.poly]
lead_coef0 [prf, in mathcomp.algebra.poly]
lead_coef1 [prf, in mathcomp.algebra.poly]
lead_coef_comp [prf, in mathcomp.algebra.poly]
lead_coef_eq0 [prf, in mathcomp.algebra.poly]
lead_coef_exp [prf, in mathcomp.algebra.poly]
lead_coef_lreg [prf, in mathcomp.algebra.poly]
lead_coef_map [prf, in mathcomp.algebra.poly]
lead_coef_map_eq [prf, in mathcomp.algebra.poly]
lead_coef_map_id0 [prf, in mathcomp.algebra.poly]
lead_coef_map_inj [prf, in mathcomp.algebra.poly]
lead_coef_Mmonic [prf, in mathcomp.algebra.poly]
lead_coef_monicM [prf, in mathcomp.algebra.poly]
lead_coef_poly [prf, in mathcomp.algebra.poly]
lead_coef_poly_XaY [prf, in mathcomp.algebra.polyXY]
lead_coef_prod [prf, in mathcomp.algebra.poly]
lead_coef_prod_XsubC [prf, in mathcomp.algebra.poly]
lead_coef_proper_mul [prf, in mathcomp.algebra.poly]
lead_coefC [prf, in mathcomp.algebra.poly]
lead_coefDl [prf, in mathcomp.algebra.poly]
lead_coefDr [prf, in mathcomp.algebra.poly]
lead_coefE [prf, in mathcomp.algebra.poly]
lead_coefM [prf, in mathcomp.algebra.poly]
lead_coefMX [prf, in mathcomp.algebra.poly]
lead_coefN [prf, in mathcomp.algebra.poly]
lead_coefX [prf, in mathcomp.algebra.poly]
lead_coefXaddC [prf, in mathcomp.algebra.poly]
lead_coefXn [prf, in mathcomp.algebra.poly]
lead_coefXnaddC [prf, in mathcomp.algebra.poly]
lead_coefXnsubC [prf, in mathcomp.algebra.poly]
lead_coefXsubC [prf, in mathcomp.algebra.poly]
lead_coefZ [prf, in mathcomp.algebra.poly]
leBRight_ltBLeft [prf, in mathcomp.algebra.interval]
leBSide [prf, in mathcomp.algebra.interval]
leC_nat [def, in mathcomp.field.algC]
left_arc [prf, in mathcomp.boot.path]
left_mx_ideal [def, in mathcomp.algebra.mxalgebra]
left_trans [prf, in mathcomp.boot.generic_quotient]
leNz_nat [prf, in mathcomp.algebra.ssrint]
leP [prf, in mathcomp.boot.ssrnat]
leq [def, in mathcomp.boot.ssrnat]
leq0n [prf, in mathcomp.boot.ssrnat]
leq_add [prf, in mathcomp.boot.ssrnat]
leq_add2l [prf, in mathcomp.boot.ssrnat]
leq_add2r [prf, in mathcomp.boot.ssrnat]
leq_addl [prf, in mathcomp.boot.ssrnat]
leq_addr [prf, in mathcomp.boot.ssrnat]
leq_b1 [prf, in mathcomp.boot.ssrnat]
leq_bigmax [prf, in mathcomp.boot.bigop]
leq_bigmax_cond [prf, in mathcomp.boot.bigop]
leq_bigmax_seq [prf, in mathcomp.boot.bigop]
leq_bin2l [prf, in mathcomp.boot.binomial]
leq_bump [prf, in mathcomp.boot.fintype]
leq_bump2 [prf, in mathcomp.boot.fintype]
leq_card [prf, in mathcomp.boot.fintype]
leq_card_cover [prf, in mathcomp.boot.finset]
leq_card_in [prf, in mathcomp.boot.fintype]
leq_card_setU [prf, in mathcomp.boot.finset]
leq_count_mask [prf, in mathcomp.boot.seq]
leq_count_subseq [prf, in mathcomp.boot.seq]
leq_dim_orthov1 [prf, in mathcomp.algebra.sesquilinear]
leq_div [prf, in mathcomp.boot.div]
leq_div2l [prf, in mathcomp.boot.div]
leq_div2r [prf, in mathcomp.boot.div]
leq_divDl [prf, in mathcomp.boot.div]
leq_divLR [prf, in mathcomp.boot.div]
leq_divM [prf, in mathcomp.boot.div]
leq_divRL [prf, in mathcomp.boot.div]
leq_double [prf, in mathcomp.boot.ssrnat]
leq_eqVlt [prf, in mathcomp.boot.ssrnat]
leq_exp2l [prf, in mathcomp.boot.ssrnat]
leq_exp2r [prf, in mathcomp.boot.ssrnat]
leq_fact [prf, in mathcomp.boot.ssrnat]
leq_geP [prf, in mathcomp.boot.ssrnat]
leq_gtF [prf, in mathcomp.boot.ssrnat]
leq_gtP [prf, in mathcomp.boot.ssrnat]
leq_half_double [prf, in mathcomp.boot.ssrnat]
leq_homg [prf, in mathcomp.finite_group.morphism]
leq_image_card [prf, in mathcomp.boot.fintype]
leq_imset_card [prf, in mathcomp.boot.finset]
leq_leP [prf, in mathcomp.boot.ssrnat]
leq_ltn_trans [prf, in mathcomp.boot.ssrnat]
leq_ltP [prf, in mathcomp.boot.ssrnat]
leq_max [prf, in mathcomp.boot.ssrnat]
leq_maxl [prf, in mathcomp.boot.ssrnat]
leq_maxr [prf, in mathcomp.boot.ssrnat]
leq_min [prf, in mathcomp.boot.ssrnat]
leq_mod [prf, in mathcomp.boot.div]
leq_mono [prf, in mathcomp.boot.ssrnat]
leq_mono_in [prf, in mathcomp.boot.ssrnat]
leq_morphim [prf, in mathcomp.finite_group.morphism]
leq_mul [prf, in mathcomp.boot.ssrnat]
leq_mul2l [prf, in mathcomp.boot.ssrnat]
leq_mul2r [prf, in mathcomp.boot.ssrnat]
leq_nmono [prf, in mathcomp.boot.ssrnat]
leq_nmono_in [prf, in mathcomp.boot.ssrnat]
leq_of_leqif [def, in mathcomp.boot.ssrnat]
leq_ord [prf, in mathcomp.boot.fintype]
leq_pexp2l [prf, in mathcomp.boot.ssrnat]
leq_pfact [prf, in mathcomp.boot.ssrnat]
leq_pmul2l [prf, in mathcomp.boot.ssrnat]
leq_pmul2r [prf, in mathcomp.boot.ssrnat]
leq_pmull [prf, in mathcomp.boot.ssrnat]
leq_pmulr [prf, in mathcomp.boot.ssrnat]
leq_pred [prf, in mathcomp.boot.ssrnat]
leq_prod [prf, in mathcomp.boot.bigop]
leq_psubCr [prf, in mathcomp.boot.ssrnat]
leq_psubRL [prf, in mathcomp.boot.ssrnat]
leq_quotient [prf, in mathcomp.finite_group.quotient]
leq_rot_add [prf, in mathcomp.boot.seq]
leq_Sdouble [prf, in mathcomp.boot.ssrnat]
leq_size_uniq [prf, in mathcomp.boot.seq]
leq_sizeP [prf, in mathcomp.algebra.poly]
leq_sqr [prf, in mathcomp.boot.ssrnat]
leq_sub [prf, in mathcomp.boot.ssrnat]
leq_sub2l [prf, in mathcomp.boot.ssrnat]
leq_sub2lE [prf, in mathcomp.boot.ssrnat]
leq_sub2r [prf, in mathcomp.boot.ssrnat]
leq_sub2rE [prf, in mathcomp.boot.ssrnat]
leq_subCl [prf, in mathcomp.boot.ssrnat]
leq_subCr [prf, in mathcomp.boot.ssrnat]
leq_subLR [prf, in mathcomp.boot.ssrnat]
leq_subr [prf, in mathcomp.boot.ssrnat]
leq_subRL [prf, in mathcomp.boot.ssrnat]
leq_subrR [prf, in mathcomp.boot.ssrnat]
leq_sum [prf, in mathcomp.boot.bigop]
leq_total [prf, in mathcomp.boot.ssrnat]
leq_trans [prf, in mathcomp.boot.ssrnat]
leq_trunc_div [abbrev, in mathcomp.boot.div]
leq_trunc_log [prf, in mathcomp.boot.prime]
leq_uniq_count [prf, in mathcomp.boot.seq]
leq_uniq_countP [prf, in mathcomp.boot.seq]
leq_up_log [prf, in mathcomp.boot.prime]
leq_uphalf_double [prf, in mathcomp.boot.ssrnat]
leq_xor_gtn [ind, in mathcomp.boot.ssrnat]
leqDmod [prf, in mathcomp.boot.div]
leqif [def, in mathcomp.boot.ssrnat]
leqif_add [prf, in mathcomp.boot.ssrnat]
leqif_dim_orthov1 [prf, in mathcomp.algebra.sesquilinear]
leqif_dim_orthov1_full [prf, in mathcomp.algebra.sesquilinear]
leqif_eq [prf, in mathcomp.boot.ssrnat]
leqif_geq [prf, in mathcomp.boot.ssrnat]
leqif_mul [prf, in mathcomp.boot.ssrnat]
leqif_refl [prf, in mathcomp.boot.ssrnat]
leqif_sum [prf, in mathcomp.boot.bigop]
leqif_trans [prf, in mathcomp.boot.ssrnat]
leqifP [prf, in mathcomp.boot.ssrnat]
leqLHS [abbrev, in mathcomp.boot.ssrnat]
leqn0 [prf, in mathcomp.boot.ssrnat]
leqNgt [prf, in mathcomp.boot.ssrnat]
leqnn [prf, in mathcomp.boot.ssrnat]
LeqNotGtn [constr, in mathcomp.boot.ssrnat]
leqnSn [prf, in mathcomp.boot.ssrnat]
leqP [prf, in mathcomp.boot.ssrnat]
leqRHS [abbrev, in mathcomp.boot.ssrnat]
leqSpred [prf, in mathcomp.boot.ssrnat]
leqVgt [prf, in mathcomp.boot.ssrnat]
leqW [prf, in mathcomp.boot.ssrnat]
leqW_mono [prf, in mathcomp.boot.ssrnat]
leqW_mono_in [prf, in mathcomp.boot.ssrnat]
leqW_nmono [prf, in mathcomp.boot.ssrnat]
leqW_nmono_in [prf, in mathcomp.boot.ssrnat]
ler0q [prf, in mathcomp.algebra.rat]
ler0z [prf, in mathcomp.algebra.ssrint]
ler1z [prf, in mathcomp.algebra.ssrint]
ler_eXz2l [prf, in mathcomp.algebra.ssrint]
ler_int [prf, in mathcomp.algebra.ssrint]
ler_niXz2l [prf, in mathcomp.algebra.ssrint]
ler_nMz2l [prf, in mathcomp.algebra.ssrint]
ler_nMz2r [prf, in mathcomp.algebra.ssrint]
ler_nXz2r [prf, in mathcomp.algebra.ssrint]
ler_piXz2l [prf, in mathcomp.algebra.ssrint]
ler_pMz2l [prf, in mathcomp.algebra.ssrint]
ler_pMz2r [prf, in mathcomp.algebra.ssrint]
ler_pXz2r [prf, in mathcomp.algebra.ssrint]
ler_rat [prf, in mathcomp.algebra.rat]
ler_weXz2l [prf, in mathcomp.algebra.ssrint]
ler_wneXz2l [prf, in mathcomp.algebra.ssrint]
ler_wniXz2l [prf, in mathcomp.algebra.ssrint]
ler_wnMz2l [prf, in mathcomp.algebra.ssrint]
ler_wnMz2r [prf, in mathcomp.algebra.ssrint]
ler_wnXz2r [prf, in mathcomp.algebra.ssrint]
ler_wpeXz2l [prf, in mathcomp.algebra.ssrint]
ler_wpiXz2l [prf, in mathcomp.algebra.ssrint]
ler_wpMz2l [prf, in mathcomp.algebra.ssrint]
ler_wpMz2r [prf, in mathcomp.algebra.ssrint]
ler_wpXz2r [prf, in mathcomp.algebra.ssrint]
lerq0 [prf, in mathcomp.algebra.rat]
lerz0 [prf, in mathcomp.algebra.ssrint]
lerz1 [prf, in mathcomp.algebra.ssrint]
lez0_abs [prf, in mathcomp.algebra.ssrint]
lez0_nat [prf, in mathcomp.algebra.ssrint]
lez1D [prf, in mathcomp.algebra.ssrint]
lez_abs [prf, in mathcomp.algebra.ssrint]
lez_div [prf, in mathcomp.algebra.intdiv]
lez_divLR [prf, in mathcomp.algebra.intdiv]
lez_divRL [prf, in mathcomp.algebra.intdiv]
lez_floor [prf, in mathcomp.algebra.intdiv]
lez_nat [prf, in mathcomp.algebra.ssrint]
lez_pdiv2r [prf, in mathcomp.algebra.intdiv]
lezD1 [prf, in mathcomp.algebra.ssrint]
lezN_nat [prf, in mathcomp.algebra.ssrint]
lfun1_neq0 [prf, in mathcomp.algebra.vector]
lfun1_poly [prf, in mathcomp.field.falgebra]
lfun_add0 [prf, in mathcomp.algebra.vector]
lfun_addA [prf, in mathcomp.algebra.vector]
lfun_addC [prf, in mathcomp.algebra.vector]
lfun_addN [prf, in mathcomp.algebra.vector]
lfun_algType [def, in mathcomp.algebra.vector]
lfun_comp_nzRingType [def, in mathcomp.algebra.vector]
lfun_comp_pzSemiRingType [def, in mathcomp.algebra.vector]
lfun_img [def, in mathcomp.algebra.vector]
lfun_img_def [def, in mathcomp.algebra.vector]
lfun_img_key [prf, in mathcomp.algebra.vector]
lfun_img_unlockable [def, in mathcomp.algebra.vector]
lfun_is_semilinear [prf, in mathcomp.algebra.vector]
lfun_key [prf, in mathcomp.algebra.vector]
lfun_lalgType [def, in mathcomp.algebra.vector]
lfun_nzRingType [def, in mathcomp.algebra.vector]
lfun_preim [def, in mathcomp.algebra.vector]
lfun_scale0 [prf, in mathcomp.algebra.vector]
lfun_scale1 [prf, in mathcomp.algebra.vector]
lfun_scaleA [prf, in mathcomp.algebra.vector]
lfun_scaleDl [prf, in mathcomp.algebra.vector]
lfun_scaleDr [prf, in mathcomp.algebra.vector]
lfun_simp [def, in mathcomp.algebra.vector]
lfun_vect_iso [prf, in mathcomp.algebra.vector]
lfunE [prf, in mathcomp.algebra.vector]
lfunP [prf, in mathcomp.algebra.vector]
lfunPn [prf, in mathcomp.algebra.vector]
lift [def, in mathcomp.boot.fintype]
lift0 [prf, in mathcomp.boot.fintype]
lift0_mx [def, in mathcomp.algebra.matrix]
lift0_mx_is_perm [prf, in mathcomp.algebra.matrix]
lift0_mx_perm [prf, in mathcomp.algebra.matrix]
lift0_perm [def, in mathcomp.finite_group.perm]
lift0_perm0 [prf, in mathcomp.finite_group.perm]
lift0_perm_eq0 [prf, in mathcomp.finite_group.perm]
lift0_perm_lift [prf, in mathcomp.finite_group.perm]
lift0_permK [prf, in mathcomp.finite_group.perm]
lift_cst [abbrev, in mathcomp.boot.generic_quotient]
lift_embed [abbrev, in mathcomp.boot.generic_quotient]
lift_eqF [prf, in mathcomp.boot.fintype]
lift_fun1 [abbrev, in mathcomp.boot.generic_quotient]
lift_fun2 [abbrev, in mathcomp.boot.generic_quotient]
lift_inj [prf, in mathcomp.boot.fintype]
lift_max [prf, in mathcomp.boot.fintype]
lift_op1 [abbrev, in mathcomp.boot.generic_quotient]
lift_op11 [abbrev, in mathcomp.boot.generic_quotient]
lift_op2 [abbrev, in mathcomp.boot.generic_quotient]
lift_perm [def, in mathcomp.finite_group.perm]
lift_perm1 [prf, in mathcomp.finite_group.perm]
lift_perm_fun [def, in mathcomp.finite_group.perm]
lift_perm_id [prf, in mathcomp.finite_group.perm]
lift_perm_lift [prf, in mathcomp.finite_group.perm]
lift_permK [prf, in mathcomp.finite_group.perm]
lift_permM [prf, in mathcomp.finite_group.perm]
lift_permV [prf, in mathcomp.finite_group.perm]
liftK [prf, in mathcomp.boot.fintype]
lim0g [prf, in mathcomp.algebra.vector]
lim1g [prf, in mathcomp.algebra.vector]
limg [abbrev, in mathcomp.algebra.vector]
limg0 [prf, in mathcomp.algebra.vector]
limg_amulr [prf, in mathcomp.field.falgebra]
limg_basis_of [prf, in mathcomp.algebra.vector]
limg_bigcap [prf, in mathcomp.algebra.vector]
limg_cap [prf, in mathcomp.algebra.vector]
limg_comp [prf, in mathcomp.algebra.vector]
limg_dim_eq [prf, in mathcomp.algebra.vector]
limg_gal [prf, in mathcomp.field.galois]
limg_ker0 [prf, in mathcomp.algebra.vector]
limg_ker_compl [prf, in mathcomp.algebra.vector]
limg_ker_dim [prf, in mathcomp.algebra.vector]
limg_lfunVK [prf, in mathcomp.algebra.vector]
limg_line [prf, in mathcomp.algebra.vector]
limg_proj [prf, in mathcomp.algebra.vector]
limg_span [prf, in mathcomp.algebra.vector]
limg_sum [prf, in mathcomp.algebra.vector]
limgD [prf, in mathcomp.algebra.vector]
limgS [prf, in mathcomp.algebra.vector]
lin1_mx [def, in mathcomp.algebra.matrix]
lin1_mx_key [prf, in mathcomp.algebra.matrix]
lin_char1 [prf, in mathcomp.group_representation.character]
lin_char_der1 [prf, in mathcomp.group_representation.character]
lin_char_group [prf, in mathcomp.group_representation.character]
lin_char_irr [prf, in mathcomp.group_representation.character]
lin_char_neq0 [prf, in mathcomp.group_representation.character]
lin_char_prod [prf, in mathcomp.group_representation.character]
lin_char_unitr [prf, in mathcomp.group_representation.character]
lin_char_unity_root [prf, in mathcomp.group_representation.character]
lin_charM [prf, in mathcomp.group_representation.character]
lin_charV [prf, in mathcomp.group_representation.character]
lin_charV_conj [prf, in mathcomp.group_representation.character]
lin_charW [prf, in mathcomp.group_representation.character]
lin_charX [prf, in mathcomp.group_representation.character]
lin_irr_der1 [prf, in mathcomp.group_representation.character]
lin_mul_row [def, in mathcomp.algebra.matrix]
lin_mul_row_is_linear [prf, in mathcomp.algebra.matrix]
lin_mul_row_is_semilinear [prf, in mathcomp.algebra.matrix]
lin_mulmx [def, in mathcomp.algebra.matrix]
lin_mulmx_is_linear [prf, in mathcomp.algebra.matrix]
lin_mulmx_is_semilinear [prf, in mathcomp.algebra.matrix]
lin_mulmxr [def, in mathcomp.algebra.matrix]
lin_mulmxr_is_linear [prf, in mathcomp.algebra.matrix]
lin_mulmxr_is_semilinear [prf, in mathcomp.algebra.matrix]
lin_mx [def, in mathcomp.algebra.matrix]
lin_Res_IirrE [prf, in mathcomp.group_representation.character]
linear0l [prf, in mathcomp.algebra.sesquilinear]
linear0r [prf, in mathcomp.algebra.sesquilinear]
linear_char [def, in mathcomp.group_representation.character]
linear_char_divr [prf, in mathcomp.group_representation.character]
linear_char_pred [def, in mathcomp.group_representation.character]
linear_irr [def, in mathcomp.group_representation.mxrepresentation]
linear_irr_comp [abbrev, in mathcomp.group_representation.mxrepresentation]
linear_irr_comp_pchar [prf, in mathcomp.group_representation.mxrepresentation]
linear_mx_abs_irr [prf, in mathcomp.group_representation.mxrepresentation]
linear_mxsimple [prf, in mathcomp.group_representation.mxrepresentation]
linear_of_free [prf, in mathcomp.algebra.vector]
linear_sumlz [prf, in mathcomp.algebra.sesquilinear]
linear_sumr [prf, in mathcomp.algebra.sesquilinear]
linearBl [prf, in mathcomp.algebra.sesquilinear]
linearBr [prf, in mathcomp.algebra.sesquilinear]
linearDl [prf, in mathcomp.algebra.sesquilinear]
linearDr [prf, in mathcomp.algebra.sesquilinear]
linearMn [prf, in mathcomp.algebra.ssrint]
linearMnl [prf, in mathcomp.algebra.sesquilinear]
linearMNnl [prf, in mathcomp.algebra.sesquilinear]
linearMNnr [prf, in mathcomp.algebra.sesquilinear]
linearMnr [prf, in mathcomp.algebra.sesquilinear]
linearNl [prf, in mathcomp.algebra.sesquilinear]
linearNr [prf, in mathcomp.algebra.sesquilinear]
linearPl [prf, in mathcomp.algebra.sesquilinear]
linearPr [prf, in mathcomp.algebra.sesquilinear]
linearZl [prf, in mathcomp.algebra.sesquilinear]
linearZl_LR [prf, in mathcomp.algebra.sesquilinear]
linearZlr [prf, in mathcomp.algebra.sesquilinear]
linearZr [prf, in mathcomp.algebra.sesquilinear]
linearZr_LR [prf, in mathcomp.algebra.sesquilinear]
linearZrl [prf, in mathcomp.algebra.sesquilinear]
linfun [def, in mathcomp.algebra.vector]
linfun_ahom [def, in mathcomp.field.falgebra]
linfun_def [def, in mathcomp.algebra.vector]
linfun_is_ahom [prf, in mathcomp.field.falgebra]
linfun_unlockable [def, in mathcomp.algebra.vector]
lker [def, in mathcomp.algebra.vector]
lker0_amull [prf, in mathcomp.field.falgebra]
lker0_amulr [prf, in mathcomp.field.falgebra]
lker0_compfK [prf, in mathcomp.algebra.vector]
lker0_compfV [prf, in mathcomp.algebra.vector]
lker0_compfVK [prf, in mathcomp.algebra.vector]
lker0_compKf [prf, in mathcomp.algebra.vector]
lker0_compVf [prf, in mathcomp.algebra.vector]
lker0_compVKf [prf, in mathcomp.algebra.vector]
lker0_img_cap [prf, in mathcomp.algebra.vector]
lker0_lfunK [prf, in mathcomp.algebra.vector]
lker0_lfunVK [prf, in mathcomp.algebra.vector]
lker0_limgf [prf, in mathcomp.algebra.vector]
lker0P [prf, in mathcomp.algebra.vector]
lker_proj [prf, in mathcomp.algebra.vector]
lkerE [prf, in mathcomp.algebra.vector]
Lmodule_hasFinDim [abbrev, in mathcomp.algebra.vector]
Lmodule_hasFinDim [mod, in mathcomp.algebra.vector]
Lmodule_hasFinDim.axioms [abbrev, in mathcomp.algebra.vector]
Lmodule_hasFinDim.axioms_ [rec, in mathcomp.algebra.vector]
Lmodule_hasFinDim.Build [abbrev, in mathcomp.algebra.vector]
Lmodule_hasFinDim.dim [proj, in mathcomp.algebra.vector]
Lmodule_hasFinDim.Exports [mod, in mathcomp.algebra.vector]
Lmodule_hasFinDim.phant_axioms [def, in mathcomp.algebra.vector]
Lmodule_hasFinDim.phant_Build [def, in mathcomp.algebra.vector]
Lmodule_hasFinDim.vector_subdef [proj, in mathcomp.algebra.vector]
logn [def, in mathcomp.boot.prime]
logn0 [prf, in mathcomp.boot.prime]
logn1 [prf, in mathcomp.boot.prime]
logn_card_GL_p [prf, in mathcomp.algebra.mxalgebra]
logn_coprime [prf, in mathcomp.boot.prime]
logn_count_dvd [prf, in mathcomp.boot.prime]
logn_div [prf, in mathcomp.boot.prime]
logn_fact [prf, in mathcomp.boot.binomial]
logn_Gauss [prf, in mathcomp.boot.prime]
logn_gcd [prf, in mathcomp.boot.prime]
logn_gt0 [prf, in mathcomp.boot.prime]
logn_lcm [prf, in mathcomp.boot.prime]
logn_le_p_rank [prf, in mathcomp.solvable.abelian]
logn_morphim [prf, in mathcomp.finite_group.quotient]
logn_part [prf, in mathcomp.boot.prime]
logn_prime [prf, in mathcomp.boot.prime]
logn_quotient [prf, in mathcomp.solvable.abelian]
logn_quotient_cent_cyclic_pgroup [prf, in mathcomp.solvable.pgroup]
logn_rec [def, in mathcomp.boot.prime]
lognE [prf, in mathcomp.boot.prime]
lognM [prf, in mathcomp.boot.prime]
lognSg [prf, in mathcomp.finite_group.fingroup]
lognX [prf, in mathcomp.boot.prime]
lone_subgroup_char [prf, in mathcomp.finite_group.automorphism]
looping [def, in mathcomp.boot.path]
looping_order [prf, in mathcomp.boot.fingraph]
looping_uniq [prf, in mathcomp.boot.path]
loopingP [prf, in mathcomp.boot.path]
lower_central_at [def, in mathcomp.solvable.nilpotent]
lower_central_at_group [def, in mathcomp.solvable.nilpotent]
lpreim0 [prf, in mathcomp.algebra.vector]
lpreim_cap_limg [prf, in mathcomp.algebra.vector]
lpreimK [prf, in mathcomp.algebra.vector]
lpreimS [prf, in mathcomp.algebra.vector]
lra [file, in mathcomp.algebra.lra]
lreg_lead [prf, in mathcomp.algebra.poly]
lreg_lead0 [prf, in mathcomp.algebra.poly]
lreg_polyZ_eq0 [prf, in mathcomp.algebra.poly]
lreg_size [prf, in mathcomp.algebra.poly]
lSemiAlgType [abbrev, in mathcomp.algebra.algebraic_hierarchy.ssralg]
LSemiModule_hasFinDim [abbrev, in mathcomp.algebra.vector]
LSemiModule_hasFinDim [mod, in mathcomp.algebra.vector]
LSemiModule_hasFinDim.axioms [abbrev, in mathcomp.algebra.vector]
LSemiModule_hasFinDim.axioms_ [rec, in mathcomp.algebra.vector]
LSemiModule_hasFinDim.Build [abbrev, in mathcomp.algebra.vector]
LSemiModule_hasFinDim.dim [proj, in mathcomp.algebra.vector]
LSemiModule_hasFinDim.Exports [mod, in mathcomp.algebra.vector]
LSemiModule_hasFinDim.identity_builder [def, in mathcomp.algebra.vector]
LSemiModule_hasFinDim.phant_axioms [def, in mathcomp.algebra.vector]
LSemiModule_hasFinDim.phant_Build [def, in mathcomp.algebra.vector]
LSemiModule_hasFinDim.vector_subdef [proj, in mathcomp.algebra.vector]
lshift [def, in mathcomp.boot.fintype]
lshift0 [prf, in mathcomp.boot.nmodule]
lshift_inj [prf, in mathcomp.boot.fintype]
lsubmx [def, in mathcomp.algebra.matrix]
lsubmx_const [prf, in mathcomp.algebra.matrix]
lsubmx_key [prf, in mathcomp.algebra.matrix]
lsubmxEsub [prf, in mathcomp.algebra.matrix]
lt0 [prf, in mathcomp.algebra.interval_inference]
lt0b [prf, in mathcomp.boot.ssrnat]
lt0F [prf, in mathcomp.algebra.interval_inference]
lt0mx [prf, in mathcomp.algebra.mxalgebra]
lt0n [prf, in mathcomp.boot.ssrnat]
lt0n_neq0 [prf, in mathcomp.boot.ssrnat]
lt1 [prf, in mathcomp.algebra.interval_inference]
lt1mx [prf, in mathcomp.algebra.mxalgebra]
lt_bound [def, in mathcomp.algebra.interval]
lt_bound_def [prf, in mathcomp.algebra.interval]
lt_eqmx [prf, in mathcomp.algebra.mxalgebra]
lt_in_itv [prf, in mathcomp.algebra.interval]
lt_irrelevance [prf, in mathcomp.boot.ssrnat]
lt_ninfty [prf, in mathcomp.algebra.interval]
lt_rat [def, in mathcomp.algebra.rat]
lt_rat0 [prf, in mathcomp.algebra.rat]
lt_rat_def [prf, in mathcomp.algebra.rat]
lt_ratE [prf, in mathcomp.algebra.rat]
lt_size_deriv [prf, in mathcomp.algebra.poly]
ltBRight_leBLeft [prf, in mathcomp.algebra.interval]
ltBSide [prf, in mathcomp.algebra.interval]
ltC_nat [def, in mathcomp.field.algC]
lteBSide [def, in mathcomp.algebra.interval]
lteif_in_itv [prf, in mathcomp.algebra.interval]
lteNz_nat [def, in mathcomp.algebra.ssrint]
ltez_nat [def, in mathcomp.algebra.ssrint]
ltez_natE [def, in mathcomp.algebra.ssrint]
ltezN_nat [def, in mathcomp.algebra.ssrint]
ltmx [def, in mathcomp.algebra.mxalgebra]
ltmx0 [prf, in mathcomp.algebra.mxalgebra]
ltmx1 [prf, in mathcomp.algebra.mxalgebra]
ltmx_irrefl [prf, in mathcomp.algebra.mxalgebra]
ltmx_sub_trans [prf, in mathcomp.algebra.mxalgebra]
ltmx_trans [prf, in mathcomp.algebra.mxalgebra]
ltmxE [prf, in mathcomp.algebra.mxalgebra]
ltmxEneq [prf, in mathcomp.algebra.mxalgebra]
ltmxErank [prf, in mathcomp.algebra.mxalgebra]
ltmxW [prf, in mathcomp.algebra.mxalgebra]
ltn [def, in mathcomp.boot.ssrnat]
ltn0 [prf, in mathcomp.boot.ssrnat]
ltn0Sn [prf, in mathcomp.boot.ssrnat]
ltn_add2l [prf, in mathcomp.boot.ssrnat]
ltn_add2r [prf, in mathcomp.boot.ssrnat]
ltn_addl [prf, in mathcomp.boot.ssrnat]
ltn_addr [prf, in mathcomp.boot.ssrnat]
ltn_ceil [prf, in mathcomp.boot.div]
ltn_divLR [prf, in mathcomp.boot.div]
ltn_divRL [prf, in mathcomp.boot.div]
ltn_double [prf, in mathcomp.boot.ssrnat]
ltn_eqF [prf, in mathcomp.boot.ssrnat]
ltn_exp2l [prf, in mathcomp.boot.ssrnat]
ltn_exp2r [prf, in mathcomp.boot.ssrnat]
ltn_expl [prf, in mathcomp.boot.ssrnat]
ltn_fact [prf, in mathcomp.boot.ssrnat]
ltn_geF [prf, in mathcomp.boot.ssrnat]
ltn_gtP [prf, in mathcomp.boot.ssrnat]
ltn_half_double [prf, in mathcomp.boot.ssrnat]
ltn_ind [prf, in mathcomp.boot.ssrnat]
ltn_leq_trans [prf, in mathcomp.boot.ssrnat]
ltn_leqif [prf, in mathcomp.boot.ssrnat]
ltn_log0 [prf, in mathcomp.boot.prime]
ltn_log_quotient [prf, in mathcomp.solvable.pgroup]
ltn_logl [prf, in mathcomp.boot.prime]
ltn_ltP [prf, in mathcomp.boot.ssrnat]
ltn_min [prf, in mathcomp.boot.ssrnat]
ltn_mod [prf, in mathcomp.boot.div]
ltn_morphim [prf, in mathcomp.finite_group.morphism]
ltn_mul [prf, in mathcomp.boot.ssrnat]
ltn_mul2l [prf, in mathcomp.boot.ssrnat]
ltn_mul2r [prf, in mathcomp.boot.ssrnat]
ltn_mull [prf, in mathcomp.boot.ssrnat]
ltn_mulr [prf, in mathcomp.boot.ssrnat]
ltn_neqAle [prf, in mathcomp.boot.ssrnat]
ltn_odd_Frobenius_ker [prf, in mathcomp.solvable.frobenius]
ltn_ord [prf, in mathcomp.boot.fintype]
ltn_Pdiv [prf, in mathcomp.boot.div]
ltn_pdiv2_prime [prf, in mathcomp.boot.prime]
ltn_pexp2l [prf, in mathcomp.boot.ssrnat]
ltn_pfact [prf, in mathcomp.boot.ssrnat]
ltn_pmod [prf, in mathcomp.boot.div]
ltn_pmul2l [prf, in mathcomp.boot.ssrnat]
ltn_pmul2r [prf, in mathcomp.boot.ssrnat]
ltn_Pmull [prf, in mathcomp.boot.ssrnat]
ltn_Pmulr [prf, in mathcomp.boot.ssrnat]
ltn_predK [prf, in mathcomp.boot.ssrnat]
ltn_predL [prf, in mathcomp.boot.ssrnat]
ltn_predRL [prf, in mathcomp.boot.ssrnat]
ltn_psubCl [prf, in mathcomp.boot.ssrnat]
ltn_psubLR [prf, in mathcomp.boot.ssrnat]
ltn_quotient [prf, in mathcomp.finite_group.quotient]
ltn_Sdouble [prf, in mathcomp.boot.ssrnat]
ltn_size_undup [prf, in mathcomp.boot.seq]
ltn_sorted_uniq_leq [prf, in mathcomp.boot.path]
ltn_sqr [prf, in mathcomp.boot.ssrnat]
ltn_sub2l [prf, in mathcomp.boot.ssrnat]
ltn_sub2lE [prf, in mathcomp.boot.ssrnat]
ltn_sub2r [prf, in mathcomp.boot.ssrnat]
ltn_sub2rE [prf, in mathcomp.boot.ssrnat]
ltn_subCl [prf, in mathcomp.boot.ssrnat]
ltn_subCr [prf, in mathcomp.boot.ssrnat]
ltn_subLR [prf, in mathcomp.boot.ssrnat]
ltn_subRL [prf, in mathcomp.boot.ssrnat]
ltn_subrL [prf, in mathcomp.boot.ssrnat]
ltn_subrR [prf, in mathcomp.boot.ssrnat]
ltn_trans [prf, in mathcomp.boot.ssrnat]
ltn_unsplit [prf, in mathcomp.boot.fintype]
ltn_uphalf_double [prf, in mathcomp.boot.ssrnat]
ltn_xor_geq [ind, in mathcomp.boot.ssrnat]
ltngtP [prf, in mathcomp.boot.ssrnat]
ltnLHS [abbrev, in mathcomp.boot.ssrnat]
ltnn [prf, in mathcomp.boot.ssrnat]
ltnNge [prf, in mathcomp.boot.ssrnat]
ltnNleqif [prf, in mathcomp.boot.ssrnat]
LtnNotGeq [constr, in mathcomp.boot.ssrnat]
ltnP [prf, in mathcomp.boot.ssrnat]
ltnRHS [abbrev, in mathcomp.boot.ssrnat]
ltnS [prf, in mathcomp.boot.ssrnat]
ltnSE [prf, in mathcomp.boot.ssrnat]
ltnSn [prf, in mathcomp.boot.ssrnat]
ltnW [prf, in mathcomp.boot.ssrnat]
ltnW_homo [prf, in mathcomp.boot.ssrnat]
ltnW_homo_in [prf, in mathcomp.boot.ssrnat]
ltnW_nhomo [prf, in mathcomp.boot.ssrnat]
ltnW_nhomo_in [prf, in mathcomp.boot.ssrnat]
ltNz_nat [prf, in mathcomp.algebra.ssrint]
ltP [prf, in mathcomp.boot.ssrnat]
ltr0_sgz [prf, in mathcomp.algebra.ssrint]
ltr0q [prf, in mathcomp.algebra.rat]
ltr0z [prf, in mathcomp.algebra.ssrint]
ltr1z [prf, in mathcomp.algebra.ssrint]
ltr_eXz2l [prf, in mathcomp.algebra.ssrint]
ltr_int [prf, in mathcomp.algebra.ssrint]
ltr_niXz2l [prf, in mathcomp.algebra.ssrint]
ltr_nMz2l [prf, in mathcomp.algebra.ssrint]
ltr_nMz2r [prf, in mathcomp.algebra.ssrint]
ltr_nXz2r [prf, in mathcomp.algebra.ssrint]
ltr_piXz2l [prf, in mathcomp.algebra.ssrint]
ltr_pMz2l [prf, in mathcomp.algebra.ssrint]
ltr_pMz2r [prf, in mathcomp.algebra.ssrint]
ltr_pXz2r [prf, in mathcomp.algebra.ssrint]
ltr_rat [prf, in mathcomp.algebra.rat]
ltrq0 [prf, in mathcomp.algebra.rat]
ltrz0 [prf, in mathcomp.algebra.ssrint]
ltrz1 [prf, in mathcomp.algebra.ssrint]
ltz0_abs [prf, in mathcomp.algebra.ssrint]
ltz1D [prf, in mathcomp.algebra.ssrint]
ltz_ceil [prf, in mathcomp.algebra.intdiv]
ltz_divLR [prf, in mathcomp.algebra.intdiv]
ltz_divRL [prf, in mathcomp.algebra.intdiv]
ltz_mod [prf, in mathcomp.algebra.intdiv]
ltz_nat [prf, in mathcomp.algebra.ssrint]
ltz_pmod [prf, in mathcomp.algebra.intdiv]
ltzD1 [prf, in mathcomp.algebra.ssrint]
ltzN_nat [prf, in mathcomp.algebra.ssrint]
LUP_card_GL [prf, in mathcomp.algebra.mxalgebra]