OAI/Algebra/AuslanderReiten/Ext/ExtKunnethMap.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ArExplicit.ExternalTensor.tensor_conjugate line 14
2. theorem OAI.ArExplicit.ExternalTensor.homology_conjugate line 28
3. def OAI.ArExplicit.ExternalTensor.nativeHomEndExt line 45
4. def OAI.ArExplicit.ExternalTensor.homTensorMap line 60
5. def OAI.ArExplicit.ExternalTensor.homKunnethCoordinates line 67
6. theorem OAI.ArExplicit.ExternalTensor.homKunnethCoordinates_natural line 77
7. def OAI.ArExplicit.ExternalTensor.tensorHomEndExt line 91
8. theorem OAI.ArExplicit.ExternalTensor.extKunnethEquiv_apply line 98
9. theorem OAI.ArExplicit.ExternalTensor.extKunnethEquiv_tensorHomEndExt line 108