OAI/Combinatorics/Chromatic/GradedAlgebra/HalfspacePolynomialCoefficients.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.QuantumTorus.rootChartRatio line 24
2. lemma OAI.ElementaryPositivity.QuantumTorus.halfspace_polynomial_coefficients line 35
3. lemma OAI.ElementaryPositivity.QuantumTorus.halfspace_canonical_polynomial_coefficients line 51
4. def OAI.ElementaryPositivity.QuantumTorus.rootSectionChart line 88
5. def OAI.ElementaryPositivity.QuantumTorus.polynomialSectionCoefficient line 97
6. lemma OAI.ElementaryPositivity.QuantumTorus.rootSectionChart_negative line 100
7. lemma OAI.ElementaryPositivity.QuantumTorus.rootChartRatio_section line 113
8. lemma OAI.ElementaryPositivity.QuantumTorus.polynomialSection_rebase line 124
9. lemma OAI.ElementaryPositivity.QuantumTorus.actualPolynomialAdjoint_inverse_finite line 140
10. lemma OAI.ElementaryPositivity.QuantumTorus.actualPolynomialAdjointCoefficient_one line 151
11. lemma OAI.ElementaryPositivity.QuantumTorus.polynomialSection_negative line 156