OAI/Topology/CoarseAssembly/UnitalCycleNormalization.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Self-adjoint normalization of a unital Fredholm cycle

The compact adjoint defect allows replacement of the operator by its self-adjoint part, with the represented algebra and K-homology class fixed.

  1. theorem OAI.CoarseAssembly.Analytic.exists_selfAdjoint_representative line 18