OAI/Combinatorics/Chromatic/Walls/RationalFiberReciprocal.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ElementaryPositivity.RationalFiber.ratFunc_hom_ext_C_X line 11
  2. lemma OAI.ElementaryPositivity.RationalFiber.reciprocal_transcendental line 19
  3. def OAI.ElementaryPositivity.RationalFiber.reciprocalEval line 22
  4. lemma OAI.ElementaryPositivity.RationalFiber.reciprocalEval_injective line 24
  5. lemma OAI.ElementaryPositivity.RationalFiber.reciprocalEval_regular line 26
  6. def OAI.ElementaryPositivity.RationalFiber.reciprocal line 29
  7. lemma OAI.ElementaryPositivity.RationalFiber.reciprocal_polynomial line 31
  8. lemma OAI.ElementaryPositivity.RationalFiber.reciprocal_X line 34
  9. lemma OAI.ElementaryPositivity.RationalFiber.reciprocal_constant line 38
  10. lemma OAI.ElementaryPositivity.RationalFiber.reciprocal_involutive line 41
  11. lemma OAI.ElementaryPositivity.RationalFiber.reciprocal_scale line 43
  12. def OAI.ElementaryPositivity.RationalFiber.reciprocalEquiv line 48
  13. def OAI.ElementaryPositivity.RationalFiber.expandInfinity line 50
  14. lemma OAI.ElementaryPositivity.RationalFiber.expandInfinity_injective line 51
  15. lemma OAI.ElementaryPositivity.RationalFiber.expandZero_X line 53
  16. lemma OAI.ElementaryPositivity.RationalFiber.expandZero_constant line 55
  17. lemma OAI.ElementaryPositivity.RationalFiber.expandZero_X_zpow line 59
  18. lemma OAI.ElementaryPositivity.RationalFiber.expandInfinity_X_zpow line 62