OAI/Algebra/AuslanderReiten/HomComplex/FullHomHomotopyMaps.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ArExplicit.fullHomPostcomp_congr line 15
2. theorem OAI.ArExplicit.fullHomPrecomp_congr line 21
3. theorem OAI.ArExplicit.fullHomPostcomp_id line 27
4. theorem OAI.ArExplicit.fullHomPrecomp_id line 33
5. theorem OAI.ArExplicit.fullHomPostcomp_homotopy_inverse line 38
6. theorem OAI.ArExplicit.fullHomPostcomp_bijective line 45