OAI/Combinatorics/Chromatic/GradedAlgebra/RegradeLog.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.FormalLog.logPolynomial line 14
2. lemma OAI.ElementaryPositivity.FormalLog.logPolynomial_coeff line 16
3. lemma OAI.ElementaryPositivity.QuantumTorus.homogenize_smul line 38
4. def OAI.ElementaryPositivity.QuantumTorus.regradeLinear line 44
5. lemma OAI.ElementaryPositivity.QuantumTorus.RegradeBound.pow line 61
6. lemma OAI.ElementaryPositivity.QuantumTorus.regrade_pow line 68
7. lemma OAI.ElementaryPositivity.QuantumTorus.regrade_logPolynomial line 73
8. lemma OAI.ElementaryPositivity.QuantumTorus.regrade_constant line 99
9. lemma OAI.ElementaryPositivity.QuantumTorus.regrade_coeff_congr line 105
10. lemma OAI.ElementaryPositivity.QuantumTorus.regrade_log line 112