OAI/Algebra/AuslanderReiten/Homology/ProjectiveNullhomotopyAbove.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.ArExplicit.ProjectiveNullhomotopyAbove.Pair line 18
2. theorem OAI.ArExplicit.ProjectiveNullhomotopyAbove.step line 30
3. def OAI.ArExplicit.ProjectiveNullhomotopyAbove.sequence line 37
4. theorem OAI.ArExplicit.ProjectiveNullhomotopyAbove.sequence_succ_lo line 42
5. theorem OAI.ArExplicit.ProjectiveNullhomotopyAbove.exists_homotopy line 50