OAI/Combinatorics/Chromatic/GradedAlgebra/LaurentGeometric.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ElementaryPositivity.LaurentAtInfinity.geometric line 10
  2. lemma OAI.ElementaryPositivity.LaurentAtInfinity.one_sub_mul_geometric line 11
  3. lemma OAI.ElementaryPositivity.LaurentAtInfinity.oneSubUnit_inv line 21
  4. lemma OAI.ElementaryPositivity.LaurentAtInfinity.affineUnit_inv_val line 24
  5. def OAI.ElementaryPositivity.LaurentAtInfinity.IsHomogeneous line 44
  6. lemma OAI.ElementaryPositivity.LaurentAtInfinity.IsHomogeneous.zero line 47
  7. lemma OAI.ElementaryPositivity.LaurentAtInfinity.IsHomogeneous.add line 51
  8. lemma OAI.ElementaryPositivity.LaurentAtInfinity.IsHomogeneous.neg line 56
  9. lemma OAI.ElementaryPositivity.LaurentAtInfinity.IsHomogeneous.sub line 61
  10. lemma OAI.ElementaryPositivity.LaurentAtInfinity.homogeneous_single line 66
  11. lemma OAI.ElementaryPositivity.LaurentAtInfinity.homogeneous_one line 75
  12. lemma OAI.ElementaryPositivity.LaurentAtInfinity.IsHomogeneous.mul line 79
  13. lemma OAI.ElementaryPositivity.LaurentAtInfinity.IsHomogeneous.pow line 90
  14. lemma OAI.ElementaryPositivity.LaurentAtInfinity.homogeneous_affine line 99
  15. lemma OAI.ElementaryPositivity.LaurentAtInfinity.homogeneous_affine_inv line 108
  16. lemma OAI.ElementaryPositivity.LaurentAtInfinity.homogeneous_affine_zpow line 126
  17. lemma OAI.ElementaryPositivity.LaurentAtInfinity.homogeneous_sum line 146
  18. lemma OAI.ElementaryPositivity.LaurentAtInfinity.homogeneous_prod line 154
  19. lemma OAI.ElementaryPositivity.LaurentAtInfinity.homogeneous_ringHom line 163