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_pos {n : } (Hn : n 0) :