OAI/Algebra/AuslanderReiten/Bar/ModuleBarTwistExtAction.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ArExplicit.ModuleBar.twistExtAction_extMk line 20
  2. theorem OAI.ArExplicit.ModuleBar.transportedHom_closed line 39
  3. def OAI.ArExplicit.ModuleBar.transportedCochain line 45
  4. theorem OAI.ArExplicit.ModuleBar.transportedCochain_closed line 51
  5. theorem OAI.ArExplicit.ModuleBar.twistExtAction_extMk_transported line 61
  6. theorem OAI.ArExplicit.ModuleBar.extClass3_comp_extMk line 72
  7. theorem OAI.ArExplicit.ModuleBar.transportedCochain_cubic line 89
  8. theorem OAI.ArExplicit.ModuleBar.extMk_congr line 97
  9. theorem OAI.ArExplicit.ModuleBar.extMk_smul_native line 107
  10. theorem OAI.ArExplicit.ModuleBar.twistExtAction_cubic line 121