OAI/NumberTheory/JointDickman/Amplification/RamanujanRoots.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Primitive-root sums and the Ramanujan factor

  1. theorem OAI.JointDickman.stdAddChar_natCast line 14
  2. theorem OAI.JointDickman.stdAddChar_eq_primitive_power line 19
  3. theorem OAI.JointDickman.nthRoots_image_stdAddChar line 26
  4. theorem OAI.JointDickman.sum_nthRoots_one line 40
  5. theorem OAI.JointDickman.sum_primitiveRoots_eq_moebius line 59