OAI/Analysis/InterpolatedFactors/DoubleTrace.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.FreeGroupFactorMain.Amplification.flattenHilbert_single line 19
  2. theorem OAI.FreeGroupFactorMain.Amplification.flatten_projectionTrace line 27
  3. def OAI.FreeGroupFactorMain.Amplification.doubleFiniteDiagonal line 52
  4. def OAI.FreeGroupFactorMain.Amplification.finiteFlatten line 87
  5. theorem OAI.FreeGroupFactorMain.Amplification.doubleFiniteDiagonal_projection line 90
  6. theorem OAI.FreeGroupFactorMain.Amplification.finiteFlatten_projection line 104
  7. theorem OAI.FreeGroupFactorMain.Amplification.finiteFlatten_trace line 109
  8. def OAI.FreeGroupFactorMain.Amplification.finiteCornerSingletonIso line 135
  9. theorem OAI.FreeGroupFactorMain.Amplification.finiteCornerSingletonIso_normal line 154
  10. theorem OAI.FreeGroupFactorMain.Amplification.finiteCornerSingletonIso_trace line 160
  11. theorem OAI.FreeGroupFactorMain.Amplification.finiteCornerIso_symm line 171
  12. theorem OAI.FreeGroupFactorMain.Amplification.finiteCornerSingletonIso_symm_normal line 177
  13. theorem OAI.FreeGroupFactorMain.Amplification.finite_corner_choice_both line 184