OAI/Combinatorics/Chromatic/Shuffle/RestrictionB.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ElementaryPositivity.RawShuffle.dimensionCast_eq_castS line 15
  2. theorem OAI.ElementaryPositivity.RawShuffle.restrict_destabilizing_shuffle line 18
  3. theorem OAI.ElementaryPositivity.RawShuffle.restriction_kills_destabilizingSpace line 33
  4. def OAI.ElementaryPositivity.RawShuffle.restrictionB line 45
  5. lemma OAI.ElementaryPositivity.RawShuffle.restrictionB_mk line 52
  6. def OAI.ElementaryPositivity.RawShuffle.restrictionRelativeB line 57
  7. lemma OAI.ElementaryPositivity.RawShuffle.restrictionRelativeB_mk line 62
  8. inductive OAI.ElementaryPositivity.RawShuffle.SplitTree line 79
  9. def OAI.ElementaryPositivity.RawShuffle.SplitTree.dim line 85
  10. def OAI.ElementaryPositivity.RawShuffle.SplitTree.OnSlope line 89
  11. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.dim_ne_zero line 94
  12. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.slope_dim line 101
  13. def OAI.ElementaryPositivity.RawShuffle.SplitTree.tensor line 110
  14. def OAI.ElementaryPositivity.RawShuffle.SplitTree.tensorMap line 114
  15. def OAI.ElementaryPositivity.RawShuffle.SplitTree.rawFamily line 119
  16. def OAI.ElementaryPositivity.RawShuffle.SplitTree.quotientFamily line 120
  17. def OAI.ElementaryPositivity.RawShuffle.SplitTree.rawRestriction line 123
  18. def OAI.ElementaryPositivity.RawShuffle.SplitTree.quotientMap line 128
  19. def OAI.ElementaryPositivity.RawShuffle.SplitTree.restrictionB line 132
  20. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.restrictionB_square line 143
  21. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.restrictionB_mk line 169
  22. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.restriction_kills line 175