OAI/Algebra/FinitisticAsymmetry/Triangular/Socle.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.CummingsConstruction.NewCorner line 16
2. instance OAI.LittleFinitistic.CummingsConstruction.(instance at line 18) line 18
3. def OAI.LittleFinitistic.CummingsConstruction.newAugmentation line 22
4. def OAI.LittleFinitistic.CummingsConstruction.SimpleSum line 25
5. def OAI.LittleFinitistic.CummingsConstruction.SimpleSum.value line 28
6. instance OAI.LittleFinitistic.CummingsConstruction.SimpleSum.(instance at line 30) line 30
7. instance OAI.LittleFinitistic.CummingsConstruction.SimpleSum.(instance at line 31) line 31
8. instance OAI.LittleFinitistic.CummingsConstruction.SimpleSum.(instance at line 32) line 32
9. instance OAI.LittleFinitistic.CummingsConstruction.SimpleSum.(instance at line 33) line 33
10. def OAI.LittleFinitistic.CummingsConstruction.SimpleSum.rightCharacter line 36
11. instance OAI.LittleFinitistic.CummingsConstruction.SimpleSum.(instance at line 43) line 43
12. instance OAI.LittleFinitistic.CummingsConstruction.SimpleSum.(instance at line 45) line 45
13. instance OAI.LittleFinitistic.CummingsConstruction.SimpleSum.(instance at line 51) line 51
14. instance OAI.LittleFinitistic.CummingsConstruction.SimpleSum.(instance at line 56) line 56
15. abbrev OAI.LittleFinitistic.CummingsConstruction.T line 63
16. instance OAI.LittleFinitistic.CummingsConstruction.(instance at line 65) line 65
17. instance OAI.LittleFinitistic.CummingsConstruction.(instance at line 66) line 66
18. def OAI.LittleFinitistic.CummingsConstruction.augmentation line 69
19. lemma OAI.LittleFinitistic.CummingsConstruction.augmentation_surjective line 77
20. def OAI.LittleFinitistic.CummingsConstruction.socle line 88
21. lemma OAI.LittleFinitistic.CummingsConstruction.socle_ne_zero line 92
22. lemma OAI.LittleFinitistic.CummingsConstruction.socle_mul line 103