OAI/Combinatorics/Chromatic/Shuffle/Restriction.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ElementaryPositivity.RawShuffle.labeledPolynomial_cast line 15
2. lemma OAI.ElementaryPositivity.RawShuffle.labeledPolynomial_full line 22
3. lemma OAI.ElementaryPositivity.RawShuffle.rightInput_zero_rename line 32
4. lemma OAI.ElementaryPositivity.RawShuffle.leftInput_zero_rename line 44
5. lemma OAI.ElementaryPositivity.RawShuffle.restrictTensor_zero_left line 57
6. lemma OAI.ElementaryPositivity.RawShuffle.restrictTensor_zero_right line 68
7. lemma OAI.ElementaryPositivity.CoefficientIdeals.polynomial_map_quotient_eq_zero_iff line 85
8. lemma OAI.ElementaryPositivity.RawShuffle.relativeTaylorB_coeff_zero line 101
9. lemma OAI.ElementaryPositivity.RawShuffle.sourceTensorFiltration_cross_cancel line 107
10. lemma OAI.ElementaryPositivity.RawShuffle.castS_trans line 141
11. lemma OAI.ElementaryPositivity.RawShuffle.castS_rfl line 144
12. def OAI.ElementaryPositivity.RawShuffle.castB line 146
13. lemma OAI.ElementaryPositivity.RawShuffle.castB_rfl line 149
14. lemma OAI.ElementaryPositivity.RawShuffle.castB_trans line 151
15. lemma OAI.ElementaryPositivity.RawShuffle.castB_mk line 154
16. lemma OAI.ElementaryPositivity.RawShuffle.restriction_unit_kills_destabilizing line 158
17. def OAI.ElementaryPositivity.RawShuffle.restrictionBUnit line 177
18. lemma OAI.ElementaryPositivity.RawShuffle.restrictionBUnit_mk line 184
19. lemma OAI.ElementaryPositivity.RawShuffle.restrictionBUnit_eq_restrictionB line 189
20. lemma OAI.ElementaryPositivity.RawShuffle.restrictionBUnit_zero_left line 193
21. lemma OAI.ElementaryPositivity.RawShuffle.restrictionBUnit_zero_right line 204