OAI/Analysis/FreeWords/FreeCompressionMoments.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.KKFreeWords.free_centered_two line 47
  2. theorem OAI.KKFreeWords.free_centered_four line 56
  3. theorem OAI.KKFreeWords.free_centered_six line 67
  4. theorem OAI.KKFreeWords.free_centered_eight line 79
  5. theorem OAI.KKFreeWords.free_trace_pair line 93
  6. theorem OAI.KKFreeWords.free_trace_four line 104
  7. theorem OAI.KKFreeWords.free_trace_six_partial line 122
  8. theorem OAI.KKFreeWords.free_compression_four line 138
  9. theorem OAI.KKFreeWords.trace_star line 223
  10. theorem OAI.KKFreeWords.projection_compression_second line 228
  11. theorem OAI.KKFreeWords.projection_compression_fourth line 243