OAI/Analysis/Pureness/Completion/CompletedRootRank.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CuntzPureness.completedRootRank line 10
2. lemma OAI.CuntzPureness.completedRootRank_normalized_tendsto line 13
3. lemma OAI.CuntzPureness.completedRootRank_zero line 18
4. lemma OAI.CuntzPureness.completedRootRank_smul line 21
5. theorem OAI.CuntzPureness.completed_root_trace_tendsto_rank line 25
6. theorem OAI.CuntzPureness.completedRootRank_include line 53