OAI/Analysis/Quantum/PPTSquare/PairResult.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExplicitPencil.gram_identity line 13
2. lemma OAI.ExplicitPencil.rank_identity line 23
3. lemma OAI.ExplicitPencil.positive_test_matrix line 26
4. lemma OAI.ExplicitPencil.e0_projector line 32
5. lemma OAI.ExplicitPencil.positive_test line 36
6. theorem OAI.ExplicitPencil.twenty_directions line 42
7. theorem OAI.ExplicitPencil.main_pair line 54
8. def OAI.ExplicitPencil.Theta line 62
9. theorem OAI.ExplicitPencil.main_channel line 64