OAI/Algebra/Finitistic/Ordinary/OrdinaryBlockComplexes.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.BlockModule.firstComplex line 13
2. abbrev OAI.LittleFinitistic.BlockModule.secondComplex line 15
3. def OAI.LittleFinitistic.BlockModule.firstMap line 20
4. def OAI.LittleFinitistic.BlockModule.secondMap line 24
5. theorem OAI.LittleFinitistic.OrdinarySimulation.OffDiagonal.complex_d_all line 34