OAI/Analysis/KadisonSimilarity/FreeProduct/DihedralHaarFunctionalCalculus.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The Haar law determines the continuous functional calculus of the real part of the rotation, tested against every rotation power.

  1. theorem OAI.KadisonSimilarity.trace_cfc_realPart_rotation line 14