OAI/Combinatorics/Chromatic/GradedAlgebra/InputOrderedProduct.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.WeightedTorusSeries.partialCoefficient line 18
2. lemma OAI.ElementaryPositivity.WeightedTorusSeries.partialCoefficient_union line 22
3. lemma OAI.ElementaryPositivity.WeightedTorusSeries.partialCoefficient_empty line 49
4. lemma OAI.ElementaryPositivity.WeightedTorusSeries.push_partial_empty line 59
5. lemma OAI.ElementaryPositivity.WeightedTorusSeries.push_partial_union line 79
6. theorem OAI.ElementaryPositivity.WeightedTorusSeries.push_partial_list line 87
7. lemma OAI.ElementaryPositivity.WeightedTorusSeries.weight_single line 119
8. lemma OAI.ElementaryPositivity.WeightedTorusSeries.supported_single_eq line 123
9. lemma OAI.ElementaryPositivity.WeightedTorusSeries.single_nsmul line 130
10. lemma OAI.ElementaryPositivity.WeightedTorusSeries.push_axis line 136