OAI/Topology/CoarseAssembly/OperatorNormalization.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A self-adjoint Fredholm operator is a compact perturbation of an involution

  1. theorem OAI.CoarseAssembly.Analytic.exists_compact_involution line 13
  2. theorem OAI.CoarseAssembly.Analytic.compact_commutator_of_compact_change line 37