OAI/Topology/CoarseAssembly/DegenerateCutDown.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Degenerate cycles have zero explicit Toeplitz index

  1. theorem OAI.CoarseAssembly.Analytic.representedCorrection_annihilates line 13
  2. theorem OAI.CoarseAssembly.Analytic.cutDown_degenerate line 49
  3. theorem OAI.CoarseAssembly.Analytic.cutDown_degenerate_sq line 74
  4. theorem OAI.CoarseAssembly.Analytic.rawCycleToeplitz_eq_cutDown line 90
  5. theorem OAI.CoarseAssembly.Analytic.rawCycleIndex_degenerate line 100