Theorem harmonic_pos

Modification history

2025-02-17 19:42
Mathlib/NumberTheory/Harmonic/Defs.lean
chore(NumberTheory/Harmonic): move some results downstream from `Defs.lean` (#21999) …
Modified harmonic_posView on Github →
2024-03-19 20:08
Mathlib/NumberTheory/Harmonic/Defs.lean
chore: tidy various files (#11490)
Modified harmonic_posView on Github →
2024-03-01 13:29
Mathlib/NumberTheory/Harmonic/Defs.lean
feat: explicit logarithmic bounds on the harmonic numbers (#9984) …
Modified harmonic_posView 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_posView on Github →