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

chore: move results on Σ i : Fin n, f i earlier #19415

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

chore: move results on Σ i : Fin n, f i earlier #19415

wants to merge 9 commits into from

Commits on Nov 23, 2024

  1. move results

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

  2. tweak

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

  3. Update BigOperators.lean

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

  4. lake shake

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

  5. Update Finsupp.lean

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

  6. Update Reflection.lean

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

  7. Update Pi.lean

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

Commits on Nov 24, 2024

  1. Update Finsupp.lean

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

  2. fix

    @vihdzp
    vihdzp committed Nov 24, 2024
    Configuration menu
    Copy the full SHA
    124b15f View commit details
    Browse the repository at this point in the history