OAI/Algebra/AuslanderReiten/Bar/ModuleBarTensorTwist.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ArExplicit.ModuleBar.nativeTensorTwist line 20
2. theorem OAI.ArExplicit.ModuleBar.nativeTensorTwist_kunneth line 29
3. def OAI.ArExplicit.ModuleBar.tensorTwist line 43
4. theorem OAI.ArExplicit.ModuleBar.tensorTwist_kunneth line 50
5. theorem OAI.ArExplicit.ModuleBar.nativeTensorTwist_kunneth_of_factors line 69
6. theorem OAI.ArExplicit.ModuleBar.tensorTwist_kunneth_of_factors line 77