Theorem harmonic_succ

Modification history

2024-03-01 13:29

Mathlib/NumberTheory/Harmonic/Defs.lean

feat: explicit logarithmic bounds on the harmonic numbers (#9984) …

Modified harmonic_succ View on Github →

2023-09-29 04:40

Mathlib/NumberTheory/Padics/Harmonic.lean

feat: the n-th harmonic number is not an integer for n > 1. (#7319) …

Added harmonic_succ View on Github →