OAI/Analysis/Commutator/TracialDoubleCompression.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.TracialSequence.constantSequence line 28
2. lemma OAI.Kadison.TracialSequence.constantSequence_apply line 37
3. lemma OAI.Kadison.TracialSequence.trace_constant line 40
4. def OAI.Kadison.TracialSequence.constantHom line 45
5. lemma OAI.Kadison.TracialSequence.constantHom_coe line 51
6. lemma OAI.Kadison.TracialSequence.constant_trace line 58
7. abbrev OAI.Kadison.TracialSequence.doubleCompressionPreGNS line 65
8. lemma OAI.Kadison.TracialSequence.double_embedding line 69
9. lemma OAI.Kadison.TracialSequence.double_compression_preserves line 106