OAI/Analysis/Pureness/Stabilization/CuntzIdentities.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CuntzTrace.squareCutMultiplier line 8
2. lemma OAI.CuntzTrace.squareCutMultiplier_continuous line 11
3. lemma OAI.CuntzTrace.squareCutMultiplier_zero line 17
4. lemma OAI.CuntzTrace.squareCutMultiplier_identity line 20
5. theorem OAI.CuntzTrace.starMul_cut_factorization line 34
6. theorem OAI.CuntzTrace.starMul_cuntzBelow_mulStar line 56
7. theorem OAI.CuntzTrace.mulStar_cuntzBelow_starMul line 63
8. theorem OAI.CuntzTrace.starMul_cuntzBelow_iff line 68