Documentation Verification Report

SemistandardTableau

📁 Source: Mathlib/Combinatorics/Young/SemistandardTableau.lean

Statistics

Metric	Count
Definitions `SemistandardYoungTableau`, `copy`, `entry`, `highestWeight`, `instFunLike`, `instInhabited`	6
Theorems `coe_copy`, `col_strict`, `col_strict'`, `col_weak`, `copy_eq`, `ext`, `ext_iff`, `highestWeight_apply`, `row_weak`, `row_weak'`, `row_weak_of_le`, `to_fun_eq_coe`, `zeros`, `zeros'`	14
Total	20

SemistandardYoungTableau

Definitions

Name	Category	Theorems
`copy` 📖	CompOp	2 math math: `coe_copy`, `copy_eq`
`entry` 📖	CompOp	4 math math: `to_fun_eq_coe`, `row_weak'`, `zeros'`, `col_strict'`
`highestWeight` 📖	CompOp	1 math math: `highestWeight_apply`
`instFunLike` 📖	CompOp	8 math math: `to_fun_eq_coe`, `ext_iff`, `zeros`, `col_strict`, `row_weak_of_le`, `highestWeight_apply`, `col_weak`, `row_weak`
`instInhabited` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_copy` 📖	mathematical	`DFunLike.coe` `SemistandardYoungTableau` `instFunLike`	`copy`	—	—
`col_strict` 📖	mathematical	`YoungDiagram` `SetLike.instMembership` `YoungDiagram.instSetLikeProdNat`	`DFunLike.coe` `SemistandardYoungTableau` `instFunLike`	—	`col_strict'`
`col_strict'` 📖	mathematical	`YoungDiagram` `SetLike.instMembership` `YoungDiagram.instSetLikeProdNat`	`entry`	—	—
`col_weak` 📖	mathematical	`YoungDiagram` `SetLike.instMembership` `YoungDiagram.instSetLikeProdNat`	`DFunLike.coe` `SemistandardYoungTableau` `instFunLike`	—	`eq_or_lt_of_le` `le_refl` `le_of_lt` `col_strict`
`copy_eq` 📖	mathematical	`DFunLike.coe` `SemistandardYoungTableau` `instFunLike`	`copy`	—	`DFunLike.ext'`
`ext` 📖	—	`DFunLike.coe` `SemistandardYoungTableau` `instFunLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `SemistandardYoungTableau` `instFunLike`	—	`ext`
`highestWeight_apply` 📖	mathematical	—	`DFunLike.coe` `SemistandardYoungTableau` `instFunLike` `highestWeight` `YoungDiagram` `SetLike.instMembership` `YoungDiagram.instSetLikeProdNat` `YoungDiagram.decidableMem`	—	—
`row_weak` 📖	mathematical	`YoungDiagram` `SetLike.instMembership` `YoungDiagram.instSetLikeProdNat`	`DFunLike.coe` `SemistandardYoungTableau` `instFunLike`	—	`row_weak'`
`row_weak'` 📖	mathematical	`YoungDiagram` `SetLike.instMembership` `YoungDiagram.instSetLikeProdNat`	`entry`	—	—
`row_weak_of_le` 📖	mathematical	`YoungDiagram` `SetLike.instMembership` `YoungDiagram.instSetLikeProdNat`	`DFunLike.coe` `SemistandardYoungTableau` `instFunLike`	—	`eq_or_lt_of_le` `le_refl` `row_weak`
`to_fun_eq_coe` 📖	mathematical	—	`entry` `DFunLike.coe` `SemistandardYoungTableau` `instFunLike`	—	—
`zeros` 📖	mathematical	`YoungDiagram` `SetLike.instMembership` `YoungDiagram.instSetLikeProdNat`	`DFunLike.coe` `SemistandardYoungTableau` `instFunLike`	—	`zeros'`
`zeros'` 📖	mathematical	`YoungDiagram` `SetLike.instMembership` `YoungDiagram.instSetLikeProdNat`	`entry`	—	—

(root)

Definitions

Name	Category	Theorems
`SemistandardYoungTableau` 📖	CompData	8 math math: `SemistandardYoungTableau.to_fun_eq_coe`, `SemistandardYoungTableau.ext_iff`, `SemistandardYoungTableau.zeros`, `SemistandardYoungTableau.col_strict`, `SemistandardYoungTableau.row_weak_of_le`, `SemistandardYoungTableau.highestWeight_apply`, `SemistandardYoungTableau.col_weak`, `SemistandardYoungTableau.row_weak`

---

← Back to Index