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.

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

feat: Nesbitt's inequality #19414

Open
wants to merge 17 commits into
base: master
Choose a base branch
from
Open

feat: Nesbitt's inequality #19414

wants to merge 17 commits into from

Commits on Nov 20, 2024

  1. prove lemma

    vihdzp committed Nov 20, 2024
    Configuration menu
    Copy the full SHA
    396a25a View commit details
    Browse the repository at this point in the history
  2. fix indent

    vihdzp committed Nov 20, 2024
    Configuration menu
    Copy the full SHA
    25efc02 View commit details
    Browse the repository at this point in the history
  3. tiny tweaks

    vihdzp committed Nov 20, 2024
    Configuration menu
    Copy the full SHA
    ed2ff54 View commit details
    Browse the repository at this point in the history

Commits on Nov 21, 2024

  1. AM-GM

    vihdzp committed Nov 21, 2024
    Configuration menu
    Copy the full SHA
    f3dae53 View commit details
    Browse the repository at this point in the history
  2. generalize Cauchy-Schwarz

    vihdzp committed Nov 21, 2024
    Configuration menu
    Copy the full SHA
    db46322 View commit details
    Browse the repository at this point in the history
  3. prove sedrakyan

    vihdzp committed Nov 21, 2024
    Configuration menu
    Copy the full SHA
    b60a817 View commit details
    Browse the repository at this point in the history

Commits on Nov 22, 2024

  1. Update Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean

    Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
    vihdzp and YaelDillies authored Nov 22, 2024
    Configuration menu
    Copy the full SHA
    b028f67 View commit details
    Browse the repository at this point in the history
  2. Update Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean

    Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
    vihdzp and YaelDillies authored Nov 22, 2024
    Configuration menu
    Copy the full SHA
    c0059be View commit details
    Browse the repository at this point in the history
  3. Update Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean

    Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
    vihdzp and YaelDillies authored Nov 22, 2024
    Configuration menu
    Copy the full SHA
    4cf3fb4 View commit details
    Browse the repository at this point in the history
  4. Update Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean

    Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
    vihdzp and YaelDillies authored Nov 22, 2024
    Configuration menu
    Copy the full SHA
    48604e1 View commit details
    Browse the repository at this point in the history
  5. expand docstring

    vihdzp committed Nov 22, 2024
    Configuration menu
    Copy the full SHA
    84cdb38 View commit details
    Browse the repository at this point in the history
  6. reorder file

    vihdzp committed Nov 22, 2024
    Configuration menu
    Copy the full SHA
    9596fff View commit details
    Browse the repository at this point in the history
  7. Update Finset.lean

    vihdzp committed Nov 22, 2024
    Configuration menu
    Copy the full SHA
    50551e2 View commit details
    Browse the repository at this point in the history
  8. prove thm

    vihdzp committed Nov 22, 2024
    Configuration menu
    Copy the full SHA
    d011ea4 View commit details
    Browse the repository at this point in the history
  9. Update Finset.lean

    vihdzp committed Nov 22, 2024
    Configuration menu
    Copy the full SHA
    36eb833 View commit details
    Browse the repository at this point in the history

Commits on Nov 23, 2024

  1. Configuration menu
    Copy the full SHA
    2ec018c View commit details
    Browse the repository at this point in the history
  2. golf

    vihdzp committed Nov 23, 2024
    Configuration menu
    Copy the full SHA
    0cfd0a7 View commit details
    Browse the repository at this point in the history