OAI/Analysis/Commutator/TracialSequenceTrace.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.VectorFunctional.functional line 22
2. lemma OAI.Kadison.VectorFunctional.functional_apply line 34
3. lemma OAI.Kadison.VectorFunctional.functional_star_mul line 37
4. lemma OAI.Kadison.VectorFunctional.continuous_functional_wot line 43
5. def OAI.Kadison.TracialSequence.sequenceTrace line 57
6. lemma OAI.Kadison.TracialSequence.tendsto_trace line 60
7. lemma OAI.Kadison.TracialSequence.trace_one line 70
8. lemma OAI.Kadison.TracialSequence.trace_mul line 78
9. lemma OAI.Kadison.TracialSequence.trace_faithful line 84