OAI/Combinatorics/Chromatic/Walls/RootProducts.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.ElementaryPositivity.QuantumTorus.WallUnitDatum line 14
  2. def OAI.ElementaryPositivity.QuantumTorus.WallUnitDatum.value line 22
  3. def OAI.ElementaryPositivity.QuantumTorus.WallUnitDatum.Allowed line 26
  4. lemma OAI.ElementaryPositivity.QuantumTorus.rootDegree_nsmul line 29
  5. lemma OAI.ElementaryPositivity.QuantumTorus.weightedRay_graded line 35
  6. lemma OAI.ElementaryPositivity.QuantumTorus.indexedUnit_constant line 48
  7. lemma OAI.ElementaryPositivity.QuantumTorus.WallUnitDatum.constant line 54
  8. lemma OAI.ElementaryPositivity.QuantumTorus.WallUnitDatum.graded line 60
  9. def OAI.ElementaryPositivity.QuantumTorus.literalRootProducts line 64
  10. lemma OAI.ElementaryPositivity.QuantumTorus.literalRootProducts_graded line 67
  11. lemma OAI.ElementaryPositivity.QuantumTorus.literalRootProducts_constant line 77
  12. def OAI.ElementaryPositivity.LaurentPositive.NatCoeff line 96
  13. def OAI.ElementaryPositivity.LaurentPositive.Positive line 98
  14. lemma OAI.ElementaryPositivity.LaurentPositive.natCoeff_zero line 100
  15. lemma OAI.ElementaryPositivity.LaurentPositive.natCoeff_one line 101
  16. lemma OAI.ElementaryPositivity.LaurentPositive.NatCoeff.add line 102
  17. lemma OAI.ElementaryPositivity.LaurentPositive.NatCoeff.mul line 106
  18. lemma OAI.ElementaryPositivity.LaurentPositive.NatCoeff.sum line 110
  19. lemma OAI.ElementaryPositivity.LaurentPositive.positive_zero line 119
  20. lemma OAI.ElementaryPositivity.LaurentPositive.positive_one line 120
  21. lemma OAI.ElementaryPositivity.LaurentPositive.Positive.add line 124
  22. lemma OAI.ElementaryPositivity.LaurentPositive.Positive.mul line 126
  23. lemma OAI.ElementaryPositivity.LaurentPositive.Positive.sum line 132
  24. lemma OAI.ElementaryPositivity.LaurentPositive.single line 141
  25. lemma OAI.ElementaryPositivity.LaurentPositive.series line 146
  26. lemma OAI.ElementaryPositivity.LaurentPositive.of_converges line 152