OAI/Analysis/BoundedHochschild/FreeHaarFamilies.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Free Haar extensions, graded families and finite free-group erasure.

  1. def OAI.HochschildUltrapower.powerFamily line 41
  2. lemma OAI.HochschildUltrapower.powerFamily_apply line 43
  3. theorem OAI.HochschildUltrapower.exists_free_haar_extension line 47
  4. def OAI.HochschildSplitWord.invLetter line 111
  5. def OAI.HochschildSplitWord.signedLetter line 112
  6. def OAI.HochschildSplitWord.sumProduct line 114
  7. def OAI.HochschildSplitWord.splitWord line 117
  8. lemma OAI.HochschildSplitWord.hom_mk line 120
  9. lemma OAI.HochschildSplitWord.sumProduct_splitWord line 130
  10. lemma OAI.HochschildSplitWord.sumProduct_splitWord_group line 144
  11. def OAI.HochschildUltrapower.gradedDegree line 163
  12. lemma OAI.HochschildUltrapower.gradedDegree_left line 165
  13. lemma OAI.HochschildUltrapower.gradedDegree_right line 167
  14. lemma OAI.HochschildUltrapower.gradedDegree_empty line 170
  15. def OAI.HochschildUltrapower.splitNew line 178
  16. lemma OAI.HochschildUltrapower.degree_splitNew line 182
  17. lemma OAI.HochschildUltrapower.powerFamily_star line 192
  18. def OAI.HochschildUltrapower.mixedFamily line 200
  19. def OAI.HochschildUltrapower.updateFamily line 203
  20. lemma OAI.HochschildUltrapower.mixedFamily_splitNew line 206
  21. lemma OAI.HochschildUltrapower.mixedFamily_splitNew_inv line 234
  22. theorem OAI.HochschildUltrapower.exists_finite_graded_family line 260