OAI/Combinatorics/Chromatic/GradedAlgebra/Eval.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ElementaryPositivity.IndependentCenters.eval line 9
  2. def OAI.ElementaryPositivity.IndependentCenters.substitute line 13
  3. lemma OAI.ElementaryPositivity.IndependentCenters.substitute_C_C line 18
  4. lemma OAI.ElementaryPositivity.IndependentCenters.substitute_C_X line 23
  5. lemma OAI.ElementaryPositivity.IndependentCenters.substitute_X line 28
  6. lemma OAI.ElementaryPositivity.IndependentCenters.eval_C_C line 32
  7. lemma OAI.ElementaryPositivity.IndependentCenters.eval_C_X line 37
  8. lemma OAI.ElementaryPositivity.IndependentCenters.eval_X line 42
  9. def OAI.ElementaryPositivity.IndependentCenters.plus line 47
  10. def OAI.ElementaryPositivity.IndependentCenters.minus line 49
  11. lemma OAI.ElementaryPositivity.IndependentCenters.minus_plus line 53
  12. lemma OAI.ElementaryPositivity.IndependentCenters.plus_minus line 62
  13. lemma OAI.ElementaryPositivity.IndependentCenters.minus_plus_apply line 71
  14. lemma OAI.ElementaryPositivity.IndependentCenters.plus_minus_apply line 74
  15. lemma OAI.ElementaryPositivity.IndependentCenters.eval_plus line 77
  16. lemma OAI.ElementaryPositivity.IndependentCenters.diagonal_dvd_of_relative_dvd line 89
  17. def OAI.ElementaryPositivity.IndependentCenters.diagonal line 98
  18. def OAI.ElementaryPositivity.IndependentCenters.DiagonalDivides line 101
  19. lemma OAI.ElementaryPositivity.IndependentCenters.diagonalDivides_of_relative line 105