OAI/Analysis/JiangSu/CStarAlgebras/ConcreteIterateDiagonalization.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JiangSuConstruction.stepUnitary line 19
2. lemma OAI.JiangSuConstruction.stageStep_eval line 26
3. theorem OAI.JiangSuConstruction.concrete_iterate_diagonalization line 31
4. lemma OAI.JiangSuConstruction.block_reindex_both line 93
5. theorem OAI.JiangSuConstruction.actual_index_normalized_matching line 106
6. lemma OAI.JiangSuConstruction.unitary_conjugating_matching line 156
7. theorem OAI.JiangSuConstruction.concrete_stage_matching line 166