OAI/Analysis/Commutator/CyclePairTrace2.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.SchurWeyl.endpointPairingPerm line 21
2. lemma OAI.Kadison.SchurWeyl.endpointPairingPerm_none line 24
3. lemma OAI.Kadison.SchurWeyl.endpointPairingPerm_some line 27
4. def OAI.Kadison.SchurWeyl.optionPairRepresentative line 30
5. lemma OAI.Kadison.SchurWeyl.optionPairRepresentative_apply line 35
6. def OAI.Kadison.SchurWeyl.endpointPairingCycleEquiv line 42
7. lemma OAI.Kadison.SchurWeyl.cycleCount_endpointPairing line 70
8. theorem OAI.Kadison.SchurWeyl.rawCycleTrace_option line 75
9. theorem OAI.Kadison.SchurWeyl.cycleTrace_endpointPairing line 91