OAI/Analysis/Quantum/DimensionTen/ExteriorEvaluation.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DimensionTen.tensorMap_kronecker line 13
2. lemma OAI.DimensionTen.exteriorMap_veronese line 29
3. lemma OAI.DimensionTen.firstSix_isometry line 35
4. lemma OAI.DimensionTen.firstSix_compression line 41
5. lemma OAI.DimensionTen.phiTwo_phiOne line 48
6. lemma OAI.DimensionTen.compositeChoi_posSemidef line 53
7. lemma OAI.DimensionTen.compositeChoi_pairing line 56
8. lemma OAI.DimensionTen.blocksZ_zero_gram line 73
9. lemma OAI.DimensionTen.blocks_zero_gram line 75
10. lemma OAI.DimensionTen.pencil_ezero line 85
11. lemma OAI.DimensionTen.pencilMap_ezero_fast line 87