OAI/Combinatorics/Chromatic/QuantumTorus/QuantumTorus.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.QuantumTorus.Torus line 11
2. instance OAI.ElementaryPositivity.QuantumTorus.Torus.(instance at line 16) line 16
3. instance OAI.ElementaryPositivity.QuantumTorus.Torus.(instance at line 17) line 17
4. def OAI.ElementaryPositivity.QuantumTorus.Torus.monomial line 19
5. def OAI.ElementaryPositivity.QuantumTorus.Torus.multiply line 20
6. instance OAI.ElementaryPositivity.QuantumTorus.Torus.(instance at line 24) line 24
7. instance OAI.ElementaryPositivity.QuantumTorus.Torus.(instance at line 25) line 25
8. lemma OAI.ElementaryPositivity.QuantumTorus.Torus.monomial_zero line 27
9. lemma OAI.ElementaryPositivity.QuantumTorus.Torus.monomial_add line 28
10. lemma OAI.ElementaryPositivity.QuantumTorus.Torus.monomial_smul line 30
11. lemma OAI.ElementaryPositivity.QuantumTorus.Torus.mul_zero line 34
12. lemma OAI.ElementaryPositivity.QuantumTorus.Torus.zero_mul line 35
13. lemma OAI.ElementaryPositivity.QuantumTorus.Torus.add_mul line 38
14. lemma OAI.ElementaryPositivity.QuantumTorus.Torus.mul_add line 48
15. lemma OAI.ElementaryPositivity.QuantumTorus.Torus.monomial_mul_monomial line 61
16. lemma OAI.ElementaryPositivity.QuantumTorus.Torus.mul_assoc line 69
17. lemma OAI.ElementaryPositivity.QuantumTorus.Torus.one_mul line 90
18. lemma OAI.ElementaryPositivity.QuantumTorus.Torus.mul_one line 100
19. instance OAI.ElementaryPositivity.QuantumTorus.Torus.(instance at line 109) line 109
20. def OAI.ElementaryPositivity.QuantumTorus.Torus.X line 113
21. lemma OAI.ElementaryPositivity.QuantumTorus.Torus.X_zero line 115
22. lemma OAI.ElementaryPositivity.QuantumTorus.Torus.X_mul_X line 116
23. lemma OAI.ElementaryPositivity.QuantumTorus.Torus.X_mul_X_of_pairing_zero line 120
24. lemma OAI.ElementaryPositivity.QuantumTorus.Torus.X_commute line 124