OAI/Analysis/KadisonSimilarity/FreeProduct/NormalFreeDihedral.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The generated free dihedral algebra inherits its normal realization from the ambient tracial geometry. Its spectral input is therefore a consequence of the two free centered symmetries.

  1. theorem OAI.KadisonSimilarity.TracialCornerGeometry.generated_dihedral_spectralInput line 20