OAI/Algebra/AuslanderReiten/Duality/SymmetricStableDuality.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ArExplicit.FrobeniusTrace.regularFromDual line 18
  2. def OAI.ArExplicit.FrobeniusTrace.dualFromRegular line 21
  3. theorem OAI.ArExplicit.FrobeniusTrace.trace_leftEquiv_symm line 24
  4. theorem OAI.ArExplicit.FrobeniusTrace.dualFromRegular_regularFromDual line 30
  5. theorem OAI.ArExplicit.FrobeniusTrace.regularFromDual_dualFromRegular line 37
  6. def OAI.ArExplicit.FrobeniusTrace.dualModuleHomEquiv line 49
  7. theorem OAI.ArExplicit.FrobeniusTrace.dualModuleHomEquiv_precomp line 76
  8. def OAI.ArExplicit.FrobeniusTrace.freeHomDualEquiv line 90
  9. theorem OAI.ArExplicit.FrobeniusTrace.freeHomDualEquiv_symm_apply line 97
  10. theorem OAI.ArExplicit.FrobeniusTrace.free_map_apply line 104
  11. def OAI.ArExplicit.FrobeniusTrace.freeTrace line 113
  12. theorem OAI.ArExplicit.FrobeniusTrace.trace_map_coordinate line 117
  13. theorem OAI.ArExplicit.FrobeniusTrace.freeTrace_cyclic line 125
  14. theorem OAI.ArExplicit.FrobeniusTrace.freeHomDual_naturality_source line 138
  15. theorem OAI.ArExplicit.FrobeniusTrace.freeHomDual_naturality_target line 147