OAI/Combinatorics/Chromatic/Walls/TranslatedCompletion.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.QuantumTorus.shiftRootGrade line 16
2. def OAI.ElementaryPositivity.QuantumTorus.ShiftGraded line 21
3. lemma OAI.ElementaryPositivity.QuantumTorus.shiftRootGrade_finite line 23
4. lemma OAI.ElementaryPositivity.QuantumTorus.shiftRootGrade_mul line 27
5. lemma OAI.ElementaryPositivity.QuantumTorus.ShiftGraded.mul line 45
6. lemma OAI.ElementaryPositivity.QuantumTorus.shiftGraded_zero_iff line 54
7. lemma OAI.ElementaryPositivity.QuantumTorus.ShiftGraded.adjoint line 57
8. lemma OAI.ElementaryPositivity.QuantumTorus.ShiftGraded.sub line 64
9. lemma OAI.ElementaryPositivity.QuantumTorus.ShiftGraded.monomial line 69
10. def OAI.ElementaryPositivity.QuantumTorus.sectionValue line 84
11. lemma OAI.ElementaryPositivity.QuantumTorus.ShiftGraded.sectionValue line 87
12. def OAI.ElementaryPositivity.QuantumTorus.chargeGrade line 105
13. lemma OAI.ElementaryPositivity.QuantumTorus.chargeGrade_one line 110
14. lemma OAI.ElementaryPositivity.QuantumTorus.chargeGrade_X line 116
15. lemma OAI.ElementaryPositivity.QuantumTorus.chargeGrade_mul line 121
16. lemma OAI.ElementaryPositivity.QuantumTorus.chargeGrade_series_mul line 138
17. lemma OAI.ElementaryPositivity.QuantumTorus.chargeGrade_inverse line 147
18. lemma OAI.ElementaryPositivity.QuantumTorus.adjoint_charge line 164