OAI/Topology/CoarseAssembly/ToeplitzProductIndex.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Multiplicativity of Toeplitz compression modulo compact operators

  1. theorem OAI.CoarseAssembly.Analytic.compact_commutator_mul line 13
  2. theorem OAI.CoarseAssembly.Analytic.compact_commutator_star_unitary line 22
  3. theorem OAI.CoarseAssembly.Analytic.toeplitzCompression_product_difference line 33
  4. theorem OAI.CoarseAssembly.Analytic.toeplitzCompression_product_compact line 41
  5. theorem OAI.CoarseAssembly.Analytic.toeplitzCompression_index_mul line 48