OAI/Algebra/AuslanderReiten/Algebras/TensorStructure.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ArExplicit.A line 12
  2. theorem OAI.ArExplicit.A_finrank line 14
  3. def OAI.ArExplicit.A.quotientCoordinates line 21
  4. theorem OAI.ArExplicit.A.quotient_jacobson line 26
  5. def OAI.ArExplicit.A.quotientTensorMap line 32
  6. def OAI.ArExplicit.A.diagonalAlg line 35
  7. theorem OAI.ArExplicit.A.radical_eq_ker_tensorMap line 38
  8. theorem OAI.ArExplicit.A.radical_eq_ker_diagonal line 46
  9. theorem OAI.ArExplicit.A.diagonalAlg_surjective line 59
  10. def OAI.ArExplicit.A.semisimpleQuotientEquiv line 64
  11. def OAI.ArExplicit.A.radicalU line 69
  12. def OAI.ArExplicit.A.radicalT line 70
  13. theorem OAI.ArExplicit.A.left_radical_mem line 72
  14. theorem OAI.ArExplicit.A.radicalU_mem line 79
  15. theorem OAI.ArExplicit.A.radicalT_mem line 84
  16. def OAI.ArExplicit.A.originalProjection line 89
  17. theorem OAI.ArExplicit.A.originalProjection_radicalU line 95
  18. theorem OAI.ArExplicit.A.originalProjection_radicalT line 99
  19. theorem OAI.ArExplicit.A.fourfold_product_ne_zero line 103
  20. theorem OAI.ArExplicit.A.jacobson_fourth_ne_bot line 110