OAI/Combinatorics/Chromatic/QuantumTorus/RationalFiberTorus.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ElementaryPositivity.RationalFiber.FiberTorus line 10
  2. instance OAI.ElementaryPositivity.RationalFiber.FiberTorus.(instance at line 13) line 13
  3. def OAI.ElementaryPositivity.RationalFiber.FiberTorus.monomial line 14
  4. def OAI.ElementaryPositivity.RationalFiber.FiberTorus.twist line 15
  5. lemma OAI.ElementaryPositivity.RationalFiber.FiberTorus.twist_add line 16
  6. lemma OAI.ElementaryPositivity.RationalFiber.FiberTorus.twist_constant line 19
  7. lemma OAI.ElementaryPositivity.RationalFiber.FiberTorus.twist_zero line 20
  8. def OAI.ElementaryPositivity.RationalFiber.FiberTorus.multiply line 21
  9. instance OAI.ElementaryPositivity.RationalFiber.FiberTorus.(instance at line 24) line 24
  10. instance OAI.ElementaryPositivity.RationalFiber.FiberTorus.(instance at line 25) line 25
  11. lemma OAI.ElementaryPositivity.RationalFiber.FiberTorus.monomial_zero line 26
  12. lemma OAI.ElementaryPositivity.RationalFiber.FiberTorus.monomial_add line 27
  13. lemma OAI.ElementaryPositivity.RationalFiber.FiberTorus.mul_zero line 29
  14. lemma OAI.ElementaryPositivity.RationalFiber.FiberTorus.zero_mul line 30
  15. lemma OAI.ElementaryPositivity.RationalFiber.FiberTorus.add_mul line 31
  16. lemma OAI.ElementaryPositivity.RationalFiber.FiberTorus.mul_add line 39
  17. lemma OAI.ElementaryPositivity.RationalFiber.FiberTorus.monomial_mul line 50
  18. lemma OAI.ElementaryPositivity.RationalFiber.FiberTorus.mul_assoc line 57
  19. lemma OAI.ElementaryPositivity.RationalFiber.FiberTorus.one_mul line 77
  20. lemma OAI.ElementaryPositivity.RationalFiber.FiberTorus.mul_one line 86
  21. instance OAI.ElementaryPositivity.RationalFiber.FiberTorus.(instance at line 94) line 94
  22. def OAI.ElementaryPositivity.RationalFiber.FiberTorus.coefficient line 97
  23. def OAI.ElementaryPositivity.RationalFiber.FiberTorus.X line 98
  24. lemma OAI.ElementaryPositivity.RationalFiber.FiberTorus.rational_commutation line 99
  25. def OAI.ElementaryPositivity.RationalFiber.off line 112
  26. lemma OAI.ElementaryPositivity.RationalFiber.off_val line 116
  27. lemma OAI.ElementaryPositivity.RationalFiber.split_sum line 117
  28. lemma OAI.ElementaryPositivity.RationalFiber.off_p line 118
  29. lemma OAI.ElementaryPositivity.RationalFiber.off_complement line 119
  30. def OAI.ElementaryPositivity.RationalFiber.complementAlpha line 123
  31. def OAI.ElementaryPositivity.RationalFiber.complementOmega line 124
  32. lemma OAI.ElementaryPositivity.RationalFiber.split_pairing line 130
  33. def OAI.ElementaryPositivity.RationalFiber.centeredScalar line 146
  34. lemma OAI.ElementaryPositivity.RationalFiber.centeredScalar_mul line 148