ExpLog

📁 Source: Mathlib/NumberTheory/EulerProduct/ExpLog.lean

Statistics

Metric	Count
Definitions	0
Theorems exp_tsum_primes_log_eq_tsum, clog_one_sub	2
Total	2

EulerProduct

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exp_tsum_primes_log_eq_tsum 📖	mathematical	Summable Real Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Norm.norm Complex Complex.instNorm DFunLike.coe MonoidWithZeroHom Nat.instMulZeroOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Complex.instSemiring MonoidWithZeroHom.funLike SummationFilter.unconditional	Complex.exp tsum Nat.Primes ESeminormedAddCommMonoid.toAddCommMonoid SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Complex.instNeg Complex.log Complex.instSub Complex.instOne Nat.Prime	—	Summable.norm_lt_one Complex.instCompleteSpace Summable.of_norm LT.lt.false Nat.Prime.one_lt Subtype.prop sub_eq_zero NormOneClass.norm_one NormedDivisionRing.to_normOneClass HasProd.tprod_eq Complex.instT2Space SummationFilter.instNeBotUnconditional HasSum.cexp Summable.hasSum Summable.subtype SeminormedAddCommGroup.to_isUniformAddGroup Summable.neg SeminormedAddCommGroup.toIsTopologicalAddGroup Summable.clog_one_sub Complex.exp_neg Complex.exp_log eulerProduct_completely_multiplicative_tprod

Summable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
clog_one_sub 📖	mathematical	Summable Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup SummationFilter.unconditional	Complex.log Complex.instSub Complex.instOne	—	Complex.one_mem_slitPlane sub_zero DifferentiableAt.fun_comp' Complex.differentiableAt_log DifferentiableAt.const_sub differentiableAt_id Complex.log_one DifferentiableAt.isBigO_sub Asymptotics.IsBigO.comp_summable Complex.instFiniteDimensionalReal Complex.instCompleteSpace

---

← Back to Index