OAI/Analysis/Quantum/PPTSquare/Evaluation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PencilEvaluation.action line 14
2. def OAI.PencilEvaluation.evaluation line 17
3. lemma OAI.PencilEvaluation.denominator_ne line 20
4. lemma OAI.PencilEvaluation.action_commute line 24
5. lemma OAI.PencilEvaluation.low_vecMul line 35
6. lemma OAI.PencilEvaluation.high_vecMul line 44
7. lemma OAI.PencilEvaluation.eigen_low_recursion line 52
8. lemma OAI.PencilEvaluation.exists_evaluations line 65