Theorems · Theorem · number theory
harmonic_not_int
∀ {n : ℕ}, 2 ≤ n → ¬(harmonic n).isInt = trueThe n-th harmonic number is not an integer for n ≥ 2.
- Defined in
- Mathlib.NumberTheory.Harmonic.Int
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 84 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- LT.lt.ne'proof · cited by 1,417
- neg_negproof · cited by 960
- zpow_natCastproof · cited by 271
- Nat.logproof · cited by 101
- one_lt_twoproof · cited by 67
- harmonicstatement · cited by 27
- one_lt_pow₀proof · cited by 18
- ne_zero_of_ltproof · cited by 17
- padicNorm.eq_zpow_of_nonzeroproof · cited by 7
- Nat.log_posproof · cited by 3
- harmonic_posproof · cited by 3
- padicValRat_two_harmonicproof · cited by 2
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.