OAI/Analysis/KadisonKastler/FreeDiagonalWords.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Reduced centered words in the finite diagonal family

  1. def OAI.KadisonKastler.diagonalWord line 18
  2. def OAI.KadisonKastler.ReducedDiagonalWord line 21
  3. theorem OAI.KadisonKastler.ReducedDiagonalWord.reverse line 24
  4. theorem OAI.KadisonKastler.ReducedDiagonalWord.join_reverse line 28
  5. theorem OAI.KadisonKastler.diagonalWord_nil line 35
  6. theorem OAI.KadisonKastler.diagonalWord_cons line 37
  7. theorem OAI.KadisonKastler.diagonalWord_append line 40
  8. theorem OAI.KadisonKastler.star_diagonalWord line 44
  9. theorem OAI.KadisonKastler.trace_reducedDiagonalWord line 55
  10. theorem OAI.KadisonKastler.trace_diagonalWord_cross line 76