RiemannZeta

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

Statistics

Metric	Count
Definitions RiemannHypothesis, completedRiemannZeta, completedRiemannZeta₀, riemannZeta	4
Theorems completedCosZeta_zero, completedCosZeta₀_zero, completedHurwitzZetaEven_zero, completedHurwitzZetaEven₀_zero, cosZeta_zero, expZeta_zero, hurwitzZetaEven_zero, hurwitzZeta_zero, completedRiemannZeta_eq, completedRiemannZeta_one_sub, completedRiemannZeta_residue_one, completedRiemannZeta₀_one_sub, completedZeta_eq_tsum_of_one_lt_re, differentiableAt_completedZeta, differentiableAt_riemannZeta, differentiable_completedZeta₀, riemannZeta_def_of_ne_zero, riemannZeta_neg_two_mul_nat_add_one, riemannZeta_one_sub, riemannZeta_residue_one, riemannZeta_zero, tendsto_sub_mul_tsum_nat_cpow, tendsto_sub_mul_tsum_nat_rpow, two_mul_riemannZeta_eq_tsum_int_inv_pow_of_even, zeta_eq_tsum_one_div_nat_add_one_cpow, zeta_eq_tsum_one_div_nat_cpow, zeta_nat_eq_tsum_of_gt_one	27
Total	31

HurwitzZeta

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
completedCosZeta_zero 📖	mathematical	—	completedCosZeta UnitAddCircle NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid QuotientAddGroup.Quotient.addCommGroup Real Real.instAddCommGroup AddSubgroup.zmultiples AddCommGroup.toAddGroup Real.instOne completedRiemannZeta	—	completedRiemannZeta.eq_1 completedHurwitzZetaEven.eq_1 completedCosZeta.eq_1 hurwitzEvenFEPair_zero_symm
completedCosZeta₀_zero 📖	mathematical	—	completedCosZeta₀ UnitAddCircle NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid QuotientAddGroup.Quotient.addCommGroup Real Real.instAddCommGroup AddSubgroup.zmultiples AddCommGroup.toAddGroup Real.instOne completedRiemannZeta₀	—	completedRiemannZeta₀.eq_1 completedHurwitzZetaEven₀.eq_1 completedCosZeta₀.eq_1 hurwitzEvenFEPair_zero_symm
completedHurwitzZetaEven_zero 📖	mathematical	—	completedHurwitzZetaEven UnitAddCircle NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid QuotientAddGroup.Quotient.addCommGroup Real Real.instAddCommGroup AddSubgroup.zmultiples AddCommGroup.toAddGroup Real.instOne completedRiemannZeta	—	—
completedHurwitzZetaEven₀_zero 📖	mathematical	—	completedHurwitzZetaEven₀ UnitAddCircle NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid QuotientAddGroup.Quotient.addCommGroup Real Real.instAddCommGroup AddSubgroup.zmultiples AddCommGroup.toAddGroup Real.instOne completedRiemannZeta₀	—	—
cosZeta_zero 📖	mathematical	—	cosZeta UnitAddCircle NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid QuotientAddGroup.Quotient.addCommGroup Real Real.instAddCommGroup AddSubgroup.zmultiples AddCommGroup.toAddGroup Real.instOne riemannZeta	—	completedCosZeta_zero
expZeta_zero 📖	mathematical	—	expZeta UnitAddCircle NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid QuotientAddGroup.Quotient.addCommGroup Real Real.instAddCommGroup AddSubgroup.zmultiples AddCommGroup.toAddGroup Real.instOne riemannZeta	—	expZeta.eq_1 cosZeta_zero add_eq_left AddLeftCancelSemigroup.toIsLeftCancelAdd mul_eq_zero NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass eq_false_intro Complex.I_ne_zero CharZero.eq_neg_self_iff Complex.instCharZero sinZeta_neg neg_zero
hurwitzZetaEven_zero 📖	mathematical	—	hurwitzZetaEven UnitAddCircle NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid QuotientAddGroup.Quotient.addCommGroup Real Real.instAddCommGroup AddSubgroup.zmultiples AddCommGroup.toAddGroup Real.instOne riemannZeta	—	—
hurwitzZeta_zero 📖	mathematical	—	hurwitzZeta UnitAddCircle NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid QuotientAddGroup.Quotient.addCommGroup Real Real.instAddCommGroup AddSubgroup.zmultiples AddCommGroup.toAddGroup Real.instOne riemannZeta	—	AddLeftCancelSemigroup.toIsLeftCancelAdd neg_zero NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Complex.instCharZero hurwitzZetaOdd_neg

(root)

Definitions

Name	Category	Theorems
RiemannHypothesis 📖	MathDef	—
completedRiemannZeta 📖	CompOp	11 math math: completedZeta_eq_tsum_of_one_lt_re, completedRiemannZeta_eq, HurwitzZeta.completedHurwitzZetaEven_zero, HurwitzZeta.completedCosZeta_zero, differentiableAt_completedZeta, completedRiemannZeta_residue_one, completedRiemannZeta_one, riemannZeta_def_of_ne_zero, DirichletCharacter.completedLFunction_modOne_eq, ZMod.completedLFunction_modOne_eq, completedRiemannZeta_one_sub
completedRiemannZeta₀ 📖	CompOp	6 math math: completedRiemannZeta_eq, HurwitzZeta.completedCosZeta₀_zero, completedRiemannZeta₀_one, HurwitzZeta.completedHurwitzZetaEven₀_zero, completedRiemannZeta₀_one_sub, differentiable_completedZeta₀
riemannZeta 📖	CompOp	48 math math: HurwitzZeta.expZeta_zero, EisensteinSeries.hasSum_e2Summand_symmetricIcc, ZMod.LFunction_modOne_eq, tsum_eisSummand_eq_riemannZeta_mul_eisensteinSeries, two_mul_riemannZeta_eq_tsum_int_inv_pow_of_even, riemannZeta_two, HurwitzZeta.hurwitzZetaEven_zero, EisensteinSeries.E2_slash_action, DirichletCharacter.LFunction_modOne_eq, riemannZeta_one_sub, riemannZeta_im_eq_zero_of_one_lt, riemannZeta_four, tendsto_riemannZeta_sub_one_div, riemannZeta_eulerProduct_exp_log, zeta_eq_tsum_one_div_nat_cpow, ArithmeticFunction.LSeries_vonMangoldt_eq_deriv_riemannZeta_div, ZetaAsymptotics.tendsto_riemannZeta_sub_one_div_Gammaℝ, riemannZeta_neg_two_mul_nat_add_one, EisensteinSeries.hasSum_e2Summand_symmetricIco, EisensteinSeries.q_expansion_riemannZeta, DirichletCharacter.LFunctionTrivChar_eq_mul_riemannZeta, isBigO_riemannZeta_sub_one_div, EisensteinSeries.e2Summand_zero_eq_two_riemannZeta_two, tsum_riemannZetaSummand, riemannZeta_zero, LSeries_one_eq_riemannZeta, HurwitzZeta.cosZeta_zero, riemannZeta_pos_of_one_lt, zeta_eq_tsum_one_div_nat_add_one_cpow, riemannZeta_one, differentiableAt_riemannZeta, riemannZeta_eulerProduct, ArithmeticFunction.LSeries_zeta_eq_riemannZeta, HurwitzZeta.hurwitzZeta_zero, LSeriesHasSum_one, riemannZeta_re_pos_of_one_lt, EisensteinSeries.G2_eq_tsum_cexp, ArithmeticFunction.LSeriesHasSum_zeta, tsum_eisSummand_eq_tsum_sigma_mul_cexp_pow, riemannZeta_neg_nat_eq_bernoulli', riemannZeta_def_of_ne_zero, riemannZeta_eulerProduct_tprod, riemannZeta_residue_one, riemannZeta_neg_nat_eq_bernoulli, riemannZeta_two_mul_nat, zeta_nat_eq_tsum_of_gt_one, riemannZeta_eulerProduct_hasProd, ZetaAsymptotics.tendsto_riemannZeta_sub_one_div_nhds_right

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
completedRiemannZeta_eq 📖	mathematical	—	completedRiemannZeta Complex Complex.instSub completedRiemannZeta₀ DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instOne	—	HurwitzZeta.completedHurwitzZetaEven_eq
completedRiemannZeta_one_sub 📖	mathematical	—	completedRiemannZeta Complex Complex.instSub Complex.instOne	—	HurwitzZeta.completedHurwitzZetaEven_zero HurwitzZeta.completedCosZeta_zero HurwitzZeta.completedHurwitzZetaEven_one_sub
completedRiemannZeta_residue_one 📖	mathematical	—	Filter.Tendsto Complex Complex.instMul Complex.instSub Complex.instOne completedRiemannZeta nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Compl.compl Set Set.instCompl Set.instSingletonSet nhds	—	HurwitzZeta.completedHurwitzZetaEven_residue_one
completedRiemannZeta₀_one_sub 📖	mathematical	—	completedRiemannZeta₀ Complex Complex.instSub Complex.instOne	—	HurwitzZeta.completedHurwitzZetaEven₀_zero HurwitzZeta.completedCosZeta₀_zero HurwitzZeta.completedHurwitzZetaEven₀_one_sub
completedZeta_eq_tsum_of_one_lt_re 📖	mathematical	Real Real.instLT Real.instOne Complex.re	completedRiemannZeta Complex Complex.instMul Complex.instPow Complex.ofReal Real.pi DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instNeg instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.Gamma tsum ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Complex.instOne SummationFilter.unconditional	—	Nat.instAtLeastTwoHAddOfNat HasSum.tsum_eq Complex.instT2Space SummationFilter.instNeBotUnconditional HurwitzZeta.hasSum_nat_completedCosZeta HurwitzZeta.completedCosZeta_zero MulZeroClass.mul_zero MulZeroClass.zero_mul Real.cos_zero mul_one IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing mul_one_div Nat.cast_zero Complex.zero_cpow Complex.ne_zero_of_one_lt_re div_zero
differentiableAt_completedZeta 📖	mathematical	—	DifferentiableAt Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.addCommGroup Complex.instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField completedRiemannZeta	—	HurwitzZeta.differentiableAt_completedHurwitzZetaEven
differentiableAt_riemannZeta 📖	mathematical	—	DifferentiableAt Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.addCommGroup Complex.instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField riemannZeta	—	HurwitzZeta.differentiableAt_hurwitzZetaEven
differentiable_completedZeta₀ 📖	mathematical	—	Differentiable Complex DenselyNormedField.toNontriviallyNormedField Complex.instDenselyNormedField Complex.addCommGroup Complex.instModuleSelf UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField completedRiemannZeta₀	—	HurwitzZeta.differentiable_completedHurwitzZetaEven₀
riemannZeta_def_of_ne_zero 📖	mathematical	—	riemannZeta Complex DivInvMonoid.toDiv Complex.instDivInvMonoid completedRiemannZeta Complex.Gammaℝ	—	riemannZeta.eq_1 HurwitzZeta.hurwitzZetaEven.eq_1 Function.update_of_ne HurwitzZeta.completedHurwitzZetaEven_zero
riemannZeta_neg_two_mul_nat_add_one 📖	mathematical	—	riemannZeta Complex Complex.instMul Complex.instNeg instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.instAdd Complex.instOne Complex.instZero	—	HurwitzZeta.hurwitzZetaEven_neg_two_mul_nat_add_one
riemannZeta_one_sub 📖	mathematical	—	riemannZeta Complex Complex.instSub Complex.instOne Complex.instMul instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat Complex.instPow Complex.ofReal Real.pi Complex.instNeg Complex.Gamma Complex.cos DivInvMonoid.toDiv Complex.instDivInvMonoid	—	Nat.instAtLeastTwoHAddOfNat riemannZeta.eq_1 HurwitzZeta.hurwitzZetaEven_one_sub HurwitzZeta.cosZeta_zero HurwitzZeta.hurwitzZetaEven_zero
riemannZeta_residue_one 📖	mathematical	—	Filter.Tendsto Complex Complex.instMul Complex.instSub Complex.instOne riemannZeta nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField Compl.compl Set Set.instCompl Set.instSingletonSet nhds	—	HurwitzZeta.hurwitzZetaEven_residue_one
riemannZeta_zero 📖	mathematical	—	riemannZeta Complex Complex.instZero DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instNeg Complex.instOne instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat Function.update.congr_simp Function.update_self
tendsto_sub_mul_tsum_nat_cpow 📖	mathematical	—	Filter.Tendsto Complex Complex.instMul Complex.instSub Complex.instOne tsum ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instPow Complex.instNatCast SummationFilter.unconditional nhdsWithin setOf Real Real.instLT Real.instOne Complex.re nhds	—	Filter.Tendsto.congr' Filter.mp_mem eventually_mem_nhdsWithin Filter.univ_mem' zeta_eq_tsum_one_div_nat_cpow tendsto_nhdsWithin_mono_left riemannZeta_residue_one
tendsto_sub_mul_tsum_nat_rpow 📖	mathematical	—	Filter.Tendsto Real Real.instMul Real.instSub Real.instOne tsum Real.instAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace DivInvMonoid.toDiv Real.instDivInvMonoid Real.instPow Real.instNatCast SummationFilter.unconditional nhdsWithin Set.Ioi Real.instPreorder nhds	—	Filter.tendsto_ofReal_iff Complex.ofReal_one ContinuousWithinAt.tendsto_nhdsWithin Continuous.continuousWithinAt Complex.continuous_ofReal Filter.Tendsto.congr one_div Complex.ofReal_mul Complex.ofReal_sub Complex.ofReal_tsum Complex.ofReal_inv Complex.ofReal_cpow Nat.cast_nonneg Real.instIsOrderedRing Filter.Tendsto.comp tendsto_sub_mul_tsum_nat_cpow
two_mul_riemannZeta_eq_tsum_int_inv_pow_of_even 📖	mathematical	Even	Complex Complex.instMul instOfNatAtLeastTwo Complex.instNatCast Nat.instAtLeastTwoHAddOfNat riemannZeta tsum ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup Complex.instInv Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring Complex.instIntCast SummationFilter.unconditional	—	lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.cast_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Int.instIsStrictOrderedRing neg_neg_of_pos Int.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Tactic.Linarith.sub_nonpos_of_le IsStrictOrderedRing.toIsOrderedRing Nat.cast_one tsum_int_eq_zero_add_two_mul_tsum_pnat SeminormedAddCommGroup.to_isUniformAddGroup Complex.instCompleteSpace Complex.instT2Space Int.cast_neg Even.neg_pow Summable.of_norm Summable.of_nat_of_neg instIsTopologicalAddGroupReal Int.cast_natCast norm_inv norm_pow NormedDivisionRing.to_normOneClass NormedDivisionRing.toNormMulClass RCLike.norm_natCast norm_neg isReduced_of_noZeroDivisors NormMulClass.toNoZeroDivisors Complex.instNontrivial Nat.cast_zero zeta_eq_tsum_one_div_nat_add_one_cpow IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass RCLike.charZero_rclike Complex.cpow_natCast one_div Nat.cast_pow CharP.cast_eq_zero CharP.ofCharZero Complex.instCharZero tsum_pnat_eq_tsum_succ Nat.cast_add nsmul_eq_mul zero_add
zeta_eq_tsum_one_div_nat_add_one_cpow 📖	mathematical	Real Real.instLT Real.instOne Complex.re	riemannZeta tsum Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instOne Complex.instPow Complex.instAdd Complex.instNatCast SummationFilter.unconditional	—	zeta_eq_tsum_one_div_nat_cpow one_div CharP.cast_eq_zero CharP.ofCharZero Complex.instCharZero Complex.zero_cpow Complex.ne_zero_of_one_lt_re div_zero Nat.cast_add Nat.cast_one zero_add Summable.tsum_eq_zero_add SeminormedAddCommGroup.toIsTopologicalAddGroup Complex.instT2Space Complex.summable_one_div_nat_cpow
zeta_eq_tsum_one_div_nat_cpow 📖	mathematical	Real Real.instLT Real.instOne Complex.re	riemannZeta tsum Complex ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instOne Complex.instPow Complex.instNatCast SummationFilter.unconditional	—	Nat.instAtLeastTwoHAddOfNat HurwitzZeta.cosZeta_zero MulZeroClass.mul_zero MulZeroClass.zero_mul Real.cos_zero HasSum.tsum_eq Complex.instT2Space SummationFilter.instNeBotUnconditional HurwitzZeta.hasSum_nat_cosZeta
zeta_nat_eq_tsum_of_gt_one 📖	mathematical	—	riemannZeta Complex Complex.instNatCast tsum ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing Complex.instNormedField ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Complex.instNormedAddCommGroup DivInvMonoid.toDiv Complex.instDivInvMonoid Complex.instOne Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Complex.instSemiring SummationFilter.unconditional	—	zeta_eq_tsum_one_div_nat_cpow Complex.ofReal_natCast Complex.ofReal_re Nat.cast_one Nat.cast_lt IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass RCLike.charZero_rclike Complex.cpow_natCast

---

← Back to Index