-
Notifications
You must be signed in to change notification settings - Fork 298
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/young): define list of row lengths of a Young diagram #17061
Conversation
|
||
-/ | ||
|
||
-- This belongs somewhere in the list namespace. Is it already in mathlib? |
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.
Probably the best would be in data/list/range.lean
, but if list.sorted
isn't avaliable there, perhaps put these in data/list/sort.lean
?
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.
Found it: there is list.pairwise_lt_range
but no list.pairwise_le_range
. Adding it seems to mean all of mathlib has to be recompiled (since list
is so basic). Is there a way to speed it 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.
You can make the change, then push a commit to your branch; CI will run on it, and when it is done you can use leanproject get-cache
to download the compiled oleans.
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.
Done.
Co-authored-by: Kyle Miller <kmill31415@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.
Thanks!
bors r+
…ram (#17061) Define `row_lens : list ℕ`, the list of row lengths of a Young diagram and prove it is weakly decreasing and positive. This is the first half of the equivalence `young_diagram ≃ {w : list ℕ // w.sorted (≥) ∧ ∀ x ∈ w, 0 < x}`.
Pull request successfully merged into master. Build succeeded: |
Define
row_lens : list ℕ
, the list of row lengths of a Young diagram and prove it is weakly decreasing and positive.This is the first half of the equivalence
young_diagram ≃ {w : list ℕ // w.sorted (≥) ∧ ∀ x ∈ w, 0 < x}
.The rest of the equivalence will be established in a separate PR.
The fact that
list.range n
is a sorted list seems worth having in mathlib but I'm not sure where it would go. In thelist
namespace?