mathlib3

a22eb8a8 - feat(combinatorics/young): add equivalence between Young diagrams and lists of natural numbers (#17445)

feat(combinatorics/young): add equivalence between Young diagrams and lists of natural numbers (#17445) Construct the equivalence between Young diagrams and weakly decreasing lists of positive natural numbers: `equiv_list_row_lens : young_diagram ≃ {w : list ℕ // w.sorted (≥) ∧ ∀ x ∈ w, 0 < x}` Co-authored-by: Kyle Miller <kmill31415@gmail.com>