OAI/Combinatorics/Chromatic/Shuffle/ManyBlockDiagonal.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ElementaryPositivity.RawShuffle.pairRelativeCoefficient line 15
  2. lemma OAI.ElementaryPositivity.RawShuffle.pairRelativeCoefficient_wrong_degree line 23
  3. def OAI.ElementaryPositivity.RawShuffle.SplitTree.pairRefinementCoefficient line 35
  4. theorem OAI.ElementaryPositivity.RawShuffle.SplitTree.pairRefinementCoefficient_zero line 45
  5. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.evalRat_extendPolynomial line 115
  6. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.evalRat_toMvPolynomial line 127
  7. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.evalRat_mapAlgHom line 134
  8. def OAI.ElementaryPositivity.RawShuffle.SplitTree.translationAtB line 142
  9. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.centerTranslation_evalRat line 149
  10. def OAI.ElementaryPositivity.RawShuffle.SplitTree.polynomialOnLeft line 169
  11. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.polynomialOnLeft_eval_tmul line 179
  12. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.polynomialOnLeft_coeff_tmul line 191
  13. def OAI.ElementaryPositivity.RawShuffle.SplitTree.pairRelativeRefinement line 202
  14. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.pairRelativeRefinement_eval_tmul line 214
  15. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.pairRefinement_translationAtB line 227
  16. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.pairRefinement_centerTranslation line 266
  17. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.toRelative_mapLinear line 305
  18. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.pairRelativeRefinement_component_coeff line 316
  19. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.restrictionB_two line 332
  20. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.restrictionB_pairRefinement line 345
  21. lemma OAI.ElementaryPositivity.RawShuffle.SplitTree.centeredRestrictionB_pairRefinement line 389
  22. theorem OAI.ElementaryPositivity.RawShuffle.SplitTree.pairLeading_diagonal_divisible line 405