OAI/Analysis/Commutator/GeneratedMatrixBicommutant.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Kadison.GeneratedMatrixBicommutant.stages line 28
  2. def OAI.Kadison.GeneratedMatrixBicommutant.algebra line 30
  3. lemma OAI.Kadison.GeneratedMatrixBicommutant.stage_mem line 32
  4. def OAI.Kadison.GeneratedMatrixBicommutant.stageHom line 36
  5. lemma OAI.Kadison.GeneratedMatrixBicommutant.representedStages_eq line 39
  6. lemma OAI.Kadison.GeneratedMatrixBicommutant.in_represented line 45
  7. lemma OAI.Kadison.GeneratedMatrixBicommutant.le_vonNeumann line 52
  8. lemma OAI.Kadison.GeneratedMatrixBicommutant.in_range line 65
  9. lemma OAI.Kadison.GeneratedMatrixBicommutant.factor line 76