OAI/Algebra/AuslanderReiten/Bar/TCasimirEvaluation.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.ArExplicit.T.simpleActionAtline 15 - theorem
OAI.ArExplicit.T.simpleActionAt_applyline 18 - def
OAI.ArExplicit.T.evaluateAtSimpleline 20 - theorem
OAI.ArExplicit.T.twistedCasimir_evaluationline 23 - def
OAI.ArExplicit.T.evaluatedDetectorline 40 - theorem
OAI.ArExplicit.T.evaluatedDetector_tmulline 44 - theorem
OAI.ArExplicit.T.twistedCasimir_evaluation_ne_zeroline 48