OAI/Algebra/AuslanderReiten/Algebras/TensorSimple.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ArExplicit.A.Simple line 17
  2. def OAI.ArExplicit.A.simpleCoordinate line 19
  3. theorem OAI.ArExplicit.A.simpleCoordinate_tmul line 23
  4. def OAI.ArExplicit.A.simpleCoordinateEquiv line 27
  5. theorem OAI.ArExplicit.A.simpleCoordinate_injective line 31
  6. def OAI.ArExplicit.A.simpleGenerator line 34
  7. theorem OAI.ArExplicit.A.simpleGenerator_coordinate line 36
  8. def OAI.ArExplicit.A.simpleCharacter line 39
  9. theorem OAI.ArExplicit.A.simpleCharacter_tmul line 43
  10. theorem OAI.ArExplicit.A.simpleCoordinate_smul line 46
  11. def OAI.ArExplicit.A.augmentationIdeal line 65
  12. instance OAI.ArExplicit.A.(instance at line 67) line 67
  13. theorem OAI.ArExplicit.A.augmentationIdeal_annihilates line 70
  14. def OAI.ArExplicit.A.socleMap line 77
  15. theorem OAI.ArExplicit.A.socleMap_tmul line 81
  16. theorem OAI.ArExplicit.A.socleMap_generator line 84
  17. theorem OAI.ArExplicit.A.socleMap_mem line 88
  18. def OAI.ArExplicit.A.beta line 103