OAI/Analysis/KadisonSimilarity/FreeProduct/NormalSpectralArc.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The abstract spectral-arc input follows once its generated algebra has the actual faithful normal range. The ambient algebra need not be presented in those coordinates.

  1. theorem OAI.KadisonSimilarity.dihedralSpectralArcInput_of_normal_range line 15