OAI/Combinatorics/Chromatic/QuantumTorus/TorusProjection.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.ElementaryPositivity.QuantumTorus.sum_monomialsline 16 - lemma
OAI.ElementaryPositivity.QuantumTorus.zeroProject_monomialline 19 - lemma
OAI.ElementaryPositivity.QuantumTorus.zeroProject_monomial_mulline 23 - lemma
OAI.ElementaryPositivity.QuantumTorus.zeroProject_mul_nonpositiveline 38 - lemma
OAI.ElementaryPositivity.QuantumTorus.zeroProject_oneline 59 - lemma
OAI.ElementaryPositivity.QuantumTorus.zeroFactor_coeff_projectionline 65