OAI/Analysis/InterpolatedFactors/StabilizationIso.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FreeGroupFactorMain.Amplification.stabilizationIso line 14
  2. theorem OAI.FreeGroupFactorMain.Amplification.stabilizationIso_normal line 30
  3. theorem OAI.FreeGroupFactorMain.Amplification.stabilizationDelta_eq_single line 39
  4. theorem OAI.FreeGroupFactorMain.Amplification.productSpatial_delta line 45
  5. theorem OAI.FreeGroupFactorMain.Amplification.stabilizationIso_projectionTrace line 53
  6. theorem OAI.FreeGroupFactorMain.Amplification.stabilizationIso_trace line 66
  7. theorem OAI.FreeGroupFactorMain.Amplification.amplification_functoriality line 79
  8. theorem OAI.FreeGroupFactorMain.Amplification.pairedIndex_apply line 94
  9. instance OAI.FreeGroupFactorMain.Amplification.doubleStabilization_isClosed line 97
  10. instance OAI.FreeGroupFactorMain.Amplification.doubleStabilization_CStarAlgebra line 101
  11. theorem OAI.FreeGroupFactorMain.Amplification.mem_doubleStabilization_iff_matrix line 103