OAI/Analysis/Commutator/InfiniteDiagonalRange.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.InfiniteAmplification.block line 22
2. lemma OAI.Kadison.InfiniteAmplification.block_map_commute line 26
3. def OAI.Kadison.InfiniteAmplification.zeroth line 32
4. lemma OAI.Kadison.InfiniteAmplification.eq_map_of_blocks line 37
5. lemma OAI.Kadison.InfiniteAmplification.diagonal_bicommutant_range line 45
6. def OAI.Kadison.InfiniteAmplification.algebra line 71