OAI/Analysis/Commutator/PartialUnitaryWords.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Kadison.FinitePatching.Words.Slot line 21
  2. abbrev OAI.Kadison.FinitePatching.Words.Letter line 23
  3. def OAI.Kadison.FinitePatching.Words.NonzeroSlot line 25
  4. def OAI.Kadison.FinitePatching.Words.Valid line 27
  5. lemma OAI.Kadison.FinitePatching.Words.valid_of_internal line 30
  6. lemma OAI.Kadison.FinitePatching.Words.internal_prefix line 52
  7. lemma OAI.Kadison.FinitePatching.Words.internal_middle line 60
  8. lemma OAI.Kadison.FinitePatching.Words.tail_nil_of_not_nonzero line 67
  9. def OAI.Kadison.FinitePatching.Words.slotPower line 74
  10. def OAI.Kadison.FinitePatching.Words.slotIncrement line 79
  11. def OAI.Kadison.FinitePatching.Words.letter line 84
  12. def OAI.Kadison.FinitePatching.Words.newLetter line 86
  13. def OAI.Kadison.FinitePatching.Words.word line 88
  14. lemma OAI.Kadison.FinitePatching.Words.word_nil line 90
  15. lemma OAI.Kadison.FinitePatching.Words.word_cons line 92
  16. lemma OAI.Kadison.FinitePatching.Words.word_append line 95
  17. lemma OAI.Kadison.FinitePatching.Words.word_open_last line 98
  18. lemma OAI.Kadison.FinitePatching.Words.word_support_last line 102
  19. lemma OAI.Kadison.FinitePatching.Words.slotPower_norm line 106
  20. lemma OAI.Kadison.FinitePatching.Words.letter_norm line 114
  21. lemma OAI.Kadison.FinitePatching.Words.word_norm line 119
  22. lemma OAI.Kadison.FinitePatching.Words.slotPower_add line 128
  23. lemma OAI.Kadison.FinitePatching.Words.letter_add line 137
  24. lemma OAI.Kadison.FinitePatching.Words.word_add line 141