OAI/Analysis/Commutator/MatrixTowerIrreducible.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Kadison.MatrixTower.exists_selfAdjoint_dense_sequence line 22
2. lemma OAI.Kadison.MatrixTower.centered_approximation line 40
3. lemma OAI.Kadison.MatrixTower.scalar_of_selfAdjoint_commutes line 67
4. theorem OAI.Kadison.MatrixTower.scalar_of_commutes line 85