OAI/Analysis/KadisonKastler/CoreTraceTranslationVector.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Trace-vector symmetry for the translation generators

  1. theorem OAI.KadisonKastler.regularCoreAction_traceVector line 22
  2. theorem OAI.KadisonKastler.coreTraceTranslation_vector_symmetry line 39