Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

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

Closed
wants to merge 74 commits into from
Closed

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

wants to merge 74 commits into from

Commits on Sep 26, 2023

  1. feat: stated the main theorem

    @kodyvajjha
    kodyvajjha committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    62e346a View commit details
    Browse the repository at this point in the history

  2. wip: progress

    @kodyvajjha
    kodyvajjha committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    5254a3e View commit details
    Browse the repository at this point in the history

  3. feat: prove not_int_of_not_padic_int

    @kodyvajjha
    kodyvajjha committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    886117a View commit details
    Browse the repository at this point in the history

  4. progress, add harmonic ne_zero

    @kodyvajjha
    kodyvajjha committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    7e789be View commit details
    Browse the repository at this point in the history

  5. slight progress.

    @kodyvajjha
    kodyvajjha committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    d8f7d3e View commit details
    Browse the repository at this point in the history

  6. add finset defn of harmonic numbers

    @kodyvajjha
    kodyvajjha committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    c7c345c View commit details
    Browse the repository at this point in the history

  7. wip min_eq_padicValRat

    @kodyvajjha
    kodyvajjha committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    25b4e91 View commit details
    Browse the repository at this point in the history

  8. feat: min_eq_padicValRat

    @kodyvajjha
    kodyvajjha committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    d193c37 View commit details
    Browse the repository at this point in the history

  9. feat: golf attempt

    @kodyvajjha
    kodyvajjha committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    a67c69f View commit details
    Browse the repository at this point in the history

  10. add le_nat_log + wip padicValRat_2_sum

    @kodyvajjha
    kodyvajjha committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    0ed3c48 View commit details
    Browse the repository at this point in the history

  11. add padicvalnat le log lemmas

    @kodyvajjha
    kodyvajjha committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    39e7c9b View commit details
    Browse the repository at this point in the history

  12. prove nat_log_eq_padicvalnat_iff

    @kodyvajjha
    kodyvajjha committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    258d3cf View commit details
    Browse the repository at this point in the history

  13. add nat log not dvd

    @kodyvajjha
    kodyvajjha committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    57f8e45 View commit details
    Browse the repository at this point in the history

  14. padicValRat_ge_neg_Nat_log'

    @kodyvajjha
    kodyvajjha committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    4df29c5 View commit details
    Browse the repository at this point in the history

  15. down to one sorry

    @kodyvajjha
    kodyvajjha committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    3f020f9 View commit details
    Browse the repository at this point in the history

  16. wip

    @kodyvajjha
    kodyvajjha committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    e4538fb View commit details
    Browse the repository at this point in the history

  17. progress?

    @kodyvajjha
    kodyvajjha committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    8ec3340 View commit details
    Browse the repository at this point in the history

  18. more lemmas, maybe progress

    @kodyvajjha
    kodyvajjha committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    60ceb83 View commit details
    Browse the repository at this point in the history

  19. sorry free proof of harmonic not int

    @kodyvajjha
    kodyvajjha committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    761aee7 View commit details
    Browse the repository at this point in the history

  20. clean up some proofs

    @kodyvajjha
    kodyvajjha committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    7cac0af View commit details
    Browse the repository at this point in the history

  21. slight more refactor

    @kodyvajjha
    kodyvajjha committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    2569522 View commit details
    Browse the repository at this point in the history

  22. cleanup

    @kodyvajjha
    kodyvajjha committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    1609582 View commit details
    Browse the repository at this point in the history

  23. remove unneeded imports

    @kodyvajjha
    kodyvajjha committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    45c0d30 View commit details
    Browse the repository at this point in the history

  24. document

    @kodyvajjha
    kodyvajjha committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    1311ab6 View commit details
    Browse the repository at this point in the history

  25. add file to counterexamples

    @kodyvajjha
    kodyvajjha committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    a7fece2 View commit details
    Browse the repository at this point in the history

  26. more changes

    @kodyvajjha
    kodyvajjha committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    15b79f9 View commit details
    Browse the repository at this point in the history

  27. simplify all proofs and add some documentation

    @kodyvajjha
    kodyvajjha committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    2a27077 View commit details
    Browse the repository at this point in the history

  28. factor out lemmas to go into padicval

    @kodyvajjha
    kodyvajjha committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    90cf371 View commit details
    Browse the repository at this point in the history

  29. remove unneeded argument

    @kodyvajjha
    kodyvajjha committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    90fd8dc View commit details
    Browse the repository at this point in the history

  30. counterexample in right place

    @kodyvajjha
    kodyvajjha committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    f70cd34 View commit details
    Browse the repository at this point in the history

  31. fix: build

    @kodyvajjha
    kodyvajjha committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    d44e4e6 View commit details
    Browse the repository at this point in the history

  32. address comments

    @kodyvajjha
    kodyvajjha committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    7fa0088 View commit details
    Browse the repository at this point in the history

  33. various indentation suggestions + renaming

    @kodyvajjha
    kodyvajjha committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    d7f092f View commit details
    Browse the repository at this point in the history

  34. move to number theory + padics

    @kodyvajjha
    kodyvajjha committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    ff72121 View commit details
    Browse the repository at this point in the history

  35. padicvalrat_2_pow -> padicvalrat_two_pow_div

    @kodyvajjha
    kodyvajjha committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    be2bc38 View commit details
    Browse the repository at this point in the history

  36. generalize to arbitrary prime p

    @kodyvajjha
    kodyvajjha committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    4c3a0e8 View commit details
    Browse the repository at this point in the history

  37. rename

    @kodyvajjha
    kodyvajjha committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    faacc31 View commit details
    Browse the repository at this point in the history

  38. more updates

    @kodyvajjha
    kodyvajjha committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    4d46a3b View commit details
    Browse the repository at this point in the history

  39. address review comments

    @kodyvajjha
    kodyvajjha committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    e3d2925 View commit details
    Browse the repository at this point in the history

  40. Update Mathlib/NumberTheory/Padics/PadicNorm.lean 

    Co-authored-by: Alex J Best <alex.j.best@gmail.com>
    @kodyvajjha @alexjbest
    kodyvajjha and alexjbest committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    e484f4f View commit details
    Browse the repository at this point in the history

  41. add padicValRat_def

    @kodyvajjha
    kodyvajjha committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    8905db7 View commit details
    Browse the repository at this point in the history

  42. appease linter

    @kodyvajjha
    kodyvajjha committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    ec511de View commit details
    Browse the repository at this point in the history

  43. alex's comments

    @kodyvajjha
    kodyvajjha committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    c7d4c9a View commit details
    Browse the repository at this point in the history

  44. simplify not_int_if_not_padic_int

    @kodyvajjha
    kodyvajjha committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    f9e5dd3 View commit details
    Browse the repository at this point in the history

  45. simplify not_int_of_not_padic_int

    @kodyvajjha
    kodyvajjha committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    ef7a81e View commit details
    Browse the repository at this point in the history

  46. Update Mathlib/NumberTheory/Padics/PadicVal.lean 

    Co-authored-by: Thomas Browning <tb65536@users.noreply.github.com>
    @kodyvajjha @tb65536
    kodyvajjha and tb65536 committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    bf02552 View commit details
    Browse the repository at this point in the history

  47. Update Mathlib/NumberTheory/Padics/PadicVal.lean 

    Co-authored-by: Thomas Browning <tb65536@users.noreply.github.com>
    @kodyvajjha @tb65536
    kodyvajjha and tb65536 committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    edd54dc View commit details
    Browse the repository at this point in the history

  48. add_eq_min

    @kodyvajjha
    kodyvajjha committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    db51df4 View commit details
    Browse the repository at this point in the history

  49. add_lt_of_lt -> lt_add_of_lt

    @kodyvajjha
    kodyvajjha committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    bc58ab8 View commit details
    Browse the repository at this point in the history

  50. simplify self_pow_div

    @kodyvajjha
    kodyvajjha committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    51f2acc View commit details
    Browse the repository at this point in the history

  51. simplify harmonic not int

    @kodyvajjha
    kodyvajjha committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    39c6fb0 View commit details
    Browse the repository at this point in the history

  52. Update Mathlib/NumberTheory/Padics/PadicVal.lean 

    Co-authored-by: Thomas Browning <tb65536@users.noreply.github.com>
    @kodyvajjha @tb65536
    kodyvajjha and tb65536 committed Sep 26, 2023
    Configuration menu
    Copy the full SHA
    797e82f View commit details
    Browse the repository at this point in the history

Commits on Sep 27, 2023

  1. move finset lemma to basic file

    @kodyvajjha
    kodyvajjha committed Sep 27, 2023
    Configuration menu
    Copy the full SHA
    6338778 View commit details
    Browse the repository at this point in the history

  2. fix proof

    @kodyvajjha
    kodyvajjha committed Sep 27, 2023
    Configuration menu
    Copy the full SHA
    5c63894 View commit details
    Browse the repository at this point in the history

  3. rename to allow dot notation

    @kodyvajjha
    kodyvajjha committed Sep 27, 2023
    Configuration menu
    Copy the full SHA
    a1cce8d View commit details
    Browse the repository at this point in the history

  4. ⁻¹ instead of /

    @kodyvajjha
    kodyvajjha committed Sep 27, 2023
    Configuration menu
    Copy the full SHA
    8741aa3 View commit details
    Browse the repository at this point in the history

  5. use dot notation

    @kodyvajjha
    kodyvajjha committed Sep 27, 2023
    Configuration menu
    Copy the full SHA
    2b3ac1a View commit details
    Browse the repository at this point in the history

  6. Nat.log instead of Int.log

    @kodyvajjha
    kodyvajjha committed Sep 27, 2023
    Configuration menu
    Copy the full SHA
    e249282 View commit details
    Browse the repository at this point in the history

  7. simpler harmonic not int proof

    @kodyvajjha
    kodyvajjha committed Sep 27, 2023
    Configuration menu
    Copy the full SHA
    f61a5c5 View commit details
    Browse the repository at this point in the history

  8. simplify proof

    @kodyvajjha
    kodyvajjha committed Sep 27, 2023
    Configuration menu
    Copy the full SHA
    7ce7924 View commit details
    Browse the repository at this point in the history

  9. add main result

    @kodyvajjha
    kodyvajjha committed Sep 27, 2023
    Configuration menu
    Copy the full SHA
    7212811 View commit details
    Browse the repository at this point in the history

  10. spacing

    @kodyvajjha
    kodyvajjha committed Sep 27, 2023
    Configuration menu
    Copy the full SHA
    00a3520 View commit details
    Browse the repository at this point in the history

Commits on Sep 28, 2023

  1. Update Mathlib/NumberTheory/Padics/PadicNorm.lean 

    Co-authored-by: Thomas Browning <tb65536@users.noreply.github.com>
    @kodyvajjha @tb65536
    kodyvajjha and tb65536 committed Sep 28, 2023
    Configuration menu
    Copy the full SHA
    1a2cb2b View commit details
    Browse the repository at this point in the history

  2. Update Mathlib/NumberTheory/Padics/PadicVal.lean 

    Co-authored-by: Thomas Browning <tb65536@users.noreply.github.com>
    @kodyvajjha @tb65536
    kodyvajjha and tb65536 committed Sep 28, 2023
    Configuration menu
    Copy the full SHA
    d8b593a View commit details
    Browse the repository at this point in the history

  3. Update Mathlib/NumberTheory/Padics/Harmonic.lean 

    Co-authored-by: Thomas Browning <tb65536@users.noreply.github.com>
    @kodyvajjha @tb65536
    kodyvajjha and tb65536 committed Sep 28, 2023
    Configuration menu
    Copy the full SHA
    e4a946d View commit details
    Browse the repository at this point in the history

  4. fix build

    @kodyvajjha
    kodyvajjha committed Sep 28, 2023
    Configuration menu
    Copy the full SHA
    40ef8dc View commit details
    Browse the repository at this point in the history

  5. appease linter

    @kodyvajjha
    kodyvajjha committed Sep 28, 2023
    Configuration menu
    Copy the full SHA
    2365d53 View commit details
    Browse the repository at this point in the history

  6. move lemmas around

    @kodyvajjha
    kodyvajjha committed Sep 28, 2023
    Configuration menu
    Copy the full SHA
    aa60496 View commit details
    Browse the repository at this point in the history

  7. delete le_nat_log_of_le

    @kodyvajjha
    kodyvajjha committed Sep 28, 2023
    Configuration menu
    Copy the full SHA
    3653d5b View commit details
    Browse the repository at this point in the history

  8. Update Mathlib/Data/Finset/Basic.lean 

    Co-authored-by: Thomas Browning <tb65536@users.noreply.github.com>
    @kodyvajjha @tb65536
    kodyvajjha and tb65536 committed Sep 28, 2023
    Configuration menu
    Copy the full SHA
    f4cbf9c View commit details
    Browse the repository at this point in the history

  9. Update Mathlib/Data/Finset/Basic.lean 

    Co-authored-by: Thomas Browning <tb65536@users.noreply.github.com>
    @kodyvajjha @tb65536
    kodyvajjha and tb65536 committed Sep 28, 2023
    Configuration menu
    Copy the full SHA
    aeb9acb View commit details
    Browse the repository at this point in the history

  10. Update Mathlib/NumberTheory/Padics/PadicVal.lean 

    Co-authored-by: Thomas Browning <tb65536@users.noreply.github.com>
    @kodyvajjha @tb65536
    kodyvajjha and tb65536 committed Sep 28, 2023
    Configuration menu
    Copy the full SHA
    12f33fb View commit details
    Browse the repository at this point in the history

Commits on Sep 29, 2023

  1. Update Mathlib/NumberTheory/Padics/PadicVal.lean 

    Co-authored-by: Thomas Browning <tb65536@users.noreply.github.com>
    @kodyvajjha @tb65536
    kodyvajjha and tb65536 committed Sep 29, 2023
    Configuration menu
    Copy the full SHA
    26fa193 View commit details
    Browse the repository at this point in the history

  2. move and rename

    @kodyvajjha
    kodyvajjha committed Sep 29, 2023
    Configuration menu
    Copy the full SHA
    c754994 View commit details
    Browse the repository at this point in the history