OAI/Combinatorics/Chromatic/GradedAlgebra/WeightedTorusSeries.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ElementaryPositivity.WeightedTorusSeries.weight line 16
  2. lemma OAI.ElementaryPositivity.WeightedTorusSeries.coord_le_weight line 23
  3. abbrev OAI.ElementaryPositivity.WeightedTorusSeries.Slice line 27
  4. instance OAI.ElementaryPositivity.WeightedTorusSeries.sliceFinite line 28
  5. instance OAI.ElementaryPositivity.WeightedTorusSeries.sliceFintype line 34
  6. lemma OAI.ElementaryPositivity.WeightedTorusSeries.split_heq line 37
  7. def OAI.ElementaryPositivity.WeightedTorusSeries.splitSliceEquiv line 42
  8. def OAI.ElementaryPositivity.WeightedTorusSeries.pairSliceEquiv line 52
  9. lemma OAI.ElementaryPositivity.WeightedTorusSeries.sum_split line 65
  10. def OAI.ElementaryPositivity.WeightedTorusSeries.pushCoeff line 87
  11. def OAI.ElementaryPositivity.WeightedTorusSeries.push line 89
  12. def OAI.ElementaryPositivity.WeightedTorusSeries.convolution line 91
  13. lemma OAI.ElementaryPositivity.WeightedTorusSeries.monomial_sum line 94
  14. lemma OAI.ElementaryPositivity.WeightedTorusSeries.torus_sum_mul line 98
  15. lemma OAI.ElementaryPositivity.WeightedTorusSeries.torus_mul_sum line 105
  16. lemma OAI.ElementaryPositivity.WeightedTorusSeries.pushCoeff_convolution line 112
  17. lemma OAI.ElementaryPositivity.WeightedTorusSeries.push_convolution line 130