OAI/Combinatorics/Chromatic/GradedAlgebra/NonpHomogenize.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.QuantumTorus.homogenizeMonomial line 15
2. def OAI.ElementaryPositivity.QuantumTorus.homogenize line 18
3. lemma OAI.ElementaryPositivity.QuantumTorus.homogenize_monomial line 20
4. lemma OAI.ElementaryPositivity.QuantumTorus.torus_sum_monomial line 24
5. lemma OAI.ElementaryPositivity.QuantumTorus.homogenize_coeff line 28
6. lemma OAI.ElementaryPositivity.QuantumTorus.homogenize_monomial_mul line 43
7. lemma OAI.ElementaryPositivity.QuantumTorus.homo_sum_mul line 49
8. lemma OAI.ElementaryPositivity.QuantumTorus.homo_mul_sum line 55
9. lemma OAI.ElementaryPositivity.QuantumTorus.homogenize_mul line 61
10. def OAI.ElementaryPositivity.QuantumTorus.biHomogenizeMonomial line 104
11. def OAI.ElementaryPositivity.QuantumTorus.biHomogenize line 108
12. lemma OAI.ElementaryPositivity.QuantumTorus.biHomogenize_monomial line 110
13. lemma OAI.ElementaryPositivity.QuantumTorus.biHomogenize_coeff line 114
14. lemma OAI.ElementaryPositivity.QuantumTorus.biHomogenize_monomial_mul line 135
15. lemma OAI.ElementaryPositivity.QuantumTorus.biHomogenize_mul line 143
16. lemma OAI.ElementaryPositivity.QuantumTorus.biHomogenize_one line 172