OAI/Algebra/AuslanderReiten/Homology/VectorCochainKunneth.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.ArExplicit.VectorCochain.hasMapBifunctor line 21
2. theorem OAI.ArExplicit.VectorCochain.totalMap_quasiIso line 24
3. theorem OAI.ArExplicit.VectorCochain.total_zero_differential line 31
4. def OAI.ArExplicit.VectorCochain.totalZeroHomologyIso line 51
5. def OAI.ArExplicit.VectorCochain.tensorSplitting line 63
6. def OAI.ArExplicit.VectorCochain.kunnethIso line 69
7. theorem OAI.ArExplicit.VectorCochain.tensorSplitting_hom line 75
8. theorem OAI.ArExplicit.VectorCochain.kunnethIso_inv line 80
9. def OAI.ArExplicit.VectorCochain.kunnethLinearEquiv line 88