OAI/Analysis/Pureness/Stabilization/CuntzDenseMaps.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CuntzTrace.starHom_continuous line 11

   Distinct definitions of this name: OAI/Analysis/Pureness/Stabilization/MatrixBlockNorm.lean:16 (different declaration text). Qualify references as OAI.CuntzTrace.starHom_continuous@path.

2. theorem OAI.CuntzTrace.Positive.map_cut line 20
3. theorem OAI.CuntzTrace.cuntzClass_maps_eq_of_dense line 27