OAI/Probability/BinarySweep/GridBounds/DiagonalRigidity.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BinaryCoordinateSweeps.Young.diagonal_rigidity_aux line 14
2. def OAI.BinaryCoordinateSweeps.Young.diagonal line 55
3. abbrev OAI.BinaryCoordinateSweeps.Young.diagonalStabilizer line 56
4. instance OAI.BinaryCoordinateSweeps.Young.diagonalStabilizer_fintype line 57
5. lemma OAI.BinaryCoordinateSweeps.Young.diagonal_row_column line 60
6. lemma OAI.BinaryCoordinateSweeps.Young.diagonal_column_row line 83
7. lemma OAI.BinaryCoordinateSweeps.Young.diagonal_tabloid_eq line 92
8. lemma OAI.BinaryCoordinateSweeps.Young.diagonal_poly_coefficient line 110
9. theorem OAI.BinaryCoordinateSweeps.Young.diagonal_polytabloids_independent line 125
10. theorem OAI.BinaryCoordinateSweeps.Young.diagonal_card_le_dimension line 135
11. def OAI.BinaryCoordinateSweeps.Young.fiberQuotientLabel line 150
12. lemma OAI.BinaryCoordinateSweeps.Young.fiberQuotientLabel_injective line 160
13. theorem OAI.BinaryCoordinateSweeps.Young.factorial_le_colorings_mul_stabilizer line 172