OrdinarySourceBimoduleTotal.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

def OAI.LittleFinitistic.OrdinarySimulation.sourceBimoduleTotalComparison line 19
Source documentation
The source signed total comparison for every Z, with the actual outside B-action retained.
```
def sourceBimoduleTotalComparison :
    BimoduleComplexTensor.total k B (B ⊗[k] ChainAlgebra k l)
      (TensorResolution.integerBimoduleComplex k B l)
      (middleLeftComplex k (B ⊗[k] ChainAlgebra k l) B (BimoduleO P a l) Z)
      (TensorResolution.finiteDegrees l) (TensorResolution.finiteDegrees_strictMono l) ≅
    BimoduleComplexTensor.total k B B (P⟦b⟧) Z
      (TensorResolution.finiteDegrees l) (TensorResolution.finiteDegrees_strictMono l) :=
…
```
Mentions: OAI.LittleFinitistic.BimoduleComplexTensor.total, OAI.LittleFinitistic.OrdinarySimulation.ChainAlgebra, OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.integerBimoduleComplex, OAI.LittleFinitistic.middleLeftComplex, OAI.LittleFinitistic.OrdinarySimulation.BimoduleO, OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.finiteDegrees, OAI.LittleFinitistic.OrdinarySimulation.TensorResolution.finiteDegrees_strictMono