OAI/Analysis/Commutator/CycleInvariants.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Kadison.SchurWeyl.rawCycleTrace line 20
  2. lemma OAI.Kadison.SchurWeyl.rawCycleTrace_eq_sum line 23
  3. def OAI.Kadison.SchurWeyl.cycleSet line 37
  4. instance OAI.Kadison.SchurWeyl.(instance at line 39) line 39
  5. def OAI.Kadison.SchurWeyl.cycleCount line 43
  6. lemma OAI.Kadison.SchurWeyl.constant_on_cycle line 46
  7. def OAI.Kadison.SchurWeyl.fixedLabelEquiv line 54
  8. lemma OAI.Kadison.SchurWeyl.fixedLabel_card line 62
  9. lemma OAI.Kadison.SchurWeyl.rawCycleTrace_single line 68
  10. def OAI.Kadison.SchurWeyl.inflateMatrix line 91
  11. lemma OAI.Kadison.SchurWeyl.prod_inflateMatrix line 96
  12. lemma OAI.Kadison.SchurWeyl.fixedLabel_indicator_sum line 108
  13. lemma OAI.Kadison.SchurWeyl.rawCycleTrace_inflate line 119
  14. def OAI.Kadison.SchurWeyl.cycleTrace line 147
  15. lemma OAI.Kadison.SchurWeyl.cycleTrace_inflate line 150
  16. lemma OAI.Kadison.SchurWeyl.cycleTrace_single line 166
  17. lemma OAI.Kadison.SchurWeyl.cycleTrace_coefficients_unique line 175
  18. lemma OAI.Kadison.SchurWeyl.stable_cycle_coefficients line 187
  19. theorem OAI.Kadison.SchurWeyl.invariant_multilinear_form_normalized line 196