OAI/Analysis/Commutator/FreeRepeatedWords.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Kadison.FreeBlocks.repeatedParams line 27
  2. lemma OAI.Kadison.FreeBlocks.repeatedParams_D line 32
  3. def OAI.Kadison.FreeBlocks.repeatPre line 43
  4. lemma OAI.Kadison.FreeBlocks.repeatedParams_J line 49
  5. lemma OAI.Kadison.FreeBlocks.norm_repeatPre line 59
  6. def OAI.Kadison.FreeBlocks.repeatPreIsometry line 68
  7. def OAI.Kadison.FreeBlocks.repeatInsertion line 73
  8. lemma OAI.Kadison.FreeBlocks.repeatInsertion_coe line 77
  9. lemma OAI.Kadison.FreeBlocks.blockRead_repeated line 83
  10. def OAI.Kadison.FreeBlocks.tensorOutput line 99
  11. lemma OAI.Kadison.FreeBlocks.norm_tensorOutput line 107
  12. def OAI.Kadison.FreeBlocks.repeatedOutput line 117
  13. lemma OAI.Kadison.FreeBlocks.repeatedOutput_bounded line 126
  14. lemma OAI.Kadison.FreeBlocks.norm_repeatedOutput_one line 152
  15. lemma OAI.Kadison.FreeBlocks.repeatedOutput_inserted line 178
  16. lemma OAI.Kadison.FreeBlocks.repeatedOutput_zero line 188
  17. lemma OAI.Kadison.FreeBlocks.norm_repeatedOutput line 199
  18. lemma OAI.Kadison.FreeBlocks.norm_base_mul line 222
  19. lemma OAI.Kadison.FreeBlocks.base_intertwining line 239
  20. lemma OAI.Kadison.FreeBlocks.repeated_error_norm line 246
  21. lemma OAI.Kadison.FreeBlocks.repeated_norm line 262