OAI/Analysis/Pureness/Comparison/TraceFunctionalCalculus.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CuntzComparison.alternating_pow line 11
2. lemma OAI.CuntzComparison.TracialState.linking_power_trace line 21
3. lemma OAI.CuntzComparison.TracialState.linking_polynomial_trace line 32
4. theorem OAI.CuntzComparison.TracialState.linking_cfc_trace line 45