OAI/Combinatorics/Chromatic/GradedAlgebra/LaurentRegrade.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ElementaryPositivity.QuantumTorus.LaurentBounded line 17
  2. lemma OAI.ElementaryPositivity.QuantumTorus.LaurentBounded.zero line 21
  3. lemma OAI.ElementaryPositivity.QuantumTorus.LaurentBounded.one line 24
  4. lemma OAI.ElementaryPositivity.QuantumTorus.LaurentBounded.add line 35
  5. lemma OAI.ElementaryPositivity.QuantumTorus.LaurentBounded.neg line 44
  6. lemma OAI.ElementaryPositivity.QuantumTorus.LaurentBounded.mul line 52
  7. lemma OAI.ElementaryPositivity.QuantumTorus.LaurentBounded.laurent_vanish line 65
  8. def OAI.ElementaryPositivity.QuantumTorus.laurentRegradeFamily line 79
  9. def OAI.ElementaryPositivity.QuantumTorus.laurentRegrade line 101
  10. lemma OAI.ElementaryPositivity.QuantumTorus.laurentRegrade_coeff line 105
  11. def OAI.ElementaryPositivity.QuantumTorus.BiBounded line 131
  12. lemma OAI.ElementaryPositivity.QuantumTorus.BiBounded.zero line 133
  13. lemma OAI.ElementaryPositivity.QuantumTorus.BiBounded.one line 134
  14. lemma OAI.ElementaryPositivity.QuantumTorus.BiBounded.add line 145
  15. lemma OAI.ElementaryPositivity.QuantumTorus.BiBounded.neg line 153
  16. lemma OAI.ElementaryPositivity.QuantumTorus.BiBounded.mul line 161
  17. lemma OAI.ElementaryPositivity.QuantumTorus.BiBounded.bi_vanish line 171
  18. lemma OAI.ElementaryPositivity.QuantumTorus.BiBounded.bi_product_vanish line 182
  19. def OAI.ElementaryPositivity.QuantumTorus.boundedBiRegrade line 199
  20. lemma OAI.ElementaryPositivity.QuantumTorus.boundedBiRegrade_coeff line 202
  21. lemma OAI.ElementaryPositivity.QuantumTorus.boundedBiRegrade_hasSum line 211
  22. lemma OAI.ElementaryPositivity.QuantumTorus.boundedBiRegrade_product_summable line 223
  23. lemma OAI.ElementaryPositivity.QuantumTorus.boundedBiRegrade_mul line 240
  24. lemma OAI.ElementaryPositivity.QuantumTorus.boundedBiRegrade_add line 257
  25. lemma OAI.ElementaryPositivity.QuantumTorus.boundedBiRegrade_one line 268
  26. lemma OAI.ElementaryPositivity.QuantumTorus.boundedBiRegrade_zero line 280