OAI/Combinatorics/Chromatic/Walls/RationalFiberScale.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ElementaryPositivity.RationalFiber.polynomialScale line 11
  2. lemma OAI.ElementaryPositivity.RationalFiber.polynomialScale_apply line 15
  3. def OAI.ElementaryPositivity.RationalFiber.scaleEval line 18
  4. lemma OAI.ElementaryPositivity.RationalFiber.scaleEval_injective line 20
  5. lemma OAI.ElementaryPositivity.RationalFiber.scaleEval_regular line 22
  6. def OAI.ElementaryPositivity.RationalFiber.scale line 25
  7. lemma OAI.ElementaryPositivity.RationalFiber.scale_polynomial line 27
  8. lemma OAI.ElementaryPositivity.RationalFiber.ratFunc_hom_ext line 32
  9. lemma OAI.ElementaryPositivity.RationalFiber.scale_one line 38
  10. lemma OAI.ElementaryPositivity.RationalFiber.scale_mul line 42
  11. lemma OAI.ElementaryPositivity.RationalFiber.scale_constant line 51
  12. lemma OAI.ElementaryPositivity.RationalFiber.scale_X line 55
  13. def OAI.ElementaryPositivity.RationalFiber.scaleEquiv line 59
  14. def OAI.ElementaryPositivity.RationalFiber.expandZero line 64
  15. lemma OAI.ElementaryPositivity.RationalFiber.expandZero_injective line 65