OAI/Algebra/AuslanderReiten/Tensor/EnvelopingBalancedMap.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ArExplicit.EnvelopingBimodule.map line 19
  2. theorem OAI.ArExplicit.EnvelopingBimodule.map_value line 28
  3. theorem OAI.ArExplicit.EnvelopingBimodule.map_left_smul line 31
  4. theorem OAI.ArExplicit.EnvelopingBimodule.map_right_smul line 36
  5. def OAI.ArExplicit.EnvelopingBimodule.mapLeft line 41
  6. theorem OAI.ArExplicit.EnvelopingBimodule.map_id line 46
  7. theorem OAI.ArExplicit.EnvelopingBimodule.map_comp line 50
  8. theorem OAI.ArExplicit.EnvelopingBimodule.map_zero line 55
  9. theorem OAI.ArExplicit.EnvelopingBimodule.map_add line 59
  10. def OAI.ArExplicit.EnvelopingBimodule.tensorMap line 65
  11. theorem OAI.ArExplicit.EnvelopingBimodule.tensorMap_tmul line 83
  12. theorem OAI.ArExplicit.EnvelopingBimodule.tensorMap_id line 87
  13. theorem OAI.ArExplicit.EnvelopingBimodule.tensorMap_comp line 95
  14. theorem OAI.ArExplicit.EnvelopingBimodule.tensorMap_zero line 104
  15. theorem OAI.ArExplicit.EnvelopingBimodule.tensorMap_add line 112