OAI/Combinatorics/Chromatic/Shuffle/HNHomogeneousBasis.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ElementaryPositivity.RawShuffle.dfinsupp_basis_apply line 12
  2. abbrev OAI.ElementaryPositivity.RawShuffle.HomogeneousBIndex line 33
  3. def OAI.ElementaryPositivity.RawShuffle.homogeneousBBasis line 34
  4. lemma OAI.ElementaryPositivity.RawShuffle.homogeneousBBasis_mem line 36
  5. def OAI.ElementaryPositivity.RawShuffle.HNBasisIndex line 40
  6. def OAI.ElementaryPositivity.RawShuffle.hnTensorBasis line 43
  7. def OAI.ElementaryPositivity.RawShuffle.hnBasisDegree line 47
  8. lemma OAI.ElementaryPositivity.RawShuffle.hnTensorBasis_nil line 51
  9. lemma OAI.ElementaryPositivity.RawShuffle.hnTensorBasis_cons line 55
  10. lemma OAI.ElementaryPositivity.RawShuffle.hnTensorBasis_polynomial line 60
  11. def OAI.ElementaryPositivity.RawShuffle.hnHomogeneousBasis line 78
  12. lemma OAI.ElementaryPositivity.RawShuffle.hnHomogeneousBasis_apply line 84
  13. lemma OAI.ElementaryPositivity.RawShuffle.hnHomogeneousBasis_degree line 93