OAI/Combinatorics/Chromatic/GradedAlgebra/LaurentContinuity.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ElementaryPositivity.LaurentPrecision.Series line 10
  2. def OAI.ElementaryPositivity.LaurentPrecision.LowerBound line 12
  3. def OAI.ElementaryPositivity.LaurentPrecision.Agrees line 13
  4. lemma OAI.ElementaryPositivity.LaurentPrecision.lowerBound_iff_orderTop line 15
  5. lemma OAI.ElementaryPositivity.LaurentPrecision.lowerBound_order line 20
  6. lemma OAI.ElementaryPositivity.LaurentPrecision.lowerBound_mono line 23
  7. lemma OAI.ElementaryPositivity.LaurentPrecision.lowerBound_zero line 26
  8. lemma OAI.ElementaryPositivity.LaurentPrecision.lowerBound_add line 28
  9. lemma OAI.ElementaryPositivity.LaurentPrecision.lowerBound_mul line 33
  10. lemma OAI.ElementaryPositivity.LaurentPrecision.agrees_iff_sub line 39
  11. lemma OAI.ElementaryPositivity.LaurentPrecision.agrees_refl line 42
  12. lemma OAI.ElementaryPositivity.LaurentPrecision.agrees_symm line 43
  13. lemma OAI.ElementaryPositivity.LaurentPrecision.agrees_mono line 45
  14. lemma OAI.ElementaryPositivity.LaurentPrecision.agrees_add line 47
  15. lemma OAI.ElementaryPositivity.LaurentPrecision.agrees_neg line 51
  16. lemma OAI.ElementaryPositivity.LaurentPrecision.agrees_sub line 54
  17. lemma OAI.ElementaryPositivity.LaurentPrecision.agrees_mul line 58
  18. def OAI.ElementaryPositivity.LaurentPrecision.Converges line 74
  19. lemma OAI.ElementaryPositivity.LaurentPrecision.converges_const line 77
  20. lemma OAI.ElementaryPositivity.LaurentPrecision.Converges.coeff line 80
  21. lemma OAI.ElementaryPositivity.LaurentPrecision.Converges.lowerBound line 84
  22. lemma OAI.ElementaryPositivity.LaurentPrecision.Converges.add line 90
  23. lemma OAI.ElementaryPositivity.LaurentPrecision.Converges.neg line 97
  24. lemma OAI.ElementaryPositivity.LaurentPrecision.Converges.sub line 102
  25. lemma OAI.ElementaryPositivity.LaurentPrecision.Converges.mul line 109
  26. lemma OAI.ElementaryPositivity.LaurentPrecision.Converges.pow line 117
  27. lemma OAI.ElementaryPositivity.LaurentPrecision.Converges.sum line 123
  28. lemma OAI.ElementaryPositivity.LaurentPrecision.Converges.nat_coeff line 133