OAI/Analysis/Pureness/Stabilization/MatrixPositive.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.CuntzTrace.(instance at line 11) line 11
2. instance OAI.CuntzTrace.(instance at line 12) line 12
3. theorem OAI.CuntzTrace.matrixLimit_positive_approximation line 14
4. theorem OAI.CuntzTrace.matrixLimit_cut_below_finite line 29