OAI/Algebra/AuslanderReiten/Duality/SymmetricHomology.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.ArExplicit.FrobeniusTrace.freeHomDual_precompline 20 - def
OAI.ArExplicit.FrobeniusTrace.freeHomHomologyDualityline 31 - def
OAI.ArExplicit.FrobeniusTrace.freeStableDualityline 45