OAI/Algebra/AuslanderReiten/Evaluation/TensorTwistEvaluation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ArExplicit.T.sourceTwist_smul_simple line 16
  2. theorem OAI.ArExplicit.T.sourceInverseTwist_smul_simple line 40
  3. def OAI.ArExplicit.T.twistedSimpleEquiv line 46
  4. def OAI.ArExplicit.T.evaluatedTwistEquiv line 55
  5. theorem OAI.ArExplicit.T.evaluatedTwistEquiv_tmul line 59
  6. theorem OAI.ArExplicit.T.evaluatedTwistEquiv_unit line 64