OAI/Algebra/AuslanderReiten/Duality/ProjectiveTraceDuality.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.ArExplicit.FiniteProjectivePresentation line 12
2. def OAI.ArExplicit.FiniteProjectivePresentation.choose line 20
3. theorem OAI.ArExplicit.FiniteProjectivePresentation.split_apply line 30
4. def OAI.ArExplicit.FrobeniusTrace.presentationHomDualEquiv line 46
5. theorem OAI.ArExplicit.FrobeniusTrace.presentationHomDualEquiv_symm_apply line 64
6. theorem OAI.ArExplicit.FrobeniusTrace.presentationHomDual_naturality_source line 69
7. def OAI.ArExplicit.FrobeniusTrace.projectiveHomDualEquiv line 88
8. theorem OAI.ArExplicit.FrobeniusTrace.projectiveHomDual_precomp line 92
9. theorem OAI.ArExplicit.FrobeniusTrace.projectiveHomDual_naturality_target line 111