Commit 2023-09-29 04:40 5d32dbde

View on Github →

feat: the n-th harmonic number is not an integer for n > 1. (#7319) The n-th Harmonic number is not an integer for n > 1. This proof uses 2-adic valuations.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Finset/Basic.lean

added theorem Finset.Nontrivial.sdiff_singleton_nonempty

added theorem Finset.range_nontrivial

Modified Mathlib/Data/Rat/Defs.lean

added theorem Rat.eq_num_of_isInt

Created Mathlib/NumberTheory/Padics/Harmonic.lean

added def harmonic

added theorem harmonic_not_int

added theorem harmonic_pos

added theorem harmonic_succ

added theorem harmonic_zero

added theorem padicValRat_two_harmonic

Modified Mathlib/NumberTheory/Padics/PadicNorm.lean

added theorem padicNorm.not_int_of_not_padic_int

Modified Mathlib/NumberTheory/Padics/PadicVal.lean

added theorem Nat.log_ne_padicValNat_succ

added theorem Nat.max_log_padicValNat_succ_eq_log_succ

added theorem nat_log_eq_padicValNat_iff

added theorem padicValNat_le_nat_log

added theorem padicValRat.add_eq_min

added theorem padicValRat.add_eq_of_lt

added theorem padicValRat.lt_add_of_lt

added theorem padicValRat.lt_sum_of_lt

added theorem padicValRat.self_pow_inv

added theorem padicValRat_def