OAI/Analysis/Commutator/MatrixTowerClosure.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Kadison.MatrixTower.concreteStage line 20
2. def OAI.Kadison.MatrixTower.stageAlgebra line 23
3. def OAI.Kadison.MatrixTower.generated line 25
4. lemma OAI.Kadison.MatrixTower.mem_generated line 41
5. lemma OAI.Kadison.MatrixTower.stageAlgebra_le line 48
6. lemma OAI.Kadison.MatrixTower.generated_le line 54
7. lemma OAI.Kadison.MatrixTower.stage_mem line 63
8. def OAI.Kadison.MatrixTower.stageHom line 68
9. lemma OAI.Kadison.MatrixTower.generated_irreducible line 74
10. lemma OAI.Kadison.MatrixTower.generated_factor line 81