OAI/RingTheory/Multiplicity/TotalExact.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Lech.BicomplexTotal.Diagonal line 11
2. def OAI.Lech.BicomplexTotal.diagonal line 13
3. instance OAI.Lech.BicomplexTotal.diagonal_preservesFiniteLimits line 17
4. instance OAI.Lech.BicomplexTotal.diagonal_preservesFiniteColimits line 22
5. instance OAI.Lech.BicomplexTotal.diagonal_additive line 27
6. lemma OAI.Lech.BicomplexTotal.diagonal_colim_map line 30
7. def OAI.Lech.BicomplexTotal.totalDegreeIso line 41
8. lemma OAI.Lech.BicomplexTotal.total_shortExact line 46