OAI/Combinatorics/Chromatic/GradedAlgebra/UnitalProduct.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ElementaryPositivity.SlopeArithmetic.OnSlopeOrZero.mass_eq line 10
2. lemma OAI.ElementaryPositivity.SlopeArithmetic.high_mass_destabilizes_onSlope line 17
3. theorem OAI.ElementaryPositivity.SlopeArithmetic.offSlope_destabilizes_onSlope line 33
4. lemma OAI.ElementaryPositivity.RawShuffle.quotient_cellTransfer_offSlope_unital line 66
5. lemma OAI.ElementaryPositivity.RawShuffle.quotient_gridShapeTensor_offSlope_unital line 77
6. theorem OAI.ElementaryPositivity.RawShuffle.quotient_gridTensor_unital_support line 98