OAI/Analysis/KadisonSimilarity/Tracial/IntegerMomentMaps.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Naturality and coefficient reindexing for finite integer-power words.

  1. theorem OAI.KadisonSimilarity.integerEval_hom line 11
  2. theorem OAI.KadisonSimilarity.integerEval_reindex line 21
  3. theorem OAI.KadisonSimilarity.admissibleIntTail_reindex line 34