mathlib

936f0a83 - feat(combinatorics/young): define list of row lengths of a Young diagram (#17061)

feat(combinatorics/young): define list of row lengths of a Young diagram (#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}`.