OAI/Analysis/JiangSu/CuntzSemigroup/CompletedOrthogonalRanks.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Pureness.positive_nnrpow_nat_succ line 19
2. lemma OAI.Pureness.positive_nnrpow_mem_hereditary line 30
3. lemma OAI.Pureness.orthogonal_add_pow_succ line 37
4. lemma OAI.Pureness.positive_reciprocal_power_add line 47
5. lemma OAI.Pureness.completed_reciprocal_power_add line 71
6. theorem OAI.Pureness.completedRootRank_add_orthogonal line 84
7. lemma OAI.TraceCone.nonunital_reciprocal_power_add line 103
8. lemma OAI.TraceCone.ExtendedTrace.rank_add_orthogonal line 117
9. lemma OAI.TraceCone.ExtendedTrace.rank_zero_positive line 129
10. lemma OAI.TraceCone.ExtendedTrace.rank_matrixBlockPositive line 138
11. def OAI.TraceCone.ExtendedTrace.stabilizedCuntzRank line 149
12. lemma OAI.TraceCone.ExtendedTrace.stabilizedCuntzRank_mk line 157
13. lemma OAI.TraceCone.ExtendedTrace.stabilizedCuntzRank_monotone line 160