OAI/Analysis/Commutator/MatrixTower.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.Kadison.MatrixTower.Stage line 20
2. lemma OAI.Kadison.MatrixTower.exists_stage_extension line 36
3. def OAI.Kadison.MatrixTower.scalarStage line 44
4. def OAI.Kadison.MatrixTower.next line 54
5. lemma OAI.Kadison.MatrixTower.next_spec line 58
6. def OAI.Kadison.MatrixTower.tower line 66
7. lemma OAI.Kadison.MatrixTower.tower_increasing line 71
8. lemma OAI.Kadison.MatrixTower.tower_size line 77
9. lemma OAI.Kadison.MatrixTower.tower_requirement line 88