OAI/Analysis/Commutator/CyclePairTrace3.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.SchurWeyl.IsEndpointPairing line 22
2. lemma OAI.Kadison.SchurWeyl.some_removeNone_of_fixed line 25
3. def OAI.Kadison.SchurWeyl.pairingOfEndpointPerm line 34
4. def OAI.Kadison.SchurWeyl.endpointPairingEquiv line 46
5. theorem OAI.Kadison.SchurWeyl.centered_expansion_contractions line 75