OAI/Algebra/AuslanderReiten/Bar/TCasimir.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ArExplicit.T.star_star line 15
  2. theorem OAI.ArExplicit.T.trace_mul_star line 19
  3. theorem OAI.ArExplicit.T.trace_vector_star line 26
  4. def OAI.ArExplicit.T.tensorRightCoordinates line 31
  5. theorem OAI.ArExplicit.T.tensorRightCoordinates_tmul line 35
  6. def OAI.ArExplicit.T.twistedCasimir line 39
  7. theorem OAI.ArExplicit.T.twistedCasimir_coordinates line 42
  8. theorem OAI.ArExplicit.T.coefficient_right_product line 58
  9. theorem OAI.ArExplicit.T.tensorRightCoordinates_left line 63
  10. theorem OAI.ArExplicit.T.twistedCasimir_equivariant line 73