OAI/InformationTheory/Entanglement/CombinatorialLocal.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteConstruction.trivial line 12
2. def OAI.FiniteConstruction.localProjection line 13
3. lemma OAI.FiniteConstruction.localProjection_six line 17
4. lemma OAI.FiniteConstruction.localProjection_hermitian line 20
5. lemma OAI.FiniteConstruction.localProjection_real line 26
6. lemma OAI.FiniteConstruction.localProjection_idempotent line 32
7. lemma OAI.FiniteConstruction.localProjection_orthogonal line 38
8. lemma OAI.FiniteConstruction.localProjection_complete line 44
9. lemma OAI.FiniteConstruction.localProjection_commute_same line 50
10. lemma OAI.FiniteConstruction.both_contexts_orthogonal line 56
11. lemma OAI.FiniteConstruction.localProjection_commute line 62