# Documentation

Mathlib.Combinatorics.Young.YoungDiagram

# Young diagrams #

A Young diagram is a finite set of up-left justified boxes:

□□□□□
□□□
□□□
□


This Young diagram corresponds to the [5, 3, 3, 1] partition of 12.

We represent it as a lower set in ℕ × ℕ in the product partial order. We write (i, j) ∈ μ to say that (i, j) (in matrix coordinates) is in the Young diagram μ.

## Main definitions #

• YoungDiagram : Young diagrams
• YoungDiagram.card : the number of cells in a Young diagram (its cardinality)
• YoungDiagram.instDistribLatticeYoungDiagram : a distributive lattice instance for Young diagrams ordered by containment, with (⊥ : YoungDiagram) the empty diagram.
• YoungDiagram.row and YoungDiagram.rowLen: rows of a Young diagram and their lengths
• YoungDiagram.col and YoungDiagram.colLen: columns of a Young diagram and their lengths

## Notation #

In "English notation", a Young diagram is drawn so that (i1, j1) ≤ (i2, j2) means (i1, j1) is weakly up-and-left of (i2, j2). This terminology is used below, e.g. in YoungDiagram.up_left_mem.

## Tags #

Young diagram

https://en.wikipedia.org/wiki/Young_tableau