OAI/Algebra/AuslanderReiten/Modules/ATwistFunctor.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ArExplicit.Resolution.aInverseRestriction line 15
2. instance OAI.ArExplicit.Resolution.aInverseRestriction_isEquivalence line 18
3. def OAI.ArExplicit.Resolution.aInverseEndpoint line 23
4. theorem OAI.ArExplicit.Resolution.aInverseEndpoint_apply line 31
5. theorem OAI.ArExplicit.Resolution.aInverseRestriction_eq line 39
6. theorem OAI.ArExplicit.Resolution.aInverseTwist_standard line 43
7. theorem OAI.ArExplicit.Resolution.aInverseTwist_standard_scalar line 55