OAI/Combinatorics/Chromatic/Shuffle/LaurentKernel.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ElementaryPositivity.RawShuffle.SeparationInfinity.inverseExponent line 16
  2. def OAI.ElementaryPositivity.RawShuffle.SeparationInfinity.rawFactor line 19
  3. def OAI.ElementaryPositivity.RawShuffle.SeparationInfinity.renameSeries line 24
  4. lemma OAI.ElementaryPositivity.RawShuffle.SeparationInfinity.rename_rawFactor line 30
  5. def OAI.ElementaryPositivity.RawShuffle.SeparationInfinity.rawInverseKernelUnit line 40
  6. lemma OAI.ElementaryPositivity.RawShuffle.SeparationInfinity.rawInverseKernelUnit_symmetric line 44
  7. def OAI.ElementaryPositivity.RawShuffle.SeparationInfinity.IsSeparate line 58
  8. def OAI.ElementaryPositivity.RawShuffle.SeparationInfinity.separateSeries line 61
  9. lemma OAI.ElementaryPositivity.RawShuffle.SeparationInfinity.realize_separateSeries line 65
  10. lemma OAI.ElementaryPositivity.RawShuffle.SeparationInfinity.realize_injective line 74
  11. def OAI.ElementaryPositivity.RawShuffle.SeparationInfinity.liftSeparateUnit line 78
  12. def OAI.ElementaryPositivity.RawShuffle.SeparationInfinity.inverseKernelUnit line 102
  13. lemma OAI.ElementaryPositivity.RawShuffle.SeparationInfinity.realize_inverseKernelUnit line 106
  14. def OAI.ElementaryPositivity.RawShuffle.SeparationInfinity.quotientInverseKernelUnit line 111