OAI/Analysis/Pureness/GroupAlgebra/WordRadialFeature.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CuntzPureness.wordBranchFeature line 12
  2. def OAI.CuntzPureness.wordRadialFeature line 17
  3. lemma OAI.CuntzPureness.inner_wordBranchFeature_zero line 20
  4. lemma OAI.CuntzPureness.wordBranchFeature_inner_zero line 28
  5. lemma OAI.CuntzPureness.wordBranchFeature_cross_zero line 35
  6. lemma OAI.CuntzPureness.wordBranchFeature_root_inner line 45
  7. lemma OAI.CuntzPureness.wordBranchFeature_inner_root line 55
  8. lemma OAI.CuntzPureness.wordBranchFeature_inner_cons_same line 59
  9. lemma OAI.CuntzPureness.wordBranchFeature_inner_cons_ne line 76
  10. lemma OAI.CuntzPureness.wordRadialFeature_inner line 88
  11. theorem OAI.CuntzPureness.wordRadialFeature_inner_eq line 101