OAI/Combinatorics/Chromatic/Walls/RayLaurentExpansion.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ElementaryPositivity.WallUnits.LaurentRay.reciprocal_transcendental line 15
  2. def OAI.ElementaryPositivity.WallUnits.LaurentRay.reciprocalEval line 19
  3. lemma OAI.ElementaryPositivity.WallUnits.LaurentRay.reciprocalEval_injective line 21
  4. lemma OAI.ElementaryPositivity.WallUnits.LaurentRay.reciprocalEval_regular line 23
  5. def OAI.ElementaryPositivity.WallUnits.LaurentRay.reciprocal line 27
  6. lemma OAI.ElementaryPositivity.WallUnits.LaurentRay.reciprocal_X line 29
  7. def OAI.ElementaryPositivity.WallUnits.LaurentRay.atInfinity line 35
  8. lemma OAI.ElementaryPositivity.WallUnits.LaurentRay.atInfinity_injective line 38
  9. lemma OAI.ElementaryPositivity.WallUnits.LaurentRay.atInfinity_v line 40
  10. lemma OAI.ElementaryPositivity.WallUnits.LaurentRay.atInfinity_v_pow line 47
  11. lemma OAI.ElementaryPositivity.WallUnits.LaurentRay.atInfinity_q line 52
  12. lemma OAI.ElementaryPositivity.WallUnits.LaurentRay.map_elementaryCoeff line 55
  13. lemma OAI.ElementaryPositivity.WallUnits.LaurentRay.map_elementary line 61
  14. lemma OAI.ElementaryPositivity.WallUnits.LaurentRay.elementary_atInfinity line 66
  15. lemma OAI.ElementaryPositivity.WallUnits.LaurentRay.map_complete line 72
  16. lemma OAI.ElementaryPositivity.WallUnits.LaurentRay.complete_atInfinity line 80
  17. lemma OAI.ElementaryPositivity.WallUnits.LaurentRay.atInfinity_eval_monomial line 85
  18. lemma OAI.ElementaryPositivity.WallUnits.LaurentRay.atInfinity_eval_coeff line 94
  19. lemma OAI.ElementaryPositivity.WallUnits.LaurentRay.positive_coeff_atInfinity line 108
  20. def OAI.ElementaryPositivity.FiniteFunctionValues.values line 124
  21. lemma OAI.ElementaryPositivity.FiniteFunctionValues.count_values line 126
  22. lemma OAI.ElementaryPositivity.FiniteFunctionValues.values_comp line 131
  23. lemma OAI.ElementaryPositivity.FiniteFunctionValues.values_eq_iff line 135
  24. lemma OAI.ElementaryPositivity.FiniteFunctionValues.values_fin line 148
  25. lemma OAI.ElementaryPositivity.FiniteFunctionValues.values_card line 152
  26. lemma OAI.ElementaryPositivity.FiniteFunctionValues.values_fin_surjective line 155