OAI/Analysis/Commutator/NormalSubalgebra.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.NormalSubalgebra.inclusion line 22
2. lemma OAI.Kadison.NormalSubalgebra.inclusion_apply line 24
3. def OAI.Kadison.NormalSubalgebra.trace line 28
4. lemma OAI.Kadison.NormalSubalgebra.trace_apply line 32
5. lemma OAI.Kadison.NormalSubalgebra.normal line 34
6. lemma OAI.Kadison.NormalSubalgebra.tracial line 43
7. lemma OAI.Kadison.NormalSubalgebra.one line 47
8. lemma OAI.Kadison.NormalSubalgebra.faithful line 49
9. lemma OAI.Kadison.NormalSubalgebra.vector_norm line 55