OAI/Topology/CoarseAssembly/FredholmInvertible.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Invertibility after the finite-rank kernel correction

  1. theorem OAI.CoarseAssembly.Analytic.isUnit_of_injective_compact_square line 13
  2. theorem OAI.CoarseAssembly.Analytic.kernel_corrected_isUnit line 34