OAI/Algebra/AuslanderReiten/Tensor/ExternalTensorHomDifferential.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ArExplicit.ExternalTensor.homCochainInclusion_d_tmul line 15
2. abbrev OAI.ArExplicit.ExternalTensor.elementaryHom line 44
3. theorem OAI.ArExplicit.ExternalTensor.elementary_horizontal_same line 50
4. theorem OAI.ArExplicit.ExternalTensor.elementary_horizontal_zero line 65
5. theorem OAI.ArExplicit.ExternalTensor.elementary_vertical_same line 79
6. theorem OAI.ArExplicit.ExternalTensor.elementary_vertical_zero line 95
7. theorem OAI.ArExplicit.ExternalTensor.elementary_d line 110
8. def OAI.ArExplicit.ExternalTensor.homCochainTotalIso line 164