[Merged by Bors] - feat(data/nat/choose/multinomial): add multinomial theorem #16317
Conversation
Co-authored-by: Junyan Xu <junyanxumath@gmail.com>
pimotte
added
awaiting-review
mathlib-dependent-issues-bot
added
the
blocked-by-other-PR
github-actions
bot
removed
the
awaiting-CI
pimotte
added
awaiting-author
|
Due to changes in #16316 this will need some changes and likely another PR dependency |
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
pimotte
added
awaiting-review
alreadydone
added
the
blocked-by-other-PR
| @@ -87,9 +99,9 @@ by simpa [finset.sum_pair hab, finset.prod_pair hab] using multinomial_spec {a, | |||
| by simp [multinomial_insert_one {b} f (finset.not_mem_singleton.mpr h) h₁] | |||
|
|
|||
| lemma binomial_succ_succ [decidable_eq α] (h : a ≠ b) : | |||
There was a problem hiding this comment.
Should this name be changed? There is no binomial nor succ in the statement. I see something similar also below.
There was a problem hiding this comment.
There are six lemmas with binomial in this file, and I think they are intended to establish a naming convention that binomial refers to multinomial {a, b} with a ≠ b (or maybe more generally finsets of cardinality two, but they don't appear in this file).
There was a problem hiding this comment.
Do you think multinomial_pair is better in place of binomial? If so I can rename all in this PR.
There was a problem hiding this comment.
Hi @riccardobrasca Do you think I should do the rename? You other comments have been marked resolved, and the only change in this PR since your last review was extracting a lemma.
There was a problem hiding this comment.
Sorry, I forgot about this PR. It binomial is intended to be a name convention than it's OK. Maybe we can write it somewhere in the doc (if it's not already present)? Otherwise LGTM, thanks!
There was a problem hiding this comment.
It turns out binomial traces back to the original code written by @kmill, so I think at least one maintainer is OK with the names; I just updated the section docstring to state this naming convention. @pimotte could you just reply bors r+ to get this PR merged? Thanks!
There was a problem hiding this comment.
Done! Thanks for finishing this up:)
mathlib-dependent-issues-bot
removed
the
blocked-by-other-PR
…17108) elaboration of has_sum_single took 17.9s -> 1.37s The timeout happens in an unrelated branch #16317 ([CI log](https://github.com/leanprover-community/mathlib/actions/runs/3294947441/jobs/5432990411)) but not yet in bors batches apparently.
|
bors d+ |
|
✌️ pimotte can now approve this pull request. To approve and merge a pull request, simply reply with |
github-actions
bot
added
delegated
|
bors r+ |
Proof by induction on the number of summands. finset.sym is used to sum over. It means we have access to the finset tooling to rewrite it, and it's one of the more direct ways of expressing it. Co-authored-by: Junyan Xu <junyanxu.math@gmail.com> Co-authored-by: Pim Otte <potte@quintor.nl> Co-authored-by: Junyan Xu <junyanxumath@gmail.com> Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
|
This PR was included in a batch that was canceled, it will be automatically retried |
Proof by induction on the number of summands. finset.sym is used to sum over. It means we have access to the finset tooling to rewrite it, and it's one of the more direct ways of expressing it. Co-authored-by: Junyan Xu <junyanxu.math@gmail.com> Co-authored-by: Pim Otte <potte@quintor.nl> Co-authored-by: Junyan Xu <junyanxumath@gmail.com> Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
|
Build failed (retrying...): |
Proof by induction on the number of summands. finset.sym is used to sum over. It means we have access to the finset tooling to rewrite it, and it's one of the more direct ways of expressing it. Co-authored-by: Pim Otte <potte@quintor.nl> Co-authored-by: Junyan Xu <junyanxumath@gmail.com> Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
Proof by induction on the number of summands. finset.sym is used to sum over. It means we have access to the finset tooling to rewrite it, and it's one of the more direct ways of expressing it.
set.pairwise#16859fillfilter_neandsigma_ext#16316 [basic sym lemma's to support definition]fill_mem,append_memand supporting lemmas #16486