OAI/Algebra/AuslanderReiten/Modules/ATwistedCompleteAction.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ArExplicit.T.completeTwistIn line 18
2. abbrev OAI.ArExplicit.T.completeTwistOut line 21
3. theorem OAI.ArExplicit.T.nativeEvaluationIso_eq line 26
4. theorem OAI.ArExplicit.T.completeTwist_inverse line 32
5. theorem OAI.ArExplicit.T.completeTwistIn_quotient line 39
6. theorem OAI.ArExplicit.T.completeTwistOut_quotient line 48
7. theorem OAI.ArExplicit.T.completeTwist_scalar line 55