OAI/Topology/CoarseAssembly/FiniteCycle.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Finite-dimensional odd cycles vanish

Every change of operator is compact on a finite-dimensional Hilbert space. Changing the operator to the identity gives a degenerate odd cycle.

  1. theorem OAI.CoarseAssembly.Analytic.finiteDimensional_cycleClass_zero line 18