OAI/Algebra/Finitistic/Dimension/PDMinimalData.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.LittleFinitistic.PDMinimal.FiniteModule line 13

   Source documentation

   Finite-dimensional actual left modules, retaining the scalar compatibility.

   structure FiniteModule where
   …

2. instance OAI.LittleFinitistic.PDMinimal.(instance at line 22) line 22
3. abbrev OAI.LittleFinitistic.PDMinimal.FiniteModule.of line 26
4. def OAI.LittleFinitistic.PDMinimal.FiniteModule.cat line 28
5. instance OAI.LittleFinitistic.PDMinimal.FiniteModule.(instance at line 29) line 29
6. structure OAI.LittleFinitistic.PDMinimal.Cover line 35

   Source documentation

   Projective covers with their actual maps and radical-kernel property.

   structure Cover (M : FiniteModule k A) where
   …

   Mentions: OAI.LittleFinitistic.PDMinimal.FiniteModule

7. theorem OAI.LittleFinitistic.PDMinimal.cover_nonempty line 45
8. def OAI.LittleFinitistic.PDMinimal.cover line 54
9. abbrev OAI.LittleFinitistic.PDMinimal.next line 56
10. def OAI.LittleFinitistic.PDMinimal.syzygy line 62
11. abbrev OAI.LittleFinitistic.PDMinimal.term line 66
12. abbrev OAI.LittleFinitistic.PDMinimal.augment line 67
13. def OAI.LittleFinitistic.PDMinimal.differential line 69
14. theorem OAI.LittleFinitistic.PDMinimal.augment_differential line 72
15. theorem OAI.LittleFinitistic.PDMinimal.differential_comp line 77
16. theorem OAI.LittleFinitistic.PDMinimal.range_differential line 81
17. theorem OAI.LittleFinitistic.PDMinimal.ker_differential line 86
18. theorem OAI.LittleFinitistic.PDMinimal.exact_differential line 95
19. theorem OAI.LittleFinitistic.PDMinimal.differential_radical line 99