OAI/Algebra/AuslanderReiten/Homology/VectorTensorKunneth.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.ArExplicit.VectorComplex.hasMapBifunctor line 20
2. theorem OAI.ArExplicit.VectorComplex.totalMap_quasiIso line 23
3. theorem OAI.ArExplicit.VectorComplex.total_zero_differential line 30
4. def OAI.ArExplicit.VectorComplex.totalZeroHomologyIso line 56
5. def OAI.ArExplicit.VectorComplex.tensorSplitting line 68
6. def OAI.ArExplicit.VectorComplex.kunnethIso line 74
7. theorem OAI.ArExplicit.VectorComplex.tensorSplitting_hom line 80
8. theorem OAI.ArExplicit.VectorComplex.kunnethIso_inv line 85
9. def OAI.ArExplicit.VectorComplex.kunnethLinearEquiv line 93