OAI/Combinatorics/Chromatic/Walls/QuantumTorusChartCompletion.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.QuantumTorus.HasRootDegree line 16
2. lemma OAI.ElementaryPositivity.QuantumTorus.rootDegree_zero line 19
3. lemma OAI.ElementaryPositivity.QuantumTorus.rootDegree_add line 24
4. def OAI.ElementaryPositivity.QuantumTorus.rootGrade line 34
5. lemma OAI.ElementaryPositivity.QuantumTorus.rootGrade_one line 40
6. lemma OAI.ElementaryPositivity.QuantumTorus.rootGrade_mul line 47
7. lemma OAI.ElementaryPositivity.QuantumTorus.rootGrade_filter line 68
8. def OAI.ElementaryPositivity.QuantumTorus.CompletedPositive line 73
9. def OAI.ElementaryPositivity.QuantumTorus.chartPositive line 79
10. def OAI.ElementaryPositivity.QuantumTorus.chartRemainder line 83
11. def OAI.ElementaryPositivity.QuantumTorus.chartZero line 87
12. def OAI.ElementaryPositivity.QuantumTorus.chartNegative line 92
13. lemma OAI.ElementaryPositivity.QuantumTorus.chart_three_factorization line 98
14. lemma OAI.ElementaryPositivity.QuantumTorus.chart_three_support line 103
15. lemma OAI.ElementaryPositivity.QuantumTorus.positiveProject_one line 126
16. lemma OAI.ElementaryPositivity.QuantumTorus.chart_three_unique line 136