The shape of a list of tableau rows

A list of rows satisfying List.IsTableauRows has weakly decreasing positive row lengths, so it determines a Young diagram List.tableauShape. Its row lengths are the lengths of the rows (List.rowLens_tableauShape) and its number of cells is the number of entries (List.card_tableauShape).

def List.tableauShape {α : Type u_1} [Preorder α] (rows : List (List α)) (hrows : rows.IsTableauRows) : YoungDiagram

The Young diagram whose row lengths are the lengths of a semistandard list of tableau rows.

@[simp]

theorem List.rowLens_tableauShape {α : Type u_1} [Preorder α] (rows : List (List α)) (hrows : rows.IsTableauRows) : (rows.tableauShape hrows).rowLens = map length rows

The row lengths of the shape inferred from tableau rows are the lengths of those rows.

@[simp]

theorem List.card_tableauShape {α : Type u_1} [Preorder α] (rows : List (List α)) (hrows : rows.IsTableauRows) : (rows.tableauShape hrows).card = rows.flatten.length

The number of cells in the shape inferred from tableau rows is the length of their flattening.