Dirichlet

📁 Source: Mathlib/NumberTheory/LSeries/Dirichlet.lean

Statistics

Metric	Count
Definitions	0
Theorems LSeriesHasSum_zeta, LSeriesSummable_moebius_iff, LSeriesSummable_vonMangoldt, LSeriesSummable_zeta_iff, LSeries_vonMangoldt_eq, LSeries_vonMangoldt_eq_deriv_riemannZeta_div, LSeries_zeta_eq, LSeries_zeta_eq_riemannZeta, LSeries_zeta_mul_Lseries_moebius, LSeries_zeta_ne_zero_of_one_lt_re, abscissaOfAbsConv_moebius, abscissaOfAbsConv_zeta, const_one_eq_zeta, convolution_vonMangoldt_const_one, convolution_vonMangoldt_zeta, not_LSeriesSummable_moebius_at_one, one_eq_delta, mul_mu_eq_one, LSeriesSummable_iff, LSeriesSummable_mul, LSeriesSummable_of_one_lt_re, LSeriesSummable_twist_vonMangoldt, LSeries_modOne_eq, LSeries_ne_zero_of_one_lt_re, LSeries_twist_vonMangoldt_eq, absicssaOfAbsConv_eq_one, apply_eq_toArithmeticFunction_apply, convolution_mul_moebius, convolution_twist_vonMangoldt, delta_mul, isMultiplicative_toArithmeticFunction, modOne_eq_one, modZero_eq_delta, mul_convolution_distrib, mul_delta, not_LSeriesSummable_at_one, abscissaOfAbsConv_one, convolution_one_eq_convolution_zeta, one_convolution_eq_zeta_convolution, LSeriesHasSum_one, LSeriesSummable_one_iff, LSeries_one_eq_riemannZeta, LSeries_one_mul_Lseries_moebius, LSeries_one_ne_zero_of_one_lt_re, riemannZeta_im_eq_zero_of_one_lt, riemannZeta_ne_zero_of_one_lt_re, riemannZeta_pos_of_one_lt, riemannZeta_re_pos_of_one_lt	48
Total	48

ArithmeticFunction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
LSeriesHasSum_zeta 📖	mathematical	Real Real.instLT Real.instOne Complex.re	LSeriesHasSum Complex Complex.instNatCast DFunLike.coe ArithmeticFunction MulZeroClass.toZero Nat.instMulZeroClass instFunLikeNat zeta riemannZeta	—	LSeriesSummable.LSeriesHasSum LSeriesSummable_zeta_iff LSeries_zeta_eq_riemannZeta
LSeriesSummable_moebius_iff 📖	mathematical	—	LSeriesSummable Complex Complex.instIntCast DFunLike.coe ArithmeticFunction MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing instFunLikeNat moebius Real Real.instLT Real.instOne Complex.re	—	not_LSeriesSummable_moebius_at_one LSeriesSummable.of_re_le_re LSeriesSummable_of_bounded_of_one_lt_re Nat.cast_one Complex.norm_intCast Real.instIsStrictOrderedRing Int.cast_one IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike abs_moebius_le_one
LSeriesSummable_vonMangoldt 📖	mathematical	Real Real.instLT Real.instOne Complex.re	LSeriesSummable Complex.ofReal DFunLike.coe ArithmeticFunction Real.instZero instFunLikeNat vonMangoldt	—	LSeriesSummable_logMul_of_lt_re LSeries.abscissaOfAbsConv_one Nat.cast_one LSeriesSummable.eq_1 summable_norm_iff Complex.instFiniteDimensionalReal Summable.of_nonneg_of_le norm_nonneg LSeries.norm_term_le Complex.norm_real abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid vonMangoldt_le_log LE.le.trans Complex.norm_mul CStarRing.norm_of_mem_unitary RCLike.instCStarRing Complex.instNontrivial SubmonoidClass.toOneMemClass Submonoid.instSubmonoidClass mul_one
LSeriesSummable_zeta_iff 📖	mathematical	—	LSeriesSummable Complex Complex.instNatCast DFunLike.coe ArithmeticFunction MulZeroClass.toZero Nat.instMulZeroClass instFunLikeNat zeta Real Real.instLT Real.instOne Complex.re	—	LSeriesSummable_congr const_one_eq_zeta LSeriesSummable_one_iff
LSeries_vonMangoldt_eq 📖	mathematical	Real Real.instLT Real.instOne Complex.re	LSeries Complex.ofReal DFunLike.coe ArithmeticFunction Real.instZero instFunLikeNat vonMangoldt Complex DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instNeg deriv DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.addCommGroup Complex.instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Pi.instOne Complex.instOne	—	LSeries_congr Subsingleton.eq_one Unique.instSubsingleton map_one MonoidHomClass.toOneHomClass MulCharClass.toMonoidHomClass MulChar.instMulCharClass one_mul DirichletCharacter.LSeries_twist_vonMangoldt_eq DirichletCharacter.LSeries_modOne_eq
LSeries_vonMangoldt_eq_deriv_riemannZeta_div 📖	mathematical	Real Real.instLT Real.instOne Complex.re	LSeries Complex.ofReal DFunLike.coe ArithmeticFunction Real.instZero instFunLikeNat vonMangoldt Complex DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instNeg deriv DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.addCommGroup Complex.instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField riemannZeta	—	Filter.EventuallyEq.deriv_eq Filter.eventuallyEq_iff_exists_mem IsOpen.mem_nhds isOpen_lt HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid continuous_const Complex.continuous_re LSeries_one_eq_riemannZeta LSeries_vonMangoldt_eq
LSeries_zeta_eq 📖	mathematical	—	LSeries Complex Complex.instNatCast DFunLike.coe ArithmeticFunction MulZeroClass.toZero Nat.instMulZeroClass instFunLikeNat zeta Pi.instOne Complex.instOne	—	LSeries_congr const_one_eq_zeta
LSeries_zeta_eq_riemannZeta 📖	mathematical	Real Real.instLT Real.instOne Complex.re	LSeries Complex Complex.instNatCast DFunLike.coe ArithmeticFunction MulZeroClass.toZero Nat.instMulZeroClass instFunLikeNat zeta riemannZeta	—	tsum_congr eq_or_ne CharP.cast_eq_zero CharP.ofCharZero Complex.instCharZero Complex.zero_cpow Complex.ne_zero_of_one_lt_re div_zero LSeries.term_of_ne_zero one_div Nat.cast_ite Nat.cast_one zeta_eq_tsum_one_div_nat_cpow
LSeries_zeta_mul_Lseries_moebius 📖	mathematical	Real Real.instLT Real.instOne Complex.re	Complex Complex.instMul LSeries Complex.instNatCast DFunLike.coe ArithmeticFunction MulZeroClass.toZero Nat.instMulZeroClass instFunLikeNat zeta Complex.instIntCast NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing moebius Complex.instOne	—	LSeries_convolution' LSeriesSummable_zeta_iff LSeriesSummable_moebius_iff coe_mul coe_zeta_mul_coe_moebius one_eq_delta LSeries_delta
LSeries_zeta_ne_zero_of_one_lt_re 📖	—	Real Real.instLT Real.instOne Complex.re	—	—	MulZeroClass.zero_mul NeZero.charZero_one Complex.instCharZero LSeries_zeta_mul_Lseries_moebius
abscissaOfAbsConv_moebius 📖	mathematical	—	LSeries.abscissaOfAbsConv Complex Complex.instIntCast DFunLike.coe ArithmeticFunction MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing instFunLikeNat moebius EReal instOneEReal	—	EReal.image_coe_Ioi csInf_Ioo instDenselyOrderedEReal EReal.coe_lt_top
abscissaOfAbsConv_zeta 📖	mathematical	—	LSeries.abscissaOfAbsConv Complex Complex.instNatCast DFunLike.coe ArithmeticFunction MulZeroClass.toZero Nat.instMulZeroClass instFunLikeNat zeta EReal instOneEReal	—	LSeries.abscissaOfAbsConv_congr Nat.cast_one LSeries.abscissaOfAbsConv_one
const_one_eq_zeta 📖	mathematical	—	Pi.instOne AddMonoidWithOne.toOne AddMonoidWithOne.toNatCast	—	Nat.cast_one
convolution_vonMangoldt_const_one 📖	mathematical	—	LSeries.convolution Complex Complex.instSemiring Complex.ofReal DFunLike.coe ArithmeticFunction Real Real.instZero instFunLikeNat vonMangoldt Pi.instOne Complex.instOne Complex.log Complex.instNatCast	—	LSeries.convolution_one_eq_convolution_zeta convolution_vonMangoldt_zeta
convolution_vonMangoldt_zeta 📖	mathematical	—	LSeries.convolution Complex Complex.instSemiring Complex.ofReal DFunLike.coe ArithmeticFunction Real Real.instZero instFunLikeNat vonMangoldt Complex.instNatCast MulZeroClass.toZero Nat.instMulZeroClass zeta Complex.log	—	CharP.cast_eq_zero CharP.ofCharZero Complex.instCharZero Nat.cast_one LSeries.convolution_def Finset.sum_congr MulZeroClass.mul_zero mul_one RCLike.charZero_rclike Complex.ofReal_sum Complex.natCast_log vonMangoldt_mul_zeta
not_LSeriesSummable_moebius_at_one 📖	mathematical	—	LSeriesSummable Complex Complex.instIntCast DFunLike.coe ArithmeticFunction MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing instFunLikeNat moebius Complex.instOne	—	not_summable_one_div_on_primes Complex.summable_ofReal Summable.of_neg SeminormedAddCommGroup.toIsTopologicalAddGroup Summable.congr Summable.indicator SeminormedAddCommGroup.to_isUniformAddGroup Complex.instCompleteSpace Set.indicator_of_mem LSeries.term_of_ne_zero Nat.Prime.ne_zero moebius_apply_prime Int.cast_neg Int.cast_one Complex.cpow_one neg_div one_div Complex.ofReal_inv Set.indicator_of_notMem neg_zero
one_eq_delta 📖	mathematical	—	DFunLike.coe ArithmeticFunction Complex Complex.instZero instFunLikeNat one Complex.instOne LSeries.delta	—	—

DirichletCharacter

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
LSeriesSummable_iff 📖	mathematical	—	LSeriesSummable DFunLike.coe DirichletCharacter Complex CommGroupWithZero.toCommMonoidWithZero Semifield.toCommGroupWithZero Field.toSemifield Complex.instField ZMod MulChar.instFunLike CommRing.toCommMonoid ZMod.commRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Real Real.instLT Real.instOne Complex.re	—	not_LSeriesSummable_at_one LSeriesSummable.of_re_le_re LSeriesSummable_of_one_lt_re
LSeriesSummable_mul 📖	mathematical	LSeriesSummable	Pi.instMul Complex Complex.instMul DFunLike.coe DirichletCharacter CommGroupWithZero.toCommMonoidWithZero Semifield.toCommGroupWithZero Field.toSemifield Complex.instField ZMod MulChar.instFunLike CommRing.toCommMonoid ZMod.commRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	Summable.of_norm Complex.instCompleteSpace Summable.of_nonneg_of_le norm_nonneg LSeries.norm_term_le Complex.norm_mul mul_le_of_le_one_left IsOrderedRing.toMulPosMono Real.instIsOrderedRing norm_le_one Summable.norm Complex.instFiniteDimensionalReal
LSeriesSummable_of_one_lt_re 📖	mathematical	Real Real.instLT Real.instOne Complex.re	LSeriesSummable DFunLike.coe DirichletCharacter Complex CommGroupWithZero.toCommMonoidWithZero Semifield.toCommGroupWithZero Field.toSemifield Complex.instField ZMod MulChar.instFunLike CommRing.toCommMonoid ZMod.commRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	LSeriesSummable_of_bounded_of_one_lt_re norm_le_one
LSeriesSummable_twist_vonMangoldt 📖	mathematical	Real Real.instLT Real.instOne Complex.re	LSeriesSummable Pi.instMul Complex Complex.instMul DFunLike.coe DirichletCharacter CommGroupWithZero.toCommMonoidWithZero Semifield.toCommGroupWithZero Field.toSemifield Complex.instField ZMod MulChar.instFunLike CommRing.toCommMonoid ZMod.commRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Complex.ofReal ArithmeticFunction Real.instZero ArithmeticFunction.instFunLikeNat ArithmeticFunction.vonMangoldt	—	LSeriesSummable_mul ArithmeticFunction.LSeriesSummable_vonMangoldt
LSeries_modOne_eq 📖	mathematical	—	LSeries DFunLike.coe DirichletCharacter Complex CommGroupWithZero.toCommMonoidWithZero Semifield.toCommGroupWithZero Field.toSemifield Complex.instField ZMod MulChar.instFunLike CommRing.toCommMonoid ZMod.commRing MulChar.hasOne AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Pi.instOne Complex.instOne	—	modOne_eq_one
LSeries_ne_zero_of_one_lt_re 📖	—	Real Real.instLT Real.instOne Complex.re	—	—	MulZeroClass.zero_mul NeZero.charZero_one Complex.instCharZero LSeries.mul_mu_eq_one
LSeries_twist_vonMangoldt_eq 📖	mathematical	Real Real.instLT Real.instOne Complex.re	LSeries Pi.instMul Complex Complex.instMul DFunLike.coe DirichletCharacter CommGroupWithZero.toCommMonoidWithZero Semifield.toCommGroupWithZero Field.toSemifield Complex.instField ZMod MulChar.instFunLike CommRing.toCommMonoid ZMod.commRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Complex.ofReal ArithmeticFunction Real.instZero ArithmeticFunction.instFunLikeNat ArithmeticFunction.vonMangoldt DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instNeg deriv DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.addCommGroup Complex.instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField	—	eq_or_ne modZero_eq_delta LSeries.delta_mul_eq_smul_delta ArithmeticFunction.vonMangoldt_apply_one zero_smul LSeries_zero LSeries_delta deriv_one neg_zero div_one LSeriesSummable_iff absicssaOfAbsConv_eq_one EReal.coe_one EReal.coe_lt_coe_iff LSeriesSummable_twist_vonMangoldt eq_div_iff LSeries_ne_zero_of_one_lt_re LSeries_convolution' convolution_twist_vonMangoldt LSeries_deriv neg_neg LSeries_congr mul_comm
absicssaOfAbsConv_eq_one 📖	mathematical	—	LSeries.abscissaOfAbsConv DFunLike.coe DirichletCharacter Complex CommGroupWithZero.toCommMonoidWithZero Semifield.toCommGroupWithZero Field.toSemifield Complex.instField ZMod MulChar.instFunLike CommRing.toCommMonoid ZMod.commRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing EReal instOneEReal	—	LSeriesSummable_iff EReal.image_coe_Ioi csInf_Ioo instDenselyOrderedEReal EReal.coe_lt_top
apply_eq_toArithmeticFunction_apply 📖	mathematical	—	DFunLike.coe DirichletCharacter ZMod MulChar.instFunLike CommRing.toCommMonoid ZMod.commRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing ArithmeticFunction MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero ArithmeticFunction.instFunLikeNat toArithmeticFunction	—	—
convolution_mul_moebius 📖	mathematical	—	LSeries.convolution Complex Complex.instSemiring DFunLike.coe DirichletCharacter CommGroupWithZero.toCommMonoidWithZero Semifield.toCommGroupWithZero Field.toSemifield Complex.instField ZMod MulChar.instFunLike CommRing.toCommMonoid ZMod.commRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Pi.instMul Complex.instMul Complex.instIntCast ArithmeticFunction MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing ArithmeticFunction.instFunLikeNat ArithmeticFunction.moebius LSeries.delta	—	LSeries.one_convolution_eq_zeta_convolution ArithmeticFunction.one_eq_delta ArithmeticFunction.coe_mul ArithmeticFunction.coe_zeta_mul_coe_moebius mul_one mul_convolution_distrib mul_delta
convolution_twist_vonMangoldt 📖	mathematical	—	LSeries.convolution Complex Complex.instSemiring Pi.instMul Complex.instMul DFunLike.coe DirichletCharacter CommGroupWithZero.toCommMonoidWithZero Semifield.toCommGroupWithZero Field.toSemifield Complex.instField ZMod MulChar.instFunLike CommRing.toCommMonoid ZMod.commRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Complex.ofReal ArithmeticFunction Real Real.instZero ArithmeticFunction.instFunLikeNat ArithmeticFunction.vonMangoldt Complex.log Complex.instNatCast	—	ArithmeticFunction.convolution_vonMangoldt_const_one mul_convolution_distrib mul_one
delta_mul 📖	mathematical	—	Pi.instMul Complex Complex.instMul LSeries.delta DFunLike.coe DirichletCharacter CommGroupWithZero.toCommMonoidWithZero Semifield.toCommGroupWithZero Field.toSemifield Complex.instField ZMod MulChar.instFunLike CommRing.toCommMonoid ZMod.commRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	mul_delta mul_comm
isMultiplicative_toArithmeticFunction 📖	mathematical	—	ArithmeticFunction.IsMultiplicative CommMonoidWithZero.toMonoidWithZero toArithmeticFunction MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass DFunLike.coe DirichletCharacter ZMod MulChar.instFunLike CommRing.toCommMonoid ZMod.commRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	ArithmeticFunction.IsMultiplicative.iff_ne_zero Nat.cast_one map_one MonoidHomClass.toOneHomClass MulCharClass.toMonoidHomClass MulChar.instMulCharClass IsStrictOrderedRing.noZeroDivisors Nat.instIsStrictOrderedRing StarOrderedRing.toExistsAddOfLE Nat.instStarOrderedRing Nat.cast_mul map_mul MonoidHomClass.toMulHomClass
modOne_eq_one 📖	mathematical	—	DFunLike.coe DirichletCharacter ZMod MulChar.instFunLike CommRing.toCommMonoid ZMod.commRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Pi.instOne MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass CommMonoidWithZero.toMonoidWithZero	—	level_one MulChar.one_apply isUnit_of_subsingleton Unique.instSubsingleton Pi.one_apply
modZero_eq_delta 📖	mathematical	—	DFunLike.coe DirichletCharacter Complex CommGroupWithZero.toCommMonoidWithZero Semifield.toCommGroupWithZero Field.toSemifield Complex.instField ZMod MulChar.instFunLike CommRing.toCommMonoid ZMod.commRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing LSeries.delta	—	eq_or_ne Nat.cast_zero MulChar.map_nonunit not_isUnit_zero ZMod.nontrivial' Nat.cast_one map_one MonoidHomClass.toOneHomClass MulCharClass.toMonoidHomClass MulChar.instMulCharClass ZMod.eq_one_of_isUnit_natCast
mul_convolution_distrib 📖	mathematical	—	LSeries.convolution CommSemiring.toSemiring Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DFunLike.coe DirichletCharacter CommSemiring.toCommMonoidWithZero ZMod MulChar.instFunLike CommRing.toCommMonoid ZMod.commRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	LSeries.convolution_def Finset.sum_congr Finset.mul_sum Nat.mem_divisorsAntidiagonal Nat.cast_mul map_mul MonoidHomClass.toMulHomClass MulCharClass.toMonoidHomClass MulChar.instMulCharClass mul_mul_mul_comm
mul_delta 📖	mathematical	—	Pi.instMul Complex Complex.instMul DFunLike.coe DirichletCharacter CommGroupWithZero.toCommMonoidWithZero Semifield.toCommGroupWithZero Field.toSemifield Complex.instField ZMod MulChar.instFunLike CommRing.toCommMonoid ZMod.commRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing LSeries.delta	—	LSeries.mul_delta Nat.cast_one map_one MonoidHomClass.toOneHomClass MulCharClass.toMonoidHomClass MulChar.instMulCharClass
not_LSeriesSummable_at_one 📖	mathematical	—	LSeriesSummable DFunLike.coe DirichletCharacter Complex CommGroupWithZero.toCommMonoidWithZero Semifield.toCommGroupWithZero Field.toSemifield Complex.instField ZMod MulChar.instFunLike CommRing.toCommMonoid ZMod.commRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Complex.instOne	—	Real.not_summable_indicator_one_div_natCast Summable.of_nonneg_of_le Set.indicator_apply_nonneg Mathlib.Meta.Positivity.div_nonneg_of_pos_of_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing Mathlib.Meta.Positivity.pos_of_isNat Real.instIsOrderedRing Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Nat.cast_nonneg' IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass LSeries.norm_term_eq CharP.cast_eq_zero CharP.ofCharZero RCLike.charZero_rclike div_zero one_div MulChar.map_one CStarRing.norm_of_mem_unitary RCLike.instCStarRing Complex.instNontrivial SubmonoidClass.toOneMemClass Submonoid.instSubmonoidClass Real.rpow_one Mathlib.Meta.Positivity.nonneg_of_isNat Nat.cast_zero Mathlib.Meta.Positivity.div_nonneg_of_nonneg_of_pos norm_nonneg Real.rpow_pos_of_pos Nat.cast_pos' NeZero.charZero_one lt_of_le_of_ne' zero_le Nat.instCanonicallyOrderedAdd Summable.norm Complex.instFiniteDimensionalReal

DirichletCharacter.LSeries

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mul_mu_eq_one 📖	mathematical	Real Real.instLT Real.instOne Complex.re	Complex Complex.instMul LSeries DFunLike.coe DirichletCharacter CommGroupWithZero.toCommMonoidWithZero Semifield.toCommGroupWithZero Field.toSemifield Complex.instField ZMod MulChar.instFunLike CommRing.toCommMonoid ZMod.commRing AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Pi.instMul Complex.instIntCast ArithmeticFunction MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing ArithmeticFunction.instFunLikeNat ArithmeticFunction.moebius Complex.instOne	—	LSeries_convolution' DirichletCharacter.LSeriesSummable_of_one_lt_re DirichletCharacter.LSeriesSummable_mul ArithmeticFunction.LSeriesSummable_moebius_iff DirichletCharacter.convolution_mul_moebius LSeries_delta Pi.one_apply

LSeries

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abscissaOfAbsConv_one 📖	mathematical	—	abscissaOfAbsConv Pi.instOne Complex Complex.instOne EReal instOneEReal	—	DirichletCharacter.absicssaOfAbsConv_eq_one one_ne_zero DirichletCharacter.modOne_eq_one
convolution_one_eq_convolution_zeta 📖	mathematical	—	convolution Pi.instOne AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring AddMonoidWithOne.toNatCast DFunLike.coe ArithmeticFunction MulZeroClass.toZero Nat.instMulZeroClass ArithmeticFunction.instFunLikeNat ArithmeticFunction.zeta	—	convolution_congr ArithmeticFunction.const_one_eq_zeta
one_convolution_eq_zeta_convolution 📖	mathematical	—	convolution Pi.instOne AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring AddMonoidWithOne.toNatCast DFunLike.coe ArithmeticFunction MulZeroClass.toZero Nat.instMulZeroClass ArithmeticFunction.instFunLikeNat ArithmeticFunction.zeta	—	convolution_congr ArithmeticFunction.const_one_eq_zeta

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
LSeriesHasSum_one 📖	mathematical	Real Real.instLT Real.instOne Complex.re	LSeriesHasSum Pi.instOne Complex Complex.instOne riemannZeta	—	LSeriesSummable.LSeriesHasSum LSeriesSummable_one_iff LSeries_one_eq_riemannZeta
LSeriesSummable_one_iff 📖	mathematical	—	LSeriesSummable Pi.instOne Complex Complex.instOne Real Real.instLT Real.instOne Complex.re	—	DirichletCharacter.LSeriesSummable_iff one_ne_zero DirichletCharacter.modOne_eq_one
LSeries_one_eq_riemannZeta 📖	mathematical	Real Real.instLT Real.instOne Complex.re	LSeries Pi.instOne Complex Complex.instOne riemannZeta	—	ArithmeticFunction.LSeries_zeta_eq_riemannZeta ArithmeticFunction.LSeries_zeta_eq
LSeries_one_mul_Lseries_moebius 📖	mathematical	Real Real.instLT Real.instOne Complex.re	Complex Complex.instMul LSeries Pi.instOne Complex.instOne Complex.instIntCast DFunLike.coe ArithmeticFunction MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Int.instCommRing ArithmeticFunction.instFunLikeNat ArithmeticFunction.moebius	—	ArithmeticFunction.LSeries_zeta_mul_Lseries_moebius ArithmeticFunction.LSeries_zeta_eq
LSeries_one_ne_zero_of_one_lt_re 📖	—	Real Real.instLT Real.instOne Complex.re	—	—	ArithmeticFunction.LSeries_zeta_ne_zero_of_one_lt_re ArithmeticFunction.LSeries_zeta_eq
riemannZeta_im_eq_zero_of_one_lt 📖	mathematical	Real Real.instLT Real.instOne	Complex.im riemannZeta Complex.ofReal Real.instZero	—	Complex.pos_iff riemannZeta_pos_of_one_lt
riemannZeta_ne_zero_of_one_lt_re 📖	—	Real Real.instLT Real.instOne Complex.re	—	—	LSeries_one_ne_zero_of_one_lt_re LSeries_one_eq_riemannZeta
riemannZeta_pos_of_one_lt 📖	mathematical	Real Real.instLT Real.instOne	Complex Preorder.toLT PartialOrder.toPreorder Complex.partialOrder Complex.instZero riemannZeta Complex.ofReal	—	LSeries_one_eq_riemannZeta LSeries.positive RCLike.toZeroLEOneClass NeZero.charZero_one Complex.instCharZero LSeries.abscissaOfAbsConv_one Nat.cast_one
riemannZeta_re_pos_of_one_lt 📖	mathematical	Real Real.instLT Real.instOne	Real.instZero Complex.re riemannZeta Complex.ofReal	—	Complex.pos_iff riemannZeta_pos_of_one_lt

---

← Back to Index