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

[Merged by Bors] - feat(combinatorics/catalan): Connection between Catalan numbers and number of trees #16583

Closed
wants to merge 52 commits into from
Closed

[Merged by Bors] - feat(combinatorics/catalan): Connection between Catalan numbers and number of trees #16583

wants to merge 52 commits into from

Commits on Sep 7, 2022

  1. Initial commit

    @prakol16
    prakol16 committed Sep 7, 2022
    Configuration menu
    Copy the full SHA
    4c26295 View commit details
    Browse the repository at this point in the history

  2. Pull out nat decoding into function

    @prakol16
    prakol16 committed Sep 7, 2022
    Configuration menu
    Copy the full SHA
    b360476 View commit details
    Browse the repository at this point in the history

  3. Fix lint

    @prakol16
    prakol16 committed Sep 7, 2022
    Configuration menu
    Copy the full SHA
    e895515 View commit details
    Browse the repository at this point in the history

  4. Fix duplicate instance arg

    @prakol16
    prakol16 committed Sep 7, 2022
    Configuration menu
    Copy the full SHA
    0b546fb View commit details
    Browse the repository at this point in the history

  5. Add docstrings

    @prakol16
    prakol16 committed Sep 7, 2022
    Configuration menu
    Copy the full SHA
    4af6fbd View commit details
    Browse the repository at this point in the history

Commits on Sep 8, 2022

  1. Add missing docstrings

    @prakol16
    prakol16 committed Sep 8, 2022
    Configuration menu
    Copy the full SHA
    d1de5f2 View commit details
    Browse the repository at this point in the history

Commits on Sep 9, 2022

  1. Use unit_tree instead of tree

    @prakol16
    prakol16 committed Sep 9, 2022
    Configuration menu
    Copy the full SHA
    baa7fff View commit details
    Browse the repository at this point in the history

  2. Fix tencodable

    @prakol16
    prakol16 committed Sep 9, 2022
    Configuration menu
    Copy the full SHA
    d7e7a97 View commit details
    Browse the repository at this point in the history

Commits on Sep 10, 2022

  1. Add inhabited instance

    @prakol16
    prakol16 committed Sep 10, 2022
    Configuration menu
    Copy the full SHA
    0aa93cb View commit details
    Browse the repository at this point in the history

Commits on Sep 20, 2022

  1. Fix TODO

    @prakol16
    prakol16 committed Sep 20, 2022
    Configuration menu
    Copy the full SHA
    7f540ef View commit details
    Browse the repository at this point in the history

Commits on Sep 21, 2022

  1. Change names

    @prakol16
    prakol16 committed Sep 21, 2022
    Configuration menu
    Copy the full SHA
    309a7cd View commit details
    Browse the repository at this point in the history

  2. Add definition of height

    @prakol16
    prakol16 committed Sep 21, 2022
    Configuration menu
    Copy the full SHA
    35926e5 View commit details
    Browse the repository at this point in the history

  3. Merge branch 'tree_encoding' of https://github.com/leanprover-communi… 

    …ty/mathlib into catalan_numbers_trees
    @prakol16
    prakol16 committed Sep 21, 2022
    Configuration menu
    Copy the full SHA
    fe04240 View commit details
    Browse the repository at this point in the history

  4. Add height le nodes

    @prakol16
    prakol16 committed Sep 21, 2022
    Configuration menu
    Copy the full SHA
    ea5be3a View commit details
    Browse the repository at this point in the history

  5. Clarify definition

    @prakol16
    prakol16 committed Sep 21, 2022
    Configuration menu
    Copy the full SHA
    457d6af View commit details
    Browse the repository at this point in the history

  6. Merge branch 'tree_encoding' of https://github.com/leanprover-communi… 

    …ty/mathlib into catalan_numbers_trees
    @prakol16
    prakol16 committed Sep 21, 2022
    Configuration menu
    Copy the full SHA
    87463da View commit details
    Browse the repository at this point in the history

  7. Prove theorem

    @prakol16
    prakol16 committed Sep 21, 2022
    Configuration menu
    Copy the full SHA
    d6f6206 View commit details
    Browse the repository at this point in the history

  8. Move sum lemma to big_operators

    @prakol16
    prakol16 committed Sep 21, 2022
    Configuration menu
    Copy the full SHA
    73a5a2c View commit details
    Browse the repository at this point in the history

Commits on Sep 29, 2022

  1. Move part of #16415 into its own branch

    @prakol16
    prakol16 committed Sep 29, 2022
    Configuration menu
    Copy the full SHA
    0acbe8b View commit details
    Browse the repository at this point in the history

  2. Remove encodable definitions (unnecessary for catalan)

    @prakol16
    prakol16 committed Sep 29, 2022
    Configuration menu
    Copy the full SHA
    52657ea View commit details
    Browse the repository at this point in the history

  3. Merge branch 'unit_tree' of https://github.com/leanprover-community/m… 

    …athlib into catalan_numbers_trees
    @prakol16
    prakol16 committed Sep 29, 2022
    Configuration menu
    Copy the full SHA
    1285902 View commit details
    Browse the repository at this point in the history

  4. Fix a comment

    @prakol16
    prakol16 committed Sep 29, 2022
    Configuration menu
    Copy the full SHA
    92e9908 View commit details
    Browse the repository at this point in the history

  5. Merge branch 'unit_tree' of https://github.com/leanprover-community/m… 

    …athlib into catalan_numbers_trees
    @prakol16
    prakol16 committed Sep 29, 2022
    Configuration menu
    Copy the full SHA
    cdb34cf View commit details
    Browse the repository at this point in the history

Commits on Oct 18, 2022

  1. Remove unit_tree, replace with tree

    @prakol16
    prakol16 committed Oct 18, 2022
    Configuration menu
    Copy the full SHA
    3738f71 View commit details
    Browse the repository at this point in the history

  2. Add pattern for unit node

    @prakol16
    prakol16 committed Oct 18, 2022
    Configuration menu
    Copy the full SHA
    39ef81c View commit details
    Browse the repository at this point in the history

Commits on Oct 19, 2022

  1. Merge branch 'unit_tree' of https://github.com/leanprover-community/m… 

    …athlib into catalan_numbers_trees
    @prakol16
    prakol16 committed Oct 19, 2022
    Configuration menu
    Copy the full SHA
    e8ff7ea View commit details
    Browse the repository at this point in the history

  2. Add unit-specific lemmas

    @prakol16
    prakol16 committed Oct 19, 2022
    Configuration menu
    Copy the full SHA
    f8891fb View commit details
    Browse the repository at this point in the history

  3. Add docstring to recursor

    @prakol16
    prakol16 committed Oct 19, 2022
    Configuration menu
    Copy the full SHA
    1ecb82a View commit details
    Browse the repository at this point in the history

  4. Merge branch 'unit_tree' of https://github.com/leanprover-community/m… 

    …athlib into catalan_numbers_trees
    @prakol16
    prakol16 committed Oct 19, 2022
    Configuration menu
    Copy the full SHA
    3a838c8 View commit details
    Browse the repository at this point in the history

  5. Update to not use unit_tree

    @prakol16
    prakol16 committed Oct 19, 2022
    Configuration menu
    Copy the full SHA
    cbd29d9 View commit details
    Browse the repository at this point in the history

  6. Remove usage of new sum operators

    @prakol16
    prakol16 committed Oct 19, 2022
    Configuration menu
    Copy the full SHA
    7ec1993 View commit details
    Browse the repository at this point in the history

  7. Minor; change name of leaves, clean up comments

    @prakol16
    prakol16 committed Oct 19, 2022
    Configuration menu
    Copy the full SHA
    12f5cb2 View commit details
    Browse the repository at this point in the history

  8. Merge branch 'unit_tree' of https://github.com/leanprover-community/m… 

    …athlib into catalan_numbers_trees
    @prakol16
    prakol16 committed Oct 19, 2022
    Configuration menu
    Copy the full SHA
    acf8b38 View commit details
    Browse the repository at this point in the history

Commits on Oct 22, 2022

  1. Change name of nodes

    @prakol16
    prakol16 committed Oct 22, 2022
    Configuration menu
    Copy the full SHA
    1ea625a View commit details
    Browse the repository at this point in the history

  2. Remove non_nil

    @prakol16
    prakol16 committed Oct 22, 2022
    Configuration menu
    Copy the full SHA
    278691d View commit details
    Browse the repository at this point in the history

  3. Merge branch 'unit_tree' of https://github.com/leanprover-community/m… 

    …athlib into catalan_numbers_trees
    @prakol16
    prakol16 committed Oct 22, 2022
    Configuration menu
    Copy the full SHA
    e6cd603 View commit details
    Browse the repository at this point in the history

  4. Update for name change of nodes

    @prakol16
    prakol16 committed Oct 22, 2022
    Configuration menu
    Copy the full SHA
    1722d98 View commit details
    Browse the repository at this point in the history

  5. Fix naming of lemmas

    @prakol16
    prakol16 committed Oct 22, 2022
    Configuration menu
    Copy the full SHA
    79664c0 View commit details
    Browse the repository at this point in the history

  6. Merge branch 'unit_tree' of https://github.com/leanprover-community/m… 

    …athlib into catalan_numbers_trees
    @prakol16
    prakol16 committed Oct 22, 2022
    Configuration menu
    Copy the full SHA
    be8cb91 View commit details
    Browse the repository at this point in the history

Commits on Nov 14, 2022

  1. Add notation for tree unit instead of custom constructor

    @prakol16
    prakol16 committed Nov 14, 2022
    Configuration menu
    Copy the full SHA
    a552716 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'unit_tree' of https://github.com/leanprover-community/m… 

    …athlib into catalan_numbers_trees
    @prakol16
    prakol16 committed Nov 14, 2022
    Configuration menu
    Copy the full SHA
    aeaf435 View commit details
    Browse the repository at this point in the history

  3. Use new tree notation

    @prakol16
    prakol16 committed Nov 14, 2022
    Configuration menu
    Copy the full SHA
    910bde5 View commit details
    Browse the repository at this point in the history

Commits on Jan 27, 2023

  1. Merge branch 'master' of https://github.com/leanprover-community/mathlib 

     into catalan_numbers_trees
    @prakol16
    prakol16 committed Jan 27, 2023
    Configuration menu
    Copy the full SHA
    e524bb0 View commit details
    Browse the repository at this point in the history

  2. Fixes to disjoint change; add import

    @prakol16
    prakol16 committed Jan 27, 2023
    Configuration menu
    Copy the full SHA
    405277f View commit details
    Browse the repository at this point in the history

Commits on Jan 28, 2023

  1. Minor

    @prakol16
    prakol16 committed Jan 28, 2023
    Configuration menu
    Copy the full SHA
    556d70d View commit details
    Browse the repository at this point in the history

  2. Add coe_trees_of_nodes_eq

    @prakol16
    prakol16 committed Jan 28, 2023
    Configuration menu
    Copy the full SHA
    ad76105 View commit details
    Browse the repository at this point in the history

Commits on Jan 29, 2023

  1. Add norm cast attribute

    @prakol16
    prakol16 committed Jan 29, 2023
    Configuration menu
    Copy the full SHA
    01e9205 View commit details
    Browse the repository at this point in the history

Commits on Feb 2, 2023

  1. Shorten type declaration 

    Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
    @prakol16 @YaelDillies
    prakol16 and YaelDillies committed Feb 2, 2023
    Configuration menu
    Copy the full SHA
    dca3313 View commit details
    Browse the repository at this point in the history

Commits on Feb 3, 2023

  1. Change simp to reducible

    @prakol16
    prakol16 committed Feb 3, 2023
    Configuration menu
    Copy the full SHA
    a044a85 View commit details
    Browse the repository at this point in the history

  2. Oops, forgot to pull

    @prakol16
    prakol16 committed Feb 3, 2023
    Configuration menu
    Copy the full SHA
    884a197 View commit details
    Browse the repository at this point in the history

Commits on Feb 7, 2023

  1. golf

    @eric-wieser
    eric-wieser committed Feb 7, 2023
    Configuration menu
    Copy the full SHA
    3f879d6 View commit details
    Browse the repository at this point in the history

  2. wrap lines

    @eric-wieser
    eric-wieser committed Feb 7, 2023
    Configuration menu
    Copy the full SHA
    e73ec61 View commit details
    Browse the repository at this point in the history