This file defines the harmonic numbers.

• Mathilb/NumberTheory/Harmonic/Int.lean proves that the nth harmonic number is not an integer.
• Mathlib/NumberTheory/Harmonic/Bounds.lean provides basic log bounds.

def harmonic : ℕ → ℚ

The nth-harmonic number defined as a finset sum of consecutive reciprocals.

@[simp]

theorem harmonic_zero : harmonic 0 = 0

@[simp]

theorem harmonic_succ (n : ℕ) : harmonic (n + 1) = harmonic n + (↑(n + 1))⁻¹