OAI/Combinatorics/Chromatic/GradedAlgebra/HomogenizedPolynomialSection.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ElementaryPositivity.QuantumTorus.homogenize_hahn line 21
2. lemma OAI.ElementaryPositivity.QuantumTorus.ofPowerSeries_adjoint line 41
3. lemma OAI.ElementaryPositivity.QuantumTorus.homogenize_adjoint_actual line 47
4. lemma OAI.ElementaryPositivity.QuantumTorus.homogenize_shiftGraded line 56
5. lemma OAI.ElementaryPositivity.QuantumTorus.conePolynomial_nonnegativeOrder line 72
6. def OAI.ElementaryPositivity.QuantumTorus.polynomialInitial line 82
7. lemma OAI.ElementaryPositivity.QuantumTorus.polynomialInitial_graded line 86
8. lemma OAI.ElementaryPositivity.QuantumTorus.polynomialInitial_incoming line 93