BimoduleTotalDifferential.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

def OAI.LittleFinitistic.BimoduleTotal.horizontalBetween line 13
def OAI.LittleFinitistic.BimoduleTotal.entryBetween line 17
theorem OAI.LittleFinitistic.BimoduleTotal.total_d_apply line 24
Source documentation
The exact differential of the B-valued total, in arbitrary consecutive total degrees.
```
theorem total_d_apply (n m : ℤ) (h : n+1=m) (x : TotalTerm k B P p Z n) (j : Fin l) :
    ((total k B P p hp Z).d n m).hom x j =
      (show Term k B P Z (p j) (m + -(p j)) from
        ((ComplexTensor.column k B (right k B P) Z (p j)).d n m).hom (x j)) +
      ∑ i : Fin l, entryBetween k B P Z n m (p i) (p j) h (x i) := by
…
```
Mentions: OAI.LittleFinitistic.BimoduleTotal.TotalTerm, OAI.LittleFinitistic.BimoduleTotal.total, OAI.LittleFinitistic.BimoduleTotal.Term, OAI.LittleFinitistic.ComplexTensor.column, OAI.LittleFinitistic.BimoduleTotal.right, OAI.LittleFinitistic.BimoduleTotal.entryBetween