OAI/Combinatorics/Chromatic/GradedAlgebra/QuantumTorusSignFactors.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.QuantumTorus.supportedSubring line 14
2. def OAI.ElementaryPositivity.QuantumTorus.nonpositiveCone line 44
3. def OAI.ElementaryPositivity.QuantumTorus.positiveProject line 54
4. def OAI.ElementaryPositivity.QuantumTorus.zeroProject line 56
5. lemma OAI.ElementaryPositivity.QuantumTorus.nonpositive_iff line 59
6. lemma OAI.ElementaryPositivity.QuantumTorus.positiveProject_idem line 74
7. lemma OAI.ElementaryPositivity.QuantumTorus.zeroProject_idem line 81
8. lemma OAI.ElementaryPositivity.QuantumTorus.positive_zero_project line 88