OAI/Combinatorics/Chromatic/Shuffle/PrimitiveStringBounds.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ElementaryPositivity.RawShuffle.stringBaseComponent_basis line 18
  2. def OAI.ElementaryPositivity.RawShuffle.stringBaseComponentEmbedding line 35
  3. lemma OAI.ElementaryPositivity.RawShuffle.stringBaseComponentEmbedding_injective line 45
  4. lemma OAI.ElementaryPositivity.RawShuffle.stringBaseComponent_finite line 52
  5. lemma OAI.ElementaryPositivity.RawShuffle.stringBaseDegree_finite line 58
  6. lemma OAI.ElementaryPositivity.RawShuffle.stringBase_auxiliary_upper line 65
  7. lemma OAI.ElementaryPositivity.RawShuffle.associatedGrade_eq_zero_below line 75
  8. lemma OAI.ElementaryPositivity.RawShuffle.stringBase_auxiliary_lower line 84
  9. theorem OAI.ElementaryPositivity.RawShuffle.stringStarts_bounded_finite line 91
  10. lemma OAI.ElementaryPositivity.RawShuffle.globalOriginal_nonzero_bounds line 121
  11. abbrev OAI.ElementaryPositivity.RawShuffle.SlopeStringCoefficient line 139
  12. lemma OAI.ElementaryPositivity.RawShuffle.slopeStringCoefficient_bounds line 142
  13. def OAI.ElementaryPositivity.RawShuffle.slopeStringCutoff line 152
  14. lemma OAI.ElementaryPositivity.RawShuffle.slopeStringCutoff_bound line 156
  15. lemma OAI.ElementaryPositivity.RawShuffle.sigmaSubtype_ext line 161
  16. def OAI.ElementaryPositivity.RawShuffle.slopeStringCutoffEquiv line 169
  17. lemma OAI.ElementaryPositivity.RawShuffle.slopeStringCoefficient_finite line 193
  18. theorem OAI.ElementaryPositivity.RawShuffle.slopeStringHilbert_coefficient line 199