OAI/Algebra/AuslanderReiten/Tensor/ExternalTensorDifferential.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ArExplicit.ExternalTensor.inclusion line 20
2. abbrev OAI.ArExplicit.ExternalTensor.desc line 24
3. theorem OAI.ArExplicit.ExternalTensor.inclusion_desc line 29
4. theorem OAI.ArExplicit.ExternalTensor.hom_ext line 36
5. abbrev OAI.ArExplicit.ExternalTensor.horizontal line 42
6. abbrev OAI.ArExplicit.ExternalTensor.vertical line 45
7. theorem OAI.ArExplicit.ExternalTensor.inclusion_d line 48
8. theorem OAI.ArExplicit.ExternalTensor.horizontal_succ line 57
9. theorem OAI.ArExplicit.ExternalTensor.vertical_succ line 65
10. theorem OAI.ArExplicit.ExternalTensor.horizontal_zero line 73
11. theorem OAI.ArExplicit.ExternalTensor.vertical_zero line 78
12. theorem OAI.ArExplicit.ExternalTensor.termDirectSumEquiv_inclusion line 83
13. theorem OAI.ArExplicit.ExternalTensor.inclusion_eq_directSum line 91