OAI/Analysis/KadisonKastler/ModularGaugeIdentity.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The Fourier gauge identity for the constructed modular group

  1. theorem OAI.KadisonKastler.modularGauge_fourier_tensor line 20
  2. theorem OAI.KadisonKastler.modularGauge_fourier line 42
  3. theorem OAI.KadisonKastler.modularGauge_identity line 68