OAI/Analysis/Pureness/Completion/CompletedOrthogonalRanks.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.CuntzPureness.positive_nnrpow_nat_succline 13 - lemma
OAI.CuntzPureness.positive_nnrpow_mem_hereditaryline 23 - lemma
OAI.CuntzPureness.orthogonal_add_pow_succline 30 - lemma
OAI.CuntzPureness.positive_reciprocal_power_addline 40 - lemma
OAI.CuntzPureness.completed_reciprocal_power_addline 64 - theorem
OAI.CuntzPureness.completedRootRank_add_orthogonalline 77