OAI/Combinatorics/Chromatic/Walls/RationalPureCocycle.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ElementaryPositivity.RationalFiber.scaleAction line 12
  2. lemma OAI.ElementaryPositivity.RationalFiber.scaleAction_val line 24
  3. lemma OAI.ElementaryPositivity.RationalFiber.linearFactor_ne_zero line 26
  4. def OAI.ElementaryPositivity.RationalFiber.pureStep line 36
  5. abbrev OAI.ElementaryPositivity.RationalFiber.PureExtension line 37
  6. def OAI.ElementaryPositivity.RationalFiber.pureGenerator line 38
  7. def OAI.ElementaryPositivity.RationalFiber.pureRatio line 39
  8. lemma OAI.ElementaryPositivity.RationalFiber.pureRight line 40
  9. lemma OAI.ElementaryPositivity.RationalFiber.pureRatio_zero line 45
  10. lemma OAI.ElementaryPositivity.RationalFiber.pureRatio_one line 46
  11. lemma OAI.ElementaryPositivity.RationalFiber.pureRatio_add line 47
  12. lemma OAI.ElementaryPositivity.RationalFiber.pureRatio_nat line 50
  13. lemma OAI.ElementaryPositivity.RationalFiber.pureRatio_nat_val line 55
  14. lemma OAI.ElementaryPositivity.RationalFiber.pureRatio_neg line 67
  15. def OAI.ElementaryPositivity.RationalFiber.shiftedElementary line 81
  16. lemma OAI.ElementaryPositivity.RationalFiber.shiftedElementary_zero line 83
  17. lemma OAI.ElementaryPositivity.RationalFiber.shiftedElementary_constant line 86
  18. lemma OAI.ElementaryPositivity.RationalFiber.shiftedElementary_step line 89
  19. lemma OAI.ElementaryPositivity.RationalFiber.expandedPure_step line 103
  20. lemma OAI.ElementaryPositivity.RationalFiber.expandedPure_times_shift line 115
  21. lemma OAI.ElementaryPositivity.RationalFiber.ofPowerSeries_inv_constant_one line 130
  22. lemma OAI.ElementaryPositivity.RationalFiber.expandedPure_ratio line 134