Theorems · Theorem · number theory
riemannZeta_one
riemannZeta 1 = (↑Real.eulerMascheroniConstant - Complex.log (4 * ↑Real.pi)) / 2
Formula for ζ 1. Note that mathematically ζ 1 is undefined, but our construction ascribes
this particular value to it.
- Defined in
- Mathlib.NumberTheory.Harmonic.ZetaAsymp
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 309 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites18
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Complexstatement and proof · cited by 5,565
- nhdsproof · cited by 5,554
- Filter.Tendstoproof · cited by 3,814
- Compl.complproof · cited by 2,925
- nhdsWithinproof · cited by 1,912
- Real.pistatement · cited by 1,774
- Complex.ofRealstatement · cited by 1,654
- Complex.logstatement · cited by 187
- nhdsWithin_le_nhdsproof · cited by 145
- Filter.Tendsto.mono_leftproof · cited by 125
- tendsto_nhds_uniqueproof · cited by 118
- riemannZetastatement and proof · cited by 85
Cited by3
Results whose statement or proof uses this declaration.
- completedRiemannZeta_oneproof · cited by 1
- riemannZeta_one_ne_zeroproof · cited by 1
- riemannZeta_conjproof · cited by 0