OAI/Combinatorics/Chromatic/GradedAlgebra/Product.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ElementaryPositivity.SlopeArithmetic.OnSlopeOrZero line 10
2. lemma OAI.ElementaryPositivity.SlopeArithmetic.onSlopeOrZero_of_mass line 13
3. lemma OAI.ElementaryPositivity.SlopeArithmetic.high_mass_destabilizes line 19
4. def OAI.ElementaryPositivity.SlopeArithmetic.CellsOnSlope line 29
5. theorem OAI.ElementaryPositivity.SlopeArithmetic.offSlope_destabilizes line 33
6. lemma OAI.ElementaryPositivity.RawShuffle.quotient_cellTransfer_offSlope line 73
7. lemma OAI.ElementaryPositivity.RawShuffle.quotient_gridShapeTensor_offSlope line 83
8. theorem OAI.ElementaryPositivity.RawShuffle.quotient_gridTensor_sameSlope_support line 104
9. theorem OAI.ElementaryPositivity.RawShuffle.cleared_restriction_sameSlope_support line 124