OAI/NumberTheory/Chromatic/Bounds.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Elementary degree and divisibility bounds for chromatic sphere products.

  1. def OAI.SphereKernelArithmetic.stemDegree line 9
  2. def OAI.SphereKernelArithmetic.powerExponent line 11
  3. theorem OAI.SphereKernelArithmetic.stemDegree_pos_even line 13
  4. theorem OAI.SphereKernelArithmetic.upper_height_margin line 28
  5. theorem OAI.SphereKernelArithmetic.not_dvd_upper_dimension line 40