OAI/Analysis/Commutator/CyclicDecomposition.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.CyclicDecomposition.full line 27
2. abbrev OAI.Kadison.CyclicDecomposition.ProjLink line 33
3. def OAI.Kadison.CyclicDecomposition.cyclicLink line 35
4. def OAI.Kadison.CyclicDecomposition.Good line 50
5. lemma OAI.Kadison.CyclicDecomposition.exists_maximal_good line 53
6. lemma OAI.Kadison.CyclicDecomposition.good_projection line 68
7. lemma OAI.Kadison.CyclicDecomposition.good_commutes line 73
8. lemma OAI.Kadison.CyclicDecomposition.family_invariant line 78
9. theorem OAI.Kadison.CyclicDecomposition.maximal_spans line 93
10. structure OAI.Kadison.CyclicDecomposition.Decomposition line 152
11. theorem OAI.Kadison.CyclicDecomposition.exists_decomposition line 161