OAI/Probability/BinarySweep/YoungTheory/YoungPartition.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.BinaryCoordinateSweeps.Young.card_cellsOfRowLensline 11 - def
OAI.BinaryCoordinateSweeps.Young.diagramline 26 - lemma
OAI.BinaryCoordinateSweeps.Young.diagram_cardline 29 - lemma
OAI.BinaryCoordinateSweeps.Young.diagram_rowLensline 33 - lemma
OAI.BinaryCoordinateSweeps.Young.diagram_injectiveline 40 - def
OAI.BinaryCoordinateSweeps.Young.cellsEquivFinline 46 - def
OAI.BinaryCoordinateSweeps.Young.conjPartitionline 49 - lemma
OAI.BinaryCoordinateSweeps.Young.conjPartition_injectiveline 53