OAI/Algebra/AuslanderReiten/Homology/VectorCochainNaturality.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ArExplicit.VectorCochain.zeroHomologyIso_natural line 11
2. def OAI.ArExplicit.VectorCochain.gradedMap line 22
3. theorem OAI.ArExplicit.VectorCochain.homologyMap_splitting_inv line 26
4. theorem OAI.ArExplicit.VectorCochain.representatives_comp_splitting_inv line 36
5. def OAI.ArExplicit.VectorCochain.representativesNaturality line 50