OAI/NumberTheory/JointDickman/Arithmetic/SquarefreeMinorArc.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The squarefree exponential bound off the manuscript's rational arcs

  1. theorem OAI.JointDickman.squarefree_minor_arc_sum_bound line 10