[Merged by Bors] - feat: the n-th harmonic number is not an integer for n > 1.

[kodyvajjha]

The n-th Harmonic number is not an integer for n > 1. This proof uses 2-adic valuations.

---

This proof is of Theorem 1 in Keith Conrad's blurb. This proof is credited to Kürschák (1918). From this it follows that the 2-adic valuation of H_n tends to infinity as n does. We quickly run into open problems when similar questions are asked for odd primes p.

[Ruben-VandeVelde]

Please don't be intimidated by the comments below, they're simple stylistic suggestions

[kodyvajjha]

@Ruben-VandeVelde thank you for your comments, I've incorporated most of them and the build passes. @alexjbest suggested that we could move this material out of Counterexamples and into mathlib proper. I could do that as a follow up PR if that works.

[kodyvajjha]

i think i've addressed most of the comments - just waiting now for the build to turn green, thanks everyone!

[tb65536]

Looking very good. Maybe someone else can take one last look over?

[alexjbest]

lgtm once those last two comments are taken care of

[alexjbest]

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by alexjbest.

[alexjbest]

Thanks for making all these changes @kodyvajjha, hopefully the next PR will be smoother :)

[kodyvajjha]

Hahaha hopefully! Thanks @alexjbest

[jcommelin]

Thanks 🎉

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style