OAI/Combinatorics/Chromatic/GradedAlgebra/LaurentRectangularKernel.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.RectangularKernel.rectangular line 10
2. lemma OAI.ElementaryPositivity.RectangularKernel.rectangular_add line 14
3. lemma OAI.ElementaryPositivity.RectangularKernel.rectangular_neg line 19
4. lemma OAI.ElementaryPositivity.RectangularKernel.rectangular_sub line 24
5. lemma OAI.ElementaryPositivity.RectangularKernel.rectangular_map line 29
6. lemma OAI.ElementaryPositivity.RectangularKernel.rectangular_transpose line 35
7. lemma OAI.ElementaryPositivity.RectangularKernel.rectangular_sum line 47
8. lemma OAI.ElementaryPositivity.RectangularKernel.rectangular_diagonal line 59
9. lemma OAI.ElementaryPositivity.RectangularKernel.four_rectangle_cancellation line 72
10. lemma OAI.ElementaryPositivity.RectangularKernel.rectangular_mul line 108
11. lemma OAI.ElementaryPositivity.RectangularKernel.prod_zpow_sum line 113
12. lemma OAI.ElementaryPositivity.RectangularKernel.rectangular_constant line 120
13. lemma OAI.ElementaryPositivity.RectangularKernel.rectangular_scalar_mul line 134