OAI/Combinatorics/Chromatic/GradedAlgebra/NonpRegrade.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ElementaryPositivity.QuantumTorus.torus_product_nonzero line 17
  2. lemma OAI.ElementaryPositivity.QuantumTorus.nonp_torus_eval_sum line 31
  3. lemma OAI.ElementaryPositivity.QuantumTorus.series_product_nonzero line 37
  4. def OAI.ElementaryPositivity.QuantumTorus.RegradeBound line 46
  5. lemma OAI.ElementaryPositivity.QuantumTorus.RegradeBound.zero line 49
  6. lemma OAI.ElementaryPositivity.QuantumTorus.RegradeBound.one line 50
  7. lemma OAI.ElementaryPositivity.QuantumTorus.RegradeBound.add line 61
  8. lemma OAI.ElementaryPositivity.QuantumTorus.RegradeBound.neg line 69
  9. lemma OAI.ElementaryPositivity.QuantumTorus.RegradeBound.mul line 75
  10. lemma OAI.ElementaryPositivity.QuantumTorus.RegradeBound.homogenize_vanish line 85
  11. def OAI.ElementaryPositivity.QuantumTorus.regrade line 112
  12. lemma OAI.ElementaryPositivity.QuantumTorus.regrade_coeff line 114
  13. lemma OAI.ElementaryPositivity.QuantumTorus.regrade_hasSum line 123
  14. lemma OAI.ElementaryPositivity.QuantumTorus.regrade_product_summable line 134
  15. lemma OAI.ElementaryPositivity.QuantumTorus.regrade_mul line 159
  16. lemma OAI.ElementaryPositivity.QuantumTorus.regrade_add line 173