OAI/Analysis/BoundedHochschild/AlternatingMoments.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

Integer powers, alternating words and graded free moments.

  1. abbrev OAI.HochschildPatching.IntAtom line 34
  2. def OAI.HochschildPatching.integerEval line 36
  3. def OAI.HochschildPatching.admissibleIntTail line 39
  4. def OAI.HochschildPatching.exponentCode line 42
  5. lemma OAI.HochschildPatching.signed_exponentCode line 43
  6. def OAI.HochschildPatching.toIntAtom line 51
  7. lemma OAI.HochschildPatching.integerEval_toIntAtom line 52
  8. lemma OAI.HochschildPatching.integer_moments_of_bounded line 58
  9. def OAI.HochschildPatching.alternatingTag line 96
  10. lemma OAI.HochschildPatching.intTail_cons line 97
  11. lemma OAI.HochschildPatching.alternating_right_repr line 106
  12. lemma OAI.HochschildPatching.alternating_moment_zero line 158
  13. abbrev OAI.HochschildGradedFree.Letter line 206
  14. def OAI.HochschildGradedFree.value line 208
  15. def OAI.HochschildGradedFree.degreeLetter line 209
  16. def OAI.HochschildGradedFree.tag line 210
  17. def OAI.HochschildGradedFree.evaluate line 211
  18. def OAI.HochschildGradedFree.degree line 212
  19. def OAI.HochschildGradedFree.centeredValue line 213
  20. def OAI.HochschildGradedFree.centeredEval line 214
  21. lemma OAI.HochschildGradedFree.evaluate_nil line 217
  22. lemma OAI.HochschildGradedFree.evaluate_cons line 218
  23. lemma OAI.HochschildGradedFree.evaluate_append line 220
  24. lemma OAI.HochschildGradedFree.degree_nil line 223
  25. lemma OAI.HochschildGradedFree.degree_cons line 224
  26. lemma OAI.HochschildGradedFree.degree_append line 226
  27. lemma OAI.HochschildGradedFree.centeredEval_nil line 228
  28. lemma OAI.HochschildGradedFree.centeredEval_cons line 229
  29. lemma OAI.HochschildGradedFree.degree_rotate_ne_one line 232
  30. lemma OAI.HochschildGradedFree.centered_rotate line 242
  31. lemma OAI.HochschildGradedFree.partial_center_zero line 252
  32. lemma OAI.HochschildGradedFree.partial_center_eq line 271
  33. theorem OAI.HochschildGradedFree.moment_eq_zero_of_degree_ne_one line 295