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(order/height): The height of a poset #15026

Closed
wants to merge 28 commits into from
Closed

[Merged by Bors] - feat(order/height): The height of a poset #15026

wants to merge 28 commits into from

Commits on Jun 28, 2022

  1. first commit

    @erdOne
    erdOne committed Jun 28, 2022
    Copy the full SHA
    8bac7b9 View commit details
    Browse the repository at this point in the history

  2. address comments

    @erdOne
    erdOne committed Jun 28, 2022
    Copy the full SHA
    94780ad View commit details
    Browse the repository at this point in the history

  3. use preorder

    @erdOne
    erdOne committed Jun 28, 2022
    Copy the full SHA
    161a14b View commit details
    Browse the repository at this point in the history

  4. use has_lt

    @erdOne
    erdOne committed Jun 28, 2022
    Copy the full SHA
    b4277f7 View commit details
    Browse the repository at this point in the history

Commits on Aug 17, 2022

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

     into chain_length
    @erdOne
    erdOne committed Aug 17, 2022
    Copy the full SHA
    7e4b7a2 View commit details
    Browse the repository at this point in the history

  2. change approach

    @erdOne
    erdOne committed Aug 17, 2022
    Copy the full SHA
    bef20f1 View commit details
    Browse the repository at this point in the history

Commits on Oct 11, 2022

  1. Update height.lean

    @erdOne
    erdOne committed Oct 11, 2022
    Copy the full SHA
    b9c3a79 View commit details
    Browse the repository at this point in the history

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

     into chain_length
    @erdOne
    erdOne committed Oct 11, 2022
    Copy the full SHA
    b83383d View commit details
    Browse the repository at this point in the history

  3. Merge branch 'chain_length' of https://github.com/leanprover-communit… 

    …y/mathlib into chain_length
    @erdOne
    erdOne committed Oct 11, 2022
    Copy the full SHA
    bdf7dc6 View commit details
    Browse the repository at this point in the history

Commits on Oct 16, 2022

  1. tidy up

    @erdOne
    erdOne committed Oct 16, 2022
    Copy the full SHA
    3f2f30a View commit details
    Browse the repository at this point in the history

  2. Update height.lean

    @erdOne
    erdOne committed Oct 16, 2022
    Copy the full SHA
    f0fe339 View commit details
    Browse the repository at this point in the history

  3. fix

    @erdOne
    erdOne committed Oct 16, 2022
    Copy the full SHA
    42c73e1 View commit details
    Browse the repository at this point in the history

Commits on Jan 19, 2023

  1. Merge remote-tracking branch 'origin/master' into chain_length

    @YaelDillies
    YaelDillies committed Jan 19, 2023
    Copy the full SHA
    ef96806 View commit details
    Browse the repository at this point in the history

  2. bump, cleanup, golf

    @YaelDillies
    YaelDillies committed Jan 19, 2023
    Copy the full SHA
    2cd5b82 View commit details
    Browse the repository at this point in the history

Commits on Jan 21, 2023

  1. Junyan's changes + further golf

    @YaelDillies
    YaelDillies committed Jan 21, 2023
    Copy the full SHA
    4db0f0f View commit details
    Browse the repository at this point in the history

  2. chain_height_mono

    @YaelDillies
    YaelDillies committed Jan 21, 2023
    Copy the full SHA
    5625150 View commit details
    Browse the repository at this point in the history

  3. fix imports

    @YaelDillies
    YaelDillies committed Jan 21, 2023
    Copy the full SHA
    e8d0107 View commit details
    Browse the repository at this point in the history

Commits on Jan 22, 2023

  1. golf

    @alreadydone
    alreadydone committed Jan 22, 2023
    Copy the full SHA
    a78272d View commit details
    Browse the repository at this point in the history

  2. pairwise_of_fn lemmas + golf

    @alreadydone
    alreadydone committed Jan 22, 2023
    Copy the full SHA
    1cd2595 View commit details
    Browse the repository at this point in the history

  3. formatting

    @alreadydone
    alreadydone committed Jan 22, 2023
    Copy the full SHA
    c3ca834 View commit details
    Browse the repository at this point in the history

  4. formatting

    @alreadydone
    alreadydone committed Jan 22, 2023
    Copy the full SHA
    0e49b5f View commit details
    Browse the repository at this point in the history

  5. missing end preorder

    @alreadydone
    alreadydone committed Jan 22, 2023
    Copy the full SHA
    d0dbb3c View commit details
    Browse the repository at this point in the history

  6. move list.pairwise_of_fn

    @YaelDillies
    YaelDillies committed Jan 22, 2023
    Copy the full SHA
    1c7835d View commit details
    Browse the repository at this point in the history

  7. too focused on rel_hom that I missed obvious golf

    @alreadydone
    alreadydone committed Jan 22, 2023
    Copy the full SHA
    54e08dc View commit details
    Browse the repository at this point in the history

  8. already in list namespace 

    Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
    @alreadydone @eric-wieser
    alreadydone and eric-wieser committed Jan 22, 2023
    Copy the full SHA
    457ab19 View commit details
    Browse the repository at this point in the history

Commits on Jan 24, 2023

  1. iff version of pairwise_of_fn

    @YaelDillies
    YaelDillies committed Jan 24, 2023
    Copy the full SHA
    7d6795d View commit details
    Browse the repository at this point in the history

  2. reorder imports

    @YaelDillies
    YaelDillies committed Jan 24, 2023
    Copy the full SHA
    95e0c8e View commit details
    Browse the repository at this point in the history

Commits on Jan 26, 2023

  1. fix

    @alreadydone
    alreadydone committed Jan 26, 2023
    Copy the full SHA
    b860941 View commit details
    Browse the repository at this point in the history