OAI/Combinatorics/Chromatic/QuantumTorus/MonomialConjugation.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ElementaryPositivity.QuantumTorus.X_mul_X_neg line 20
2. def OAI.ElementaryPositivity.QuantumTorus.monomialConjugate line 25
3. lemma OAI.ElementaryPositivity.QuantumTorus.monomialConjugate_coeff line 28
4. lemma OAI.ElementaryPositivity.QuantumTorus.monomialConjugate_coeff_ne_iff line 38
5. lemma OAI.ElementaryPositivity.QuantumTorus.monomialConjugate_one line 43
6. lemma OAI.ElementaryPositivity.QuantumTorus.monomialConjugate_mul line 46
7. lemma OAI.ElementaryPositivity.QuantumTorus.monomialConjugate_regradeBound line 58
8. lemma OAI.ElementaryPositivity.QuantumTorus.regrade_monomialConjugate line 63
9. lemma OAI.ElementaryPositivity.QuantumTorus.monomialConjugate_graded line 83