OAI/Analysis/Commutator/GeneratedFreePair.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Kadison.GeneratedFreePair.algebra line 27
  2. lemma OAI.Kadison.GeneratedFreePair.left_mem line 29
  3. lemma OAI.Kadison.GeneratedFreePair.right_mem line 32
  4. lemma OAI.Kadison.GeneratedFreePair.left_le line 35
  5. abbrev OAI.Kadison.GeneratedFreePair.leftHom line 38
  6. def OAI.Kadison.GeneratedFreePair.rightHom line 40
  7. def OAI.Kadison.GeneratedFreePair.ambient line 42
  8. def OAI.Kadison.GeneratedFreePair.factors line 45
  9. lemma OAI.Kadison.GeneratedFreePair.false_range line 48
  10. lemma OAI.Kadison.GeneratedFreePair.right_factor line 57
  11. lemma OAI.Kadison.GeneratedFreePair.original_generation line 61
  12. lemma OAI.Kadison.GeneratedFreePair.le_ambient line 76
  13. theorem OAI.Kadison.GeneratedFreePair.free_in_generated line 91
  14. lemma OAI.Kadison.GeneratedFreePair.in_bicommutant line 99
  15. lemma OAI.Kadison.GeneratedFreePair.in_range_bicommutant line 108