OAI/Analysis/KadisonKastler/CoreTraceVectorTracial.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The vector trace determined by conjugation symmetry

Two operators satisfying the same Tomita vector identity have cyclic vector coefficients. This supplies the trace identity on the frequency corner without a polarization argument or an assumed trace.

  1. theorem OAI.KadisonKastler.coreTraceSymmetry_tracial line 18