OAI/Analysis/Quantum/PPTSquare/Recurrence.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PencilAlgebra.lowMon line 10
2. def OAI.PencilAlgebra.highMon line 11
3. lemma OAI.PencilAlgebra.lowMon_zero line 12
4. lemma OAI.PencilAlgebra.low_step0 line 13
5. lemma OAI.PencilAlgebra.high_step0 line 15
6. lemma OAI.PencilAlgebra.low_step1 line 17
7. lemma OAI.PencilAlgebra.high_step1 line 19
8. lemma OAI.PencilAlgebra.low_step2 line 21
9. lemma OAI.PencilAlgebra.high_step2 line 23
10. lemma OAI.PencilAlgebra.low_step line 25
11. lemma OAI.PencilAlgebra.high_step line 30
12. lemma OAI.PencilAlgebra.low_recursion line 35
13. lemma OAI.PencilAlgebra.highNext_surjective line 156