OAI/Combinatorics/Chromatic/Walls/TorusPositive.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ElementaryPositivity.QuantumTorus.TorusPositive line 15
  2. def OAI.ElementaryPositivity.QuantumTorus.IntegralPositive line 16
  3. lemma OAI.ElementaryPositivity.QuantumTorus.torusPositive_zero line 18
  4. lemma OAI.ElementaryPositivity.QuantumTorus.TorusPositive.add line 19
  5. lemma OAI.ElementaryPositivity.QuantumTorus.TorusPositive.sum line 22
  6. lemma OAI.ElementaryPositivity.QuantumTorus.torusPositive_monomial line 30
  7. lemma OAI.ElementaryPositivity.QuantumTorus.TorusPositive.mul line 40
  8. lemma OAI.ElementaryPositivity.QuantumTorus.completedPositive_C_X line 52
  9. lemma OAI.ElementaryPositivity.QuantumTorus.IntegralPositive.mul line 59
  10. lemma OAI.ElementaryPositivity.QuantumTorus.push_positive line 69
  11. def OAI.ElementaryPositivity.QuantumTorus.sumSupport line 90
  12. lemma OAI.ElementaryPositivity.QuantumTorus.torus_mul_support line 92
  13. lemma OAI.ElementaryPositivity.QuantumTorus.SeriesConverges.mul_of_support line 107
  14. lemma OAI.ElementaryPositivity.QuantumTorus.SeriesConverges.mul_C line 121
  15. lemma OAI.ElementaryPositivity.QuantumTorus.SeriesGraded.mul_C_support line 132
  16. theorem OAI.ElementaryPositivity.QuantumTorus.SeriesConverges.adjoint line 138
  17. lemma OAI.ElementaryPositivity.QuantumTorus.IntegralPositive.of_converges line 153