OAI/Topology/CoarseAssembly/BinaryCycle.lean
3 declarations, 0 contain sorry, 0 declared as axioms
Actual direct sums of odd Fredholm modules
- def
OAI.CoarseAssembly.Analytic.OddCycle.binarySumline 16 - def
OAI.CoarseAssembly.Analytic.OddCycle.binarySum_decompositionline 46 - theorem
OAI.CoarseAssembly.Analytic.binarySum_classline 54