Defs

📁 Source: Mathlib/NumberTheory/Harmonic/Defs.lean

Statistics

Metric	Count
Definitions harmonic	1
Theorems harmonic_succ, harmonic_zero	2
Total	3

(root)

Definitions

Name	Category	Theorems
harmonic 📖	CompOp	18 math math: log_add_one_le_harmonic, Real.deriv_Gamma_nat, Real.tendsto_harmonic_sub_log, Complex.deriv_Gamma_nat, harmonic_zero, harmonic_not_int, harmonic_le_one_add_log, padicValRat_two_harmonic, harmonic_floor_le_one_add_log, harmonic_pos, harmonic_succ, log_le_harmonic_floor, harmonic_eq_sum_Icc, ZetaAsymptotics.term_sum_one, Real.hasDerivAt_Gamma_nat, padicNorm_two_harmonic, Real.tendsto_harmonic_sub_log_add_one, Complex.hasDerivAt_Gamma_nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
harmonic_succ 📖	mathematical	—	harmonic	—	Finset.sum_range_succ
harmonic_zero 📖	mathematical	—	harmonic	—	—

---

← Back to Index