L (Definitions)
| 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 (Definitions)
lagrange [def, in mathcomp.algebra.qpoly]lambda_system [def, in mathcomp.analysis.measure_theory.measurable_structure]
last [def, in mathcomp.boot.seq]
lbound [def, in mathcomp.classical.classical_sets]
lcmn [def, in mathcomp.boot.div]
lcmz [def, in mathcomp.algebra.intdiv]
lcn_gFun [def, in mathcomp.solvable.nilpotent]
lcn_igFun [def, in mathcomp.solvable.nilpotent]
lcn_mgFun [def, in mathcomp.solvable.nilpotent]
lcoset [def, in mathcomp.finite_group.fingroup]
lcosets [def, in mathcomp.finite_group.fingroup]
Ldiv [def, in mathcomp.solvable.abelian]
le_bound [def, in mathcomp.algebra.interval]
le_ereal [def, in mathcomp.reals.constructive_ereal]
le_expandLR [def, in mathcomp.analysis.ereal]
le_expandRL [def, in mathcomp.analysis.ereal]
le_outer_measure [def, in mathcomp.analysis.measure_theory.measure_extension]
le_rat [def, in mathcomp.algebra.rat]
lead_coef [def, in mathcomp.algebra.poly]
Lebesgue_finite [def, in mathcomp.analysis.hoelder]
lebesgue_measure [def, in mathcomp.analysis.lebesgue_measure]
lebesgue_pt [def, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation]
lebesgue_stieltjes_measure [def, in mathcomp.analysis.lebesgue_stieltjes_measure]
LebesgueMeasure.hlength [def, in mathcomp.analysis.lebesgue_measure]
LebesgueMeasure.lebesgue_measure [def, in mathcomp.analysis.lebesgue_measure]
LebesgueSpace.pack_ [def, in mathcomp.analysis.hoelder]
LebesgueSpace.phant_clone [def, in mathcomp.analysis.hoelder]
LebesgueSpace.phant_on_ [def, in mathcomp.analysis.hoelder]
leC_nat [def, in mathcomp.field.algC]
left_mx_ideal [def, in mathcomp.algebra.mxalgebra]
leq [def, in mathcomp.boot.ssrnat]
leq_of_leqif [def, in mathcomp.boot.ssrnat]
leqif [def, in mathcomp.boot.ssrnat]
Lfun [def, in mathcomp.analysis.hoelder]
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_unlockable [def, in mathcomp.algebra.vector]
Lfun_key [def, in mathcomp.analysis.hoelder]
Lfun_keyed [def, in mathcomp.analysis.hoelder]
lfun_lalgType [def, in mathcomp.algebra.vector]
lfun_nzRingType [def, in mathcomp.algebra.vector]
lfun_preim [def, in mathcomp.algebra.vector]
lfun_simp [def, in mathcomp.algebra.vector]
Lfun_Sub [def, in mathcomp.analysis.hoelder]
Lfunction.pack_ [def, in mathcomp.analysis.hoelder]
Lfunction.phant_clone [def, in mathcomp.analysis.hoelder]
Lfunction.phant_on_ [def, in mathcomp.analysis.hoelder]
Lfunction_finite [def, in mathcomp.analysis.hoelder]
lift [def, in mathcomp.boot.fintype]
lift0_mx [def, in mathcomp.algebra.matrix]
lift0_perm [def, in mathcomp.finite_group.perm]
lift_perm [def, in mathcomp.finite_group.perm]
lift_perm_fun [def, in mathcomp.finite_group.perm]
lim [def, in mathcomp.classical.filter]
lim_in [def, in mathcomp.classical.filter]
lim_max_approxRN_seq.epsRN [def, in mathcomp.analysis.charge]
lim_max_approxRN_seq.fRN [def, in mathcomp.analysis.charge]
lim_max_approxRN_seq.sigmaRN [def, in mathcomp.analysis.charge]
lim_sup_davg [def, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation]
lim_sup_set [def, in mathcomp.analysis.measure_theory.measure_function]
lime_inf [def, in mathcomp.analysis.realfun]
lime_sup [def, in mathcomp.analysis.realfun]
limf_einf [def, in mathcomp.analysis.normedtype_theory.ereal_normedtype]
limf_esup [def, in mathcomp.analysis.normedtype_theory.ereal_normedtype]
limit_point [def, in mathcomp.analysis.topology_theory.topology_structure]
limn_einf [def, in mathcomp.analysis.sequences]
limn_esup [def, in mathcomp.analysis.sequences]
limn_inf [def, in mathcomp.analysis.sequences]
limn_sup [def, in mathcomp.analysis.sequences]
lin1_mx [def, in mathcomp.algebra.matrix]
lin_mul_row [def, in mathcomp.algebra.matrix]
lin_mulmx [def, in mathcomp.algebra.matrix]
lin_mulmxr [def, in mathcomp.algebra.matrix]
lin_mx [def, in mathcomp.algebra.matrix]
line_path [def, in mathcomp.classical.set_interval]
linfun [def, in mathcomp.algebra.vector]
linfun_ahom [def, in mathcomp.field.falgebra]
linfun_def [def, in mathcomp.algebra.vector]
linfun_unlockable [def, in mathcomp.algebra.vector]
lipschitz_on [def, in mathcomp.analysis.normedtype_theory.normed_module]
littleo0 [def, in mathcomp.analysis.landau]
littleo_clone [def, in mathcomp.analysis.landau]
littleo_is_bigO [def, in mathcomp.analysis.landau]
lker [def, in mathcomp.algebra.vector]
Lmodule_hasFinDim.phant_axioms [def, in mathcomp.algebra.vector]
Lmodule_hasFinDim.phant_Build [def, in mathcomp.algebra.vector]
Lmodule_isNormed.phant_axioms [def, in mathcomp.analysis.normedtype_theory.normed_module]
Lmodule_isNormed.phant_Build [def, in mathcomp.analysis.normedtype_theory.normed_module]
ln [def, in mathcomp.analysis.exp]
lne [def, in mathcomp.analysis.exp]
Lnorm.body [def, in mathcomp.analysis.hoelder]
Lnorm.unlock [def, in mathcomp.analysis.hoelder]
Lnorm_unlock_subterm [def, in mathcomp.analysis.hoelder]
locally_compact [def, in mathcomp.analysis.topology_theory.compact]
locally_convex [def, in mathcomp.analysis.normedtype_theory.tvs]
locally_integrable [def, in mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_differentiation]
locally_of [def, in mathcomp.analysis.topology_theory.topology_structure]
locked_acos [def, in mathcomp.analysis.trigo]
locked_asin [def, in mathcomp.analysis.trigo]
locked_atan [def, in mathcomp.analysis.trigo]
locked_cos [def, in mathcomp.analysis.trigo]
locked_Lnorm [def, in mathcomp.analysis.hoelder]
locked_sin [def, in mathcomp.analysis.trigo]
logn [def, in mathcomp.boot.prime]
logn_rec [def, in mathcomp.boot.prime]
looping [def, in mathcomp.boot.path]
lower_bound [def, in mathcomp.classical.wochoice]
lower_central_at [def, in mathcomp.solvable.nilpotent]
lower_central_at_group [def, in mathcomp.solvable.nilpotent]
lower_semicontinuous [def, in mathcomp.analysis.normedtype_theory.ereal_normedtype]
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]
lshift [def, in mathcomp.boot.fintype]
Lspace [def, in mathcomp.analysis.hoelder]
LspaceType1 [def, in mathcomp.analysis.hoelder]
LspaceType2 [def, in mathcomp.analysis.hoelder]
lsubmx [def, in mathcomp.algebra.matrix]
lt_bound [def, in mathcomp.algebra.interval]
lt_contract [def, in mathcomp.reals.constructive_ereal]
lt_ereal [def, in mathcomp.reals.constructive_ereal]
lt_expand [def, in mathcomp.reals.constructive_ereal]
lt_expandLR [def, in mathcomp.analysis.ereal]
lt_expandRL [def, in mathcomp.analysis.ereal]
lt_rat [def, in mathcomp.algebra.rat]
ltC_nat [def, in mathcomp.field.algC]
lteBSide [def, in mathcomp.algebra.interval]
ltee_pV2 [def, in mathcomp.reals.constructive_ereal]
lteey [def, in mathcomp.reals.constructive_ereal]
lteNye [def, in mathcomp.reals.constructive_ereal]
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]
ltn [def, in mathcomp.boot.ssrnat]