OAI/Topology/CoarseAssembly/MultiplierBoundaryHomotopy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Norm homotopy invariance of the Roe multiplier boundary class

  1. theorem OAI.CoarseAssembly.DiscreteRoe.multiplierBoundaryClass_homotopy line 24
  2. theorem OAI.CoarseAssembly.DiscreteRoe.multiplierBoundaryClass_eq_zero line 39