OAI/Analysis/FreeGroupFactor/NormalExtension.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.FreeGroupFactorMain.deltaOne line 16
  2. theorem OAI.FreeGroupFactorMain.deltaOne_eq line 20
  3. theorem OAI.FreeGroupFactorMain.groupVN_matrix line 25
  4. theorem OAI.FreeGroupFactorMain.groupVN_star_coefficient line 38
  5. theorem OAI.FreeGroupFactorMain.canonicalTrace_star_mul_inner line 52
  6. theorem OAI.FreeGroupFactorMain.canonicalTrace_mul line 61
  7. def OAI.FreeGroupFactorMain.hilbertSequenceMap line 78
  8. theorem OAI.FreeGroupFactorMain.spatial_ultraweak_continuous line 83
  9. def OAI.FreeGroupFactorMain.spatialGroupIso line 109
  10. theorem OAI.FreeGroupFactorMain.spatialGroupIso_normal line 123
  11. theorem OAI.FreeGroupFactorMain.normalTracialIso_of_spatial line 138
  12. theorem OAI.FreeGroupFactorMain.operator_matrix_ext line 153
  13. theorem OAI.FreeGroupFactorMain.operator_coeff_tsum line 169
  14. theorem OAI.FreeGroupFactorMain.matrix_of_commute_right line 189
  15. theorem OAI.FreeGroupFactorMain.matrix_of_commute_left line 201
  16. theorem OAI.FreeGroupFactorMain.mem_groupVN_iff_commute_right line 213
  17. theorem OAI.FreeGroupFactorMain.rightRegular_single line 258
  18. theorem OAI.FreeGroupFactorMain.mem_groupVN_of_matrix_invariant line 265
  19. theorem OAI.FreeGroupFactorMain.haar_orbit_orthonormal line 279
  20. theorem OAI.FreeGroupFactorMain.spatial_of_haar_total line 290
  21. theorem OAI.FreeGroupFactorMain.normalTracialIso_of_haar_total line 381
  22. theorem OAI.FreeGroupFactorMain.iso_extension_of_haar_total line 391