-
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
[Merged by Bors] - feat(combinatorics/catalan): Connection between Catalan numbers and number of trees #16583
Conversation
…ty/mathlib into catalan_numbers_trees
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.
Nice! I can't comment on the PR it depends on, but the main PR looks good to me.
This PR/issue depends on: |
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.
Can you merge master to reduce the diff?
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
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 think that's in good shape. Thanks!
maintainer merge
🚀 Pull request has been placed on the maintainer queue by YaelDillies. |
/-- A finset of all trees with `n` nodes. See `mem_trees_of_nodes_eq` -/ | ||
def trees_of_num_nodes_eq : ℕ → finset (tree unit) | ||
| 0 := {nil} | ||
| (n+1) := (finset.nat.antidiagonal n).attach.bUnion $ λ ijh, |
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.
@YaelDillies, can you see a way to use disj_Union
here instead?
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.
Nevermind, this can wait till a follow-up
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 thought about it but it doesn't seem obvious at all.
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.
bors merge
…umber of trees (#16583) Shows that the number of binary trees with `n` nodes is the `n`th Catalan number.
Pull request successfully merged into master. Build succeeded: |
Shows that the number of binary trees with
n
nodes is then
th Catalan number.tree unit
#16715