Documentation

Mathlib.NumberTheory.Harmonic.Defs

This file defines the harmonic numbers.

def harmonic :

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

Equations
Instances For
    @[simp]
    theorem harmonic_zero :
    @[simp]
    theorem harmonic_succ (n : ) :
    harmonic (n + 1) = harmonic n + (↑(n + 1))⁻¹
    theorem harmonic_pos {n : } (Hn : n 0) :
    theorem harmonic_eq_sum_Icc {n : } :
    harmonic n = iFinset.Icc 1 n, (↑i)⁻¹