OAI/Algebra/AuslanderReiten/Complete/CompleteResolutionAllProjectives.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ArExplicit.HomExactAt.arbitrary_projective line 16
2. def OAI.ArExplicit.GorensteinProjectiveAllTargets line 52
3. theorem OAI.ArExplicit.GorensteinProjective.all_projective_targets line 62
4. theorem OAI.ArExplicit.gorensteinProjective_iff_all_projective_targets line 76