Theorems · Definition · number theory
harmonic
ℕ → ℚ
The nth-harmonic number defined as a finset sum of consecutive reciprocals.
- Defined in
- Mathlib.NumberTheory.Harmonic.Defs
- Cited by
- 27 results in Mathlib
- Foundations
- Depth 74 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finset.sumproof · cited by 5,195
- Finset.rangeproof · cited by 1,341
Cited by29
Results whose statement or proof uses this declaration.
- Real.eulerMascheroniSeq'proof · cited by 9
- harmonic_succstatement · cited by 8
- Real.eulerMascheroniSeqproof · cited by 7
- harmonic_posstatement · cited by 3
- Real.strictMono_eulerMascheroniSeqproof · cited by 3
- Real.tendsto_eulerMascheroniSeq'proof · cited by 3
- Complex.hasDerivAt_Gamma_oneproof · cited by 3
- Real.hasDerivAt_Gamma_natstatement · cited by 2
- Real.strictAnti_eulerMascheroniSeq'proof · cited by 2
- ZetaAsymptotics.termSum_onestatement and proof · cited by 2
- harmonic_eq_sum_Iccstatement · cited by 2
- padicValRat_two_harmonicstatement and proof · cited by 2