OAI/Analysis/Commutator/RelativeMatrix.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Kadison.RelativeMatrix.concrete line 26
2. def OAI.Kadison.RelativeMatrix.relativeStar line 28
3. lemma OAI.Kadison.RelativeMatrix.mem_relativeStar line 31
4. def OAI.Kadison.RelativeMatrix.relative line 42
5. lemma OAI.Kadison.RelativeMatrix.mem_relative line 61
6. lemma OAI.Kadison.RelativeMatrix.le_original line 65
7. lemma OAI.Kadison.RelativeMatrix.diagonal_mem line 67
8. lemma OAI.Kadison.RelativeMatrix.isFactor line 73
9. lemma OAI.Kadison.RelativeMatrix.noMinimal line 86