OAI/Analysis/Commutator/NormalOriginalTower.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Kadison.MatrixTower.original_gns_generated line 24
2. lemma OAI.Kadison.MatrixTower.map_stage_range_le line 47
3. lemma OAI.Kadison.MatrixTower.copies_generated_of line 61
4. theorem OAI.Kadison.MatrixTower.original_copies_generated line 78