OAI/Algebra/AuslanderReiten/Tensor/EnvelopingBalancedRegular.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ArExplicit.EnvelopingBimodule.regularObject line 15
  2. def OAI.ArExplicit.EnvelopingBimodule.unopAction line 18
  3. def OAI.ArExplicit.EnvelopingBimodule.regularRaw line 29
  4. theorem OAI.ArExplicit.EnvelopingBimodule.regularRaw_tmul line 38
  5. def OAI.ArExplicit.EnvelopingBimodule.regularBilinear line 41
  6. theorem OAI.ArExplicit.EnvelopingBimodule.regularBilinear_balance line 45
  7. theorem OAI.ArExplicit.EnvelopingBimodule.regularBilinear_left line 62
  8. def OAI.ArExplicit.EnvelopingBimodule.regularEvaluation line 78
  9. theorem OAI.ArExplicit.EnvelopingBimodule.regularEvaluation_tmul line 84
  10. def OAI.ArExplicit.EnvelopingBimodule.regularInclusion line 88
  11. def OAI.ArExplicit.EnvelopingBimodule.regularInverse line 93
  12. theorem OAI.ArExplicit.EnvelopingBimodule.regularInverse_tmul line 98
  13. theorem OAI.ArExplicit.EnvelopingBimodule.regularInverse_evaluation line 102
  14. theorem OAI.ArExplicit.EnvelopingBimodule.regularEvaluation_inverse line 123
  15. def OAI.ArExplicit.EnvelopingBimodule.regularEquiv line 129