OAI/Combinatorics/Chromatic/Walls/WallUnits.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ElementaryPositivity.WallUnits.elementaryCoeff line 13
  2. def OAI.ElementaryPositivity.WallUnits.elementary line 17
  3. theorem OAI.ElementaryPositivity.WallUnits.coeff_elementary line 20
  4. theorem OAI.ElementaryPositivity.WallUnits.constant_elementary line 24
  5. theorem OAI.ElementaryPositivity.WallUnits.elementaryCoeff_product line 27
  6. theorem OAI.ElementaryPositivity.WallUnits.elementary_tail line 39
  7. theorem OAI.ElementaryPositivity.WallUnits.rescale_C line 57
  8. theorem OAI.ElementaryPositivity.WallUnits.elementary_head line 62
  9. theorem OAI.ElementaryPositivity.WallUnits.elementary_shift line 73
  10. theorem OAI.ElementaryPositivity.WallUnits.rescale_inv_of_const_one line 89
  11. def OAI.ElementaryPositivity.WallUnits.complete line 99
  12. theorem OAI.ElementaryPositivity.WallUnits.complete_shift line 101
  13. theorem OAI.ElementaryPositivity.WallUnits.elementary_ratio line 110
  14. theorem OAI.ElementaryPositivity.WallUnits.complete_ratio line 118
  15. def OAI.ElementaryPositivity.WallUnits.RationalRay.v line 129
  16. def OAI.ElementaryPositivity.WallUnits.RationalRay.q line 130
  17. theorem OAI.ElementaryPositivity.WallUnits.RationalRay.v_nonzero line 131
  18. theorem OAI.ElementaryPositivity.WallUnits.RationalRay.degree_pow line 133
  19. theorem OAI.ElementaryPositivity.WallUnits.RationalRay.q_nonzero line 142
  20. theorem OAI.ElementaryPositivity.WallUnits.RationalRay.q_degree line 144
  21. theorem OAI.ElementaryPositivity.WallUnits.RationalRay.q_not_root_unity line 149
  22. theorem OAI.ElementaryPositivity.WallUnits.RationalRay.q_pow line 155
  23. def OAI.ElementaryPositivity.WallUnits.RationalRay.normalized line 158
  24. theorem OAI.ElementaryPositivity.WallUnits.RationalRay.normalized_coefficient line 160
  25. theorem OAI.ElementaryPositivity.WallUnits.RationalRay.normalized_ratio line 184
  26. def OAI.ElementaryPositivity.WallUnits.PositiveRay.vUnit line 194
  27. def OAI.ElementaryPositivity.WallUnits.PositiveRay.eval line 195
  28. theorem OAI.ElementaryPositivity.WallUnits.PositiveRay.eval_T line 198
  29. def OAI.ElementaryPositivity.WallUnits.PositiveRay.Positive line 201
  30. theorem OAI.ElementaryPositivity.WallUnits.PositiveRay.positive_mul line 204
  31. theorem OAI.ElementaryPositivity.WallUnits.PositiveRay.positive_one line 210
  32. theorem OAI.ElementaryPositivity.WallUnits.PositiveRay.positive_E line 212
  33. theorem OAI.ElementaryPositivity.WallUnits.PositiveRay.geometric line 217
  34. theorem OAI.ElementaryPositivity.WallUnits.PositiveRay.positive_H line 223
  35. theorem OAI.ElementaryPositivity.WallUnits.PositiveRay.positive_E_string line 235
  36. theorem OAI.ElementaryPositivity.WallUnits.PositiveRay.positive_H_string line 244
  37. theorem OAI.ElementaryPositivity.WallUnits.RationalRay.shift_weight line 256
  38. theorem OAI.ElementaryPositivity.WallUnits.RationalRay.elementary_ratio_positive line 263
  39. theorem OAI.ElementaryPositivity.WallUnits.RationalRay.complete_ratio_positive line 270