-
Notifications
You must be signed in to change notification settings - Fork 297
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(data/fin*): uniqueness of increasing bijection #2258
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Otherwise, LGTM!
gives `(a + b)^n`. The "good" proof involves expanding along all coordinates using the fact that | ||
`x^n` is multilinear, but multilinear maps are only available now over rings, so we give instead | ||
a proof reducing to the usual binomial theorem to have a result over semirings. -/ | ||
lemma fintype.sum_pow_mul_eq_add_pow |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I did a bit of a refactor of this lemma yesterday. I first proved the lemma prod_add {α R : Type*} [comm_semiring R] (f g : α → R) (s : finset α) : s.prod (λ a, f a + g a) = s.powerset.sum (λ t : finset α, t.prod f * (s.filter (∉ t)).prod g)
and restated this lemma using a finset α
instead of the whole of α
and finset.powerset
in place of finset.univ
, and proving it using prod_add
. Are you happy for me to push these changes to this branch?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Sure, thanks!
Co-Authored-By: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Co-Authored-By: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Co-Authored-By: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Co-Authored-By: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Co-Authored-By: Bryan Gin-ge Chen <bryangingechen@gmail.com>
I made some changes. I'll let @urkud review my changes. |
PR #2048 changed the CI so that olean caches are not pushed to Azure if a later commit on the same branch occurs. The reasoning was that it was unlikely that anyone would fetch those caches. That's changed as of #2278, since `fetch_olean_cache.sh` now looks for caches from commits earlier in the history. This means that currently, we can observe the following wasteful sequence of events in several PRs (e.g. #2258): 1. commit A gets pushed to a certain branch and CI_A starts. 2. While CI_A is still running the `leanpkg build` step, commit B is pushed and CI_B starts. 3. CI_A finishes `leanpkg build` but doesn't upload its cache to Azure because of #2048 4. Now commit C is pushed and can't use the results of CI_A 5. CI_B finishes `leanpkg build` but doesn't upload its cache 6. Commit D is pushed and can't use the results of CI_A or CI_B ... (This can keep happening as long as the next commit arrives before the most recent CI uploads to Azure). I also cleaned up some stuff that was left over from when we ran the build on both "pr" and "push" events.
…nity#2258) * feat(data/fin*): uniqueness of increasing bijection * protect * remove tidy call * Update src/data/finset.lean Co-Authored-By: Bryan Gin-ge Chen <bryangingechen@gmail.com> * Update src/data/finset.lean Co-Authored-By: Bryan Gin-ge Chen <bryangingechen@gmail.com> * Update src/data/fintype/card.lean Co-Authored-By: Bryan Gin-ge Chen <bryangingechen@gmail.com> * Update src/data/fintype/card.lean Co-Authored-By: Bryan Gin-ge Chen <bryangingechen@gmail.com> * Update src/data/fintype/card.lean Co-Authored-By: Bryan Gin-ge Chen <bryangingechen@gmail.com> * prove prod_add, and use this to prove sum_pow_mul_eq_add_pow * forgot to save * fix build * remove card_sub_card Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com> Co-authored-by: Chris Hughes <chrishughes24@gmail.com> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
PR leanprover-community#2048 changed the CI so that olean caches are not pushed to Azure if a later commit on the same branch occurs. The reasoning was that it was unlikely that anyone would fetch those caches. That's changed as of leanprover-community#2278, since `fetch_olean_cache.sh` now looks for caches from commits earlier in the history. This means that currently, we can observe the following wasteful sequence of events in several PRs (e.g. leanprover-community#2258): 1. commit A gets pushed to a certain branch and CI_A starts. 2. While CI_A is still running the `leanpkg build` step, commit B is pushed and CI_B starts. 3. CI_A finishes `leanpkg build` but doesn't upload its cache to Azure because of leanprover-community#2048 4. Now commit C is pushed and can't use the results of CI_A 5. CI_B finishes `leanpkg build` but doesn't upload its cache 6. Commit D is pushed and can't use the results of CI_A or CI_B ... (This can keep happening as long as the next commit arrives before the most recent CI uploads to Azure). I also cleaned up some stuff that was left over from when we ran the build on both "pr" and "push" events.
…nity#2258) * feat(data/fin*): uniqueness of increasing bijection * protect * remove tidy call * Update src/data/finset.lean Co-Authored-By: Bryan Gin-ge Chen <bryangingechen@gmail.com> * Update src/data/finset.lean Co-Authored-By: Bryan Gin-ge Chen <bryangingechen@gmail.com> * Update src/data/fintype/card.lean Co-Authored-By: Bryan Gin-ge Chen <bryangingechen@gmail.com> * Update src/data/fintype/card.lean Co-Authored-By: Bryan Gin-ge Chen <bryangingechen@gmail.com> * Update src/data/fintype/card.lean Co-Authored-By: Bryan Gin-ge Chen <bryangingechen@gmail.com> * prove prod_add, and use this to prove sum_pow_mul_eq_add_pow * forgot to save * fix build * remove card_sub_card Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com> Co-authored-by: Chris Hughes <chrishughes24@gmail.com> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
PR leanprover-community#2048 changed the CI so that olean caches are not pushed to Azure if a later commit on the same branch occurs. The reasoning was that it was unlikely that anyone would fetch those caches. That's changed as of leanprover-community#2278, since `fetch_olean_cache.sh` now looks for caches from commits earlier in the history. This means that currently, we can observe the following wasteful sequence of events in several PRs (e.g. leanprover-community#2258): 1. commit A gets pushed to a certain branch and CI_A starts. 2. While CI_A is still running the `leanpkg build` step, commit B is pushed and CI_B starts. 3. CI_A finishes `leanpkg build` but doesn't upload its cache to Azure because of leanprover-community#2048 4. Now commit C is pushed and can't use the results of CI_A 5. CI_B finishes `leanpkg build` but doesn't upload its cache 6. Commit D is pushed and can't use the results of CI_A or CI_B ... (This can keep happening as long as the next commit arrives before the most recent CI uploads to Azure). I also cleaned up some stuff that was left over from when we ran the build on both "pr" and "push" events.
…nity#2258) * feat(data/fin*): uniqueness of increasing bijection * protect * remove tidy call * Update src/data/finset.lean Co-Authored-By: Bryan Gin-ge Chen <bryangingechen@gmail.com> * Update src/data/finset.lean Co-Authored-By: Bryan Gin-ge Chen <bryangingechen@gmail.com> * Update src/data/fintype/card.lean Co-Authored-By: Bryan Gin-ge Chen <bryangingechen@gmail.com> * Update src/data/fintype/card.lean Co-Authored-By: Bryan Gin-ge Chen <bryangingechen@gmail.com> * Update src/data/fintype/card.lean Co-Authored-By: Bryan Gin-ge Chen <bryangingechen@gmail.com> * prove prod_add, and use this to prove sum_pow_mul_eq_add_pow * forgot to save * fix build * remove card_sub_card Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com> Co-authored-by: Chris Hughes <chrishughes24@gmail.com> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
PR leanprover-community#2048 changed the CI so that olean caches are not pushed to Azure if a later commit on the same branch occurs. The reasoning was that it was unlikely that anyone would fetch those caches. That's changed as of leanprover-community#2278, since `fetch_olean_cache.sh` now looks for caches from commits earlier in the history. This means that currently, we can observe the following wasteful sequence of events in several PRs (e.g. leanprover-community#2258): 1. commit A gets pushed to a certain branch and CI_A starts. 2. While CI_A is still running the `leanpkg build` step, commit B is pushed and CI_B starts. 3. CI_A finishes `leanpkg build` but doesn't upload its cache to Azure because of leanprover-community#2048 4. Now commit C is pushed and can't use the results of CI_A 5. CI_B finishes `leanpkg build` but doesn't upload its cache 6. Commit D is pushed and can't use the results of CI_A or CI_B ... (This can keep happening as long as the next commit arrives before the most recent CI uploads to Azure). I also cleaned up some stuff that was left over from when we ran the build on both "pr" and "push" events.
Additional material on the increasing bijection between
fin k
and an ordered finset (uniqueness, and the fact that it maps0
to the minimum of the set andk-1
to its maximum), together with miscellaneous material on finsets and fintypes.