OAI/Analysis/Commutator/NormalTraceProjection.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Kadison.NormalGNS.projection_subtype line 25
2. lemma OAI.Kadison.NormalGNS.gns_projection_iff line 32
3. lemma OAI.Kadison.NormalGNS.gns_projection_le_iff line 44
4. theorem OAI.Kadison.NormalGNS.gns_noMinimal line 59
5. theorem OAI.Kadison.NormalGNS.exists_prescribed_projection_trace line 84
6. lemma OAI.Kadison.NormalGNS.projection_zero_of_trace_re_zero line 102
7. theorem OAI.Kadison.NormalGNS.exists_projection_partition line 110