OAI/Combinatorics/Chromatic/Walls/HNSpanning.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ElementaryPositivity.SlopeArithmetic.hnWordSpace line 12
  2. lemma OAI.ElementaryPositivity.SlopeArithmetic.hnWordSpace_nil line 14
  3. lemma OAI.ElementaryPositivity.SlopeArithmetic.hnWordSpace_cons line 16
  4. lemma OAI.ElementaryPositivity.SlopeArithmetic.hnWordSpace_singleton line 19
  5. lemma OAI.ElementaryPositivity.SlopeArithmetic.hnWordSpace_append line 21
  6. def OAI.ElementaryPositivity.SlopeArithmetic.hnOrderedSpan line 24
  7. lemma OAI.ElementaryPositivity.SlopeArithmetic.hnWordSpace_le line 26
  8. theorem OAI.ElementaryPositivity.SlopeArithmetic.hn_spanning line 40
  9. def OAI.ElementaryPositivity.CenterCalculus.mapLinear line 129
  10. lemma OAI.ElementaryPositivity.CenterCalculus.coeff_mapLinear line 136
  11. lemma OAI.ElementaryPositivity.CenterCalculus.mapLinear_monomial line 141
  12. def OAI.ElementaryPositivity.CenterCalculus.evalRat line 149
  13. lemma OAI.ElementaryPositivity.CenterCalculus.evalRat_C line 153
  14. lemma OAI.ElementaryPositivity.CenterCalculus.evalRat_X line 157
  15. lemma OAI.ElementaryPositivity.CenterCalculus.evalRat_monomial line 161
  16. lemma OAI.ElementaryPositivity.CenterCalculus.evalRat_mapLinear line 168
  17. theorem OAI.ElementaryPositivity.CenterCalculus.eq_of_evalRat line 176
  18. def OAI.ElementaryPositivity.CenterCalculus.toRelative line 202
  19. def OAI.ElementaryPositivity.CenterCalculus.fromRelative line 209
  20. lemma OAI.ElementaryPositivity.CenterCalculus.toRelative_C line 216
  21. lemma OAI.ElementaryPositivity.CenterCalculus.toRelative_first line 220
  22. lemma OAI.ElementaryPositivity.CenterCalculus.toRelative_second line 224
  23. lemma OAI.ElementaryPositivity.CenterCalculus.toRelative_other line 228
  24. lemma OAI.ElementaryPositivity.CenterCalculus.fromRelative_C line 232
  25. lemma OAI.ElementaryPositivity.CenterCalculus.fromRelative_common line 237
  26. lemma OAI.ElementaryPositivity.CenterCalculus.fromRelative_other line 241
  27. lemma OAI.ElementaryPositivity.CenterCalculus.fromRelative_toRelative line 245
  28. theorem OAI.ElementaryPositivity.CenterCalculus.diagonal_dvd_of_relative_coeff line 258
  29. def OAI.ElementaryPositivity.CenterCalculus.relativePoint line 269
  30. lemma OAI.ElementaryPositivity.CenterCalculus.polynomial_eval_rat_algebraMap line 276
  31. lemma OAI.ElementaryPositivity.CenterCalculus.evalRat_toRelative line 280