OAI/InformationTheory/Entanglement/CombinatorialAssembly.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteConstruction.P line 12
2. lemma OAI.FiniteConstruction.P_hermitian line 14
3. lemma OAI.FiniteConstruction.P_real line 16
4. lemma OAI.FiniteConstruction.P_idempotent line 19
5. lemma OAI.FiniteConstruction.P_orthogonal line 21
6. lemma OAI.FiniteConstruction.P_complete line 28
7. lemma OAI.FiniteConstruction.P_commute line 36
8. lemma OAI.FiniteConstruction.P_overlap_product line 39
9. lemma OAI.FiniteConstruction.P_clique line 43
10. def OAI.FiniteConstruction.data line 79