OAI/Topology/CoarseAssembly/AlgebraicRoe.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The algebra of locally compact finite-propagation operators

  1. theorem OAI.CoarseAssembly.DiscreteRoe.PropagationLE.add line 19
  2. theorem OAI.CoarseAssembly.DiscreteRoe.PropagationLE.smul line 27
  3. theorem OAI.CoarseAssembly.DiscreteRoe.Generator.zero line 32
  4. theorem OAI.CoarseAssembly.DiscreteRoe.Generator.add line 42
  5. theorem OAI.CoarseAssembly.DiscreteRoe.Generator.smul line 55
  6. theorem OAI.CoarseAssembly.DiscreteRoe.Generator.star line 66
  7. theorem OAI.CoarseAssembly.DiscreteRoe.Generator.mul line 70
  8. theorem OAI.CoarseAssembly.DiscreteRoe.roe_eq_closure_algebraic line 79