OAI/Combinatorics/Chromatic/GradedAlgebra/LaurentInfinity.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ElementaryPositivity.LaurentAtInfinity.mapRing line 10
  2. lemma OAI.ElementaryPositivity.LaurentAtInfinity.mapRing_coeff line 17
  3. lemma OAI.ElementaryPositivity.LaurentAtInfinity.mapRing_single line 20
  4. lemma OAI.ElementaryPositivity.LaurentAtInfinity.mapRing_C line 25
  5. lemma OAI.ElementaryPositivity.LaurentAtInfinity.mapRing_injective line 28
  6. def OAI.ElementaryPositivity.LaurentAtInfinity.mapLinear line 38
  7. lemma OAI.ElementaryPositivity.LaurentAtInfinity.mapLinear_coeff line 43
  8. def OAI.ElementaryPositivity.LaurentAtInfinity.zUnit line 47
  9. lemma OAI.ElementaryPositivity.LaurentAtInfinity.zUnit_val line 53
  10. lemma OAI.ElementaryPositivity.LaurentAtInfinity.zUnit_map line 55
  11. def OAI.ElementaryPositivity.LaurentAtInfinity.oneSubUnit line 60
  12. lemma OAI.ElementaryPositivity.LaurentAtInfinity.oneSubUnit_val line 63
  13. def OAI.ElementaryPositivity.LaurentAtInfinity.affineUnit line 67
  14. lemma OAI.ElementaryPositivity.LaurentAtInfinity.affineUnit_val line 70
  15. lemma OAI.ElementaryPositivity.LaurentAtInfinity.affineUnit_map line 83
  16. def OAI.ElementaryPositivity.LaurentAtInfinity.polynomial line 88
  17. lemma OAI.ElementaryPositivity.LaurentAtInfinity.polynomial_C line 91
  18. lemma OAI.ElementaryPositivity.LaurentAtInfinity.polynomial_X line 94
  19. def OAI.ElementaryPositivity.LaurentAtInfinity.polynomialAlg line 97
  20. lemma OAI.ElementaryPositivity.LaurentAtInfinity.polynomial_monomial line 105
  21. lemma OAI.ElementaryPositivity.LaurentAtInfinity.polynomial_map line 112
  22. lemma OAI.ElementaryPositivity.LaurentAtInfinity.polynomial_coeff line 118
  23. lemma OAI.ElementaryPositivity.LaurentAtInfinity.polynomial_coeff_positive line 124
  24. lemma OAI.ElementaryPositivity.LaurentAtInfinity.polynomial_injective line 132