OAI/Algebra/AuslanderReiten/Coordinates/TensorHighLift.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ArExplicit.T.productTwistedTotal line 20
2. def OAI.ArExplicit.T.tensorHighB line 22
3. def OAI.ArExplicit.T.tensorHighG line 25
4. theorem OAI.ArExplicit.T.tensorHighB_chain line 28
5. theorem OAI.ArExplicit.T.tensorHighG_homotopy line 40
6. theorem OAI.ArExplicit.T.tensorHighG_second line 57
7. theorem OAI.ArExplicit.T.tensorHighB_second line 62