OAI/Combinatorics/Chromatic/GradedAlgebra/SupportedConvolution.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.WeightedTorusSeries.Supported line 15
2. def OAI.ElementaryPositivity.WeightedTorusSeries.restrictDim line 17
3. lemma OAI.ElementaryPositivity.WeightedTorusSeries.restrictDim_supported line 20
4. lemma OAI.ElementaryPositivity.WeightedTorusSeries.restrictDim_eq line 25
5. lemma OAI.ElementaryPositivity.WeightedTorusSeries.supported_add line 30
6. lemma OAI.ElementaryPositivity.WeightedTorusSeries.restrictDim_split line 37
7. lemma OAI.ElementaryPositivity.WeightedTorusSeries.split_left_restrict line 48
8. def OAI.ElementaryPositivity.WeightedTorusSeries.supportedCoefficient line 59
9. lemma OAI.ElementaryPositivity.WeightedTorusSeries.supported_convolution line 63