Commit 2022-11-20 18:58 a22eb8a8

View on Github →

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}

Estimated changes