OAI/Analysis/Commutator/FreeAction.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Kadison.FreeWordAction.letter line 30
  2. lemma OAI.Kadison.FreeWordAction.letter_color line 36
  3. lemma OAI.Kadison.FreeWordAction.letter_val line 39
  4. lemma OAI.Kadison.FreeWordAction.reduced_map line 42
  5. def OAI.Kadison.FreeWordAction.letterLinear line 45
  6. lemma OAI.Kadison.FreeWordAction.letterLinear_value line 51
  7. lemma OAI.Kadison.FreeWordAction.letterLinear_inner line 54
  8. def OAI.Kadison.FreeWordAction.letterIso line 58
  9. def OAI.Kadison.FreeWordAction.tensorIso line 64
  10. def OAI.Kadison.FreeWordAction.mapParams line 68
  11. lemma OAI.Kadison.FreeWordAction.tensorIso_pure line 72
  12. lemma OAI.Kadison.FreeWordAction.mapParams_letters line 81
  13. def OAI.Kadison.FreeWordAction.action line 94
  14. lemma OAI.Kadison.FreeWordAction.action_word line 99