OAI/Algebra/AuslanderReiten/Tensor/EnvelopingBalancedProjective.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.ArExplicit.EnvelopingBimodule.finitePiProjective line 19
  2. instance OAI.ArExplicit.EnvelopingBimodule.regular_projective line 24
  3. abbrev OAI.ArExplicit.EnvelopingBimodule.piObject line 31
  4. def OAI.ArExplicit.EnvelopingBimodule.piProjection line 34
  5. def OAI.ArExplicit.EnvelopingBimodule.piInclusion line 37
  6. def OAI.ArExplicit.EnvelopingBimodule.tensorPiCoordinates line 40
  7. def OAI.ArExplicit.EnvelopingBimodule.tensorPiRecombine line 45
  8. theorem OAI.ArExplicit.EnvelopingBimodule.tensorPiRecombine_apply line 51
  9. theorem OAI.ArExplicit.EnvelopingBimodule.pi_reconstruct line 56
  10. theorem OAI.ArExplicit.EnvelopingBimodule.tensorPi_retraction line 65
  11. theorem OAI.ArExplicit.EnvelopingBimodule.tensorPi_projective line 84
  12. theorem OAI.ArExplicit.EnvelopingBimodule.tensor_projective line 90