OrdinaryTensorMixedSign.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.LittleFinitistic.ComplexTensor.transport_d line 12
def OAI.LittleFinitistic.ComplexTensor.vertical line 19
Source documentation
Signed vertical tensor differential on the concrete balanced tensor term.
```
def vertical (n p : ℤ) : term k A Q Z p (n + -p) →ₗ[k] term k A Q Z p ((n+1) + -p) :=
…
```
Mentions: OAI.LittleFinitistic.ComplexTensor.term
theorem OAI.LittleFinitistic.ComplexTensor.horizontal_mixed line 23
Source documentation
The two mixed terms cancel with the actual integer total-complex signs.
```
theorem horizontal_mixed (n p p' : ℤ) (h : p+1=p') :
    (vertical k A Q Z (n+1) p').comp (horizontal k A Q Z n p p' h) +
      (horizontal k A Q Z (n+1) p p' h).comp (vertical k A Q Z n p) = 0 := by
…
```
Mentions: OAI.LittleFinitistic.ComplexTensor.vertical, OAI.LittleFinitistic.ComplexTensor.horizontal