Theorem harmonic_le_one_add_log

Modification history

2024-03-01 13:29
Mathlib/NumberTheory/Harmonic/Bounds.lean
feat: explicit logarithmic bounds on the harmonic numbers (#9984) …
Added harmonic_le_one_add_logView on Github →