OAI/RepresentationTheory/UniversalSquare/Contraction/RowCertificates.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniversalTensorSquare.rowDiagram line 17
2. def OAI.UniversalTensorSquare.GoodRows line 19
3. instance OAI.UniversalTensorSquare.(instance at line 20) line 20
4. lemma OAI.UniversalTensorSquare.rowDiagram_eq line 22
5. lemma OAI.UniversalTensorSquare.rowDiagram_rows line 26
6. lemma OAI.UniversalTensorSquare.rowDiagram_card line 29
7. lemma OAI.UniversalTensorSquare.rowDiagram_rowLen line 32
8. lemma OAI.UniversalTensorSquare.rowDiagram_height line 36
9. lemma OAI.UniversalTensorSquare.rowDiagram_rowLens line 40
10. def OAI.UniversalTensorSquare.RowsStrip line 44
11. instance OAI.UniversalTensorSquare.(instance at line 47) line 47
12. lemma OAI.UniversalTensorSquare.rowsStrip_sound line 50
13. def OAI.UniversalTensorSquare.RowsChain line 63
14. def OAI.UniversalTensorSquare.stripSizes line 69
15. def OAI.UniversalTensorSquare.ChainValid line 73
16. instance OAI.UniversalTensorSquare.(instance at line 76) line 76
17. lemma OAI.UniversalTensorSquare.SizedStripChain.trans line 84
18. lemma OAI.UniversalTensorSquare.chainValid_sound line 91
19. def OAI.UniversalTensorSquare.RowsDom line 101
20. instance OAI.UniversalTensorSquare.(instance at line 103) line 103
21. lemma OAI.UniversalTensorSquare.rowsDom_of_dominates line 105
22. lemma OAI.UniversalTensorSquare.dominates_of_rowsDom line 110
23. lemma OAI.UniversalTensorSquare.height_le_of_dominates line 121