OAI/Algebra/AuslanderReiten/Tensor/ExternalTensorTransport.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ArExplicit.ExternalTensor.tensorRestriction line 15
2. theorem OAI.ArExplicit.ExternalTensor.tensorSemilinear_natural line 33
3. def OAI.ArExplicit.ExternalTensor.transportSummand line 59
4. def OAI.ArExplicit.ExternalTensor.transportTerm line 65
5. theorem OAI.ArExplicit.ExternalTensor.inclusion_transportTerm line 71
6. theorem OAI.ArExplicit.ExternalTensor.horizontal_transport line 81
7. theorem OAI.ArExplicit.ExternalTensor.vertical_transport line 97
8. def OAI.ArExplicit.ExternalTensor.transportComplex line 114