OAI/Analysis/InterpolatedFactors/NormalEquiv.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FreeGroupFactorMain.Amplification.NormalTracialEquiv.symm line 18
  2. def OAI.FreeGroupFactorMain.Amplification.NormalTracialEquiv.trans line 24
  3. abbrev OAI.FreeGroupFactorMain.Amplification.GroupCornerNormalIso line 45
  4. def OAI.FreeGroupFactorMain.Amplification.unitNormalIso line 49
  5. def OAI.FreeGroupFactorMain.Amplification.finiteSingletonNormalIso line 61
  6. def OAI.FreeGroupFactorMain.Amplification.finiteUnitCornerIso line 73
  7. theorem OAI.FreeGroupFactorMain.Amplification.canonicalTrace_one line 78
  8. theorem OAI.FreeGroupFactorMain.Amplification.finiteUnitProjection_trace line 82
  9. theorem OAI.FreeGroupFactorMain.Amplification.preferred_unit_iso line 87
  10. theorem OAI.FreeGroupFactorMain.Amplification.scaling_ratio_trace line 103
  11. def OAI.FreeGroupFactorMain.Amplification.finiteScaledIso line 115