Theorems · Inductive type · combinatorics
YoungDiagram
Type
A Young diagram is a finite collection of cells on the ℕ × ℕ grid such that whenever
a cell is present, so are all the ones above and to the left of it. Like matrices, an (i, j) cell
is a cell in row i and column j, where rows are enumerated downward and columns rightward.
Young diagrams are modeled as finite sets in ℕ × ℕ that are lower sets with respect to the
standard order on products.
- Defined in
- Mathlib.Combinatorics.Young.YoungDiagram
- Cited by
- 72 results in Mathlib
- Foundations
- Depth 0 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by99
Results whose statement or proof uses this declaration.
- SemistandardYoungTableaustatement · cited by 17
- YoungDiagram.cellsstatement and proof · cited by 16
- YoungDiagram.rowLenstatement and proof · cited by 13
- YoungDiagram.transposestatement and proof · cited by 13
- YoungDiagram.colLenstatement and proof · cited by 10
- YoungDiagram.rowLensstatement and proof · cited by 8
- YoungDiagram.ofRowLensstatement · cited by 7
- YoungDiagram.exists_notMem_rowstatement and proof · cited by 5
- SemistandardYoungTableau.entrystatement and proof · cited by 4
- YoungDiagram.colstatement and proof · cited by 4
- YoungDiagram.rowstatement and proof · cited by 4
- YoungDiagram.transpose_transposestatement and proof · cited by 3