Def harmonic

Modification history

2024-05-27 08:32

Mathlib/NumberTheory/Harmonic/Defs.lean

chore: Use the new `∑ i ∈ s, f i` notation (#13209) …

Modified harmonic View on Github →

2024-03-01 13:29

Mathlib/NumberTheory/Harmonic/Defs.lean

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

Modified harmonic 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 View on Github →