OAI/Analysis/Quantum/DimensionTen/Veronese.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DimensionTen.sqrtTwo_sq line 11
2. lemma OAI.DimensionTen.sqrtTwo_ne line 14
3. def OAI.DimensionTen.veronese line 17
4. lemma OAI.DimensionTen.symmetric_veronese line 22
5. lemma OAI.DimensionTen.veronese_adjoint line 30
6. lemma OAI.DimensionTen.symmetric_pure_veronese line 39
7. def OAI.DimensionTen.symmetricIndex line 44
8. lemma OAI.DimensionTen.symmetricIndex_bijective line 47
9. def OAI.DimensionTen.symmetricEquiv line 49
10. def OAI.DimensionTen.veroneseCoeffs line 52
11. lemma OAI.DimensionTen.veronese_dot line 56
12. lemma OAI.DimensionTen.veroneseCoeffs_ne line 68