OAI/Analysis/Pureness/GroupAlgebra/WordShellFactorization.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CuntzPureness.wordTreeDistance_eq_zero_iff line 9
  2. def OAI.CuntzPureness.wordLengthVector line 18
  3. lemma OAI.CuntzPureness.wordLengthVector_norm_le line 21
  4. lemma OAI.CuntzPureness.wordLengthVector_inner line 28
  5. abbrev OAI.CuntzPureness.WordShellIndex line 34
  6. def OAI.CuntzPureness.wordShellSign line 36
  7. def OAI.CuntzPureness.wordShellLeft line 41
  8. def OAI.CuntzPureness.wordShellRight line 46
  9. lemma OAI.CuntzPureness.wordShellSign_norm line 51
  10. lemma OAI.CuntzPureness.wordShellLeft_norm line 56
  11. lemma OAI.CuntzPureness.wordShellRight_norm line 64
  12. theorem OAI.CuntzPureness.wordShell_factorization line 72