OAI/Analysis/Commutator/MatrixIndexEquiv.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.MatrixTower.matrixIndexEquiv line 16
2. def OAI.Kadison.MatrixTower.normalizedSize line 28
3. lemma OAI.Kadison.MatrixTower.normalizedSize_succ line 30
4. def OAI.Kadison.MatrixTower.normalizedIndex line 35
5. def OAI.Kadison.MatrixTower.normalizedStage line 38
6. lemma OAI.Kadison.MatrixTower.normalizedStage_range line 41
7. def OAI.Kadison.MatrixTower.normalizedInclusion line 54
8. lemma OAI.Kadison.MatrixTower.normalizedInclusion_commutes line 60