OAI/Algebra/FinitisticAsymmetry/Triangular/Algebra.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.TriangularConstruction.OffDiagonal line 17
2. def OAI.LittleFinitistic.TriangularConstruction.offValue line 19
3. instance OAI.LittleFinitistic.TriangularConstruction.OffDiagonal.(instance at line 24) line 24
4. instance OAI.LittleFinitistic.TriangularConstruction.OffDiagonal.(instance at line 26) line 26
5. instance OAI.LittleFinitistic.TriangularConstruction.OffDiagonal.(instance at line 29) line 29
6. instance OAI.LittleFinitistic.TriangularConstruction.OffDiagonal.(instance at line 32) line 32
7. instance OAI.LittleFinitistic.TriangularConstruction.OffDiagonal.(instance at line 41) line 41
8. instance OAI.LittleFinitistic.TriangularConstruction.OffDiagonal.(instance at line 43) line 43
9. instance OAI.LittleFinitistic.TriangularConstruction.OffDiagonal.(instance at line 49) line 49
10. instance OAI.LittleFinitistic.TriangularConstruction.OffDiagonal.(instance at line 56) line 56
11. abbrev OAI.LittleFinitistic.TriangularConstruction.Algebra line 61
12. lemma OAI.LittleFinitistic.TriangularConstruction.mul_formula line 67
13. def OAI.LittleFinitistic.TriangularConstruction.toC line 71
14. lemma OAI.LittleFinitistic.TriangularConstruction.toC_surjective line 79
15. def OAI.LittleFinitistic.TriangularConstruction.rightCornerSection line 82
16. lemma OAI.LittleFinitistic.TriangularConstruction.rightCorner_projective line 102
17. lemma OAI.LittleFinitistic.TriangularConstruction.right_little_lower_bound line 110
18. lemma OAI.LittleFinitistic.TriangularConstruction.right_big_lower_bound line 118
19. lemma OAI.LittleFinitistic.TriangularConstruction.finiteDimensional line 132