OAI/Algebra/AuslanderReiten/Duality/SymmetricPairing.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.ArExplicit.FrobeniusTrace.freeHomHomologyDuality_symm_applyline 18 - theorem
OAI.ArExplicit.FrobeniusTrace.freeStableDuality_symm_cyclesline 27 - theorem
OAI.ArExplicit.FrobeniusTrace.freeStableDuality_symm_applyline 53 - theorem
OAI.ArExplicit.FrobeniusTrace.freeStableDuality_naturalline 68