Commit 2023-02-03 07:30 616115e6

View on Github →

feat: port Combinatorics.Young.YoungDiagram (#1994)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Combinatorics/Young/YoungDiagram.lean

added theorem YoungDiagram.cells_bot

added theorem YoungDiagram.cells_inf

added theorem YoungDiagram.cells_sSubset_iff

added theorem YoungDiagram.cells_subset_iff

added theorem YoungDiagram.cells_sup

added theorem YoungDiagram.coe_bot

added theorem YoungDiagram.coe_inf

added theorem YoungDiagram.coe_sup

added def YoungDiagram.col

added def YoungDiagram.colLen

added theorem YoungDiagram.colLen_anti

added theorem YoungDiagram.colLen_eq_card

added theorem YoungDiagram.colLen_transpose

added theorem YoungDiagram.col_eq_prod

added def YoungDiagram.equivListRowLens

added theorem YoungDiagram.get_rowLens

added theorem YoungDiagram.length_rowLens

added theorem YoungDiagram.mem_cells

added theorem YoungDiagram.mem_col_iff

added theorem YoungDiagram.mem_iff_lt_colLen

added theorem YoungDiagram.mem_iff_lt_rowLen

added theorem YoungDiagram.mem_inf

added theorem YoungDiagram.mem_mk

added theorem YoungDiagram.mem_ofRowLens

added theorem YoungDiagram.mem_row_iff

added theorem YoungDiagram.mem_sup

added theorem YoungDiagram.mem_transpose

added theorem YoungDiagram.mk_mem_col_iff

added theorem YoungDiagram.mk_mem_row_iff

added theorem YoungDiagram.not_mem_bot

added def YoungDiagram.ofRowLens

added theorem YoungDiagram.ofRowLens_to_rowLens_eq_self

added theorem YoungDiagram.pos_of_mem_rowLens

added def YoungDiagram.row

added def YoungDiagram.rowLen

added theorem YoungDiagram.rowLen_anti

added theorem YoungDiagram.rowLen_eq_card

added theorem YoungDiagram.rowLen_ofRowLens

added theorem YoungDiagram.rowLen_transpose

added def YoungDiagram.rowLens

added theorem YoungDiagram.rowLens_length_ofRowLens

added theorem YoungDiagram.rowLens_ofRowLens_eq_self

added theorem YoungDiagram.rowLens_sorted

added theorem YoungDiagram.row_eq_prod

added def YoungDiagram.transpose

added def YoungDiagram.transposeOrderIso

added theorem YoungDiagram.transpose_eq_iff

added theorem YoungDiagram.transpose_eq_iff_eq_transpose

added theorem YoungDiagram.transpose_le_iff

added theorem YoungDiagram.transpose_transpose

added theorem YoungDiagram.up_left_mem

added structure YoungDiagram