OAI/Analysis/BoundedHochschild/FreeCoefficients.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Centered free coefficients and vanishing graded moments.

  1. abbrev OAI.HochschildFreeMoments.Letter line 27
  2. def OAI.HochschildFreeMoments.tag line 29
  3. def OAI.HochschildFreeMoments.value line 33
  4. def OAI.HochschildFreeMoments.degreeLetter line 37
  5. def OAI.HochschildFreeMoments.evaluate line 41
  6. def OAI.HochschildFreeMoments.degree line 43
  7. lemma OAI.HochschildFreeMoments.evaluate_nil line 45
  8. lemma OAI.HochschildFreeMoments.evaluate_cons line 46
  9. lemma OAI.HochschildFreeMoments.evaluate_append line 48
  10. lemma OAI.HochschildFreeMoments.degree_nil line 50
  11. lemma OAI.HochschildFreeMoments.degree_cons line 51
  12. lemma OAI.HochschildFreeMoments.degree_append line 53
  13. def OAI.HochschildFreeMoments.FreeCoefficients line 58
  14. def OAI.HochschildFreeMoments.center line 63
  15. lemma OAI.HochschildFreeMoments.tag_center line 68
  16. lemma OAI.HochschildFreeMoments.degreeLetter_center line 70
  17. lemma OAI.HochschildFreeMoments.degree_center line 72
  18. lemma OAI.HochschildFreeMoments.center_replacement line 75
  19. lemma OAI.HochschildFreeMoments.center_moment line 85
  20. theorem OAI.HochschildFreeMoments.moment_eq_zero_of_degree_ne_one line 114