OAI/Topology/CoarseAssembly/OrthogonalBlock.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The operator algebra of an orthogonal direct sum

  1. def OAI.CoarseAssembly.Analytic.OddCycle.IsDirectSum.block line 13
  2. theorem OAI.CoarseAssembly.Analytic.OddCycle.IsDirectSum.cross_left line 16
  3. theorem OAI.CoarseAssembly.Analytic.OddCycle.IsDirectSum.cross_right line 26
  4. theorem OAI.CoarseAssembly.Analytic.OddCycle.IsDirectSum.block_mul line 36
  5. theorem OAI.CoarseAssembly.Analytic.OddCycle.IsDirectSum.block_add line 43
  6. theorem OAI.CoarseAssembly.Analytic.OddCycle.IsDirectSum.block_smul line 54
  7. theorem OAI.CoarseAssembly.Analytic.OddCycle.IsDirectSum.block_one line 61
  8. def OAI.CoarseAssembly.Analytic.OddCycle.IsDirectSum.blockHom line 66