OAI/NumberTheory/JointDickman/Amplification/ConditionedRootComparison.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Independent-root error at an unoccupied prime

  1. theorem OAI.JointDickman.categorical_shift_l1 line 10
  2. theorem OAI.JointDickman.unoccupied_reciprocal_estimates line 29
  3. theorem OAI.JointDickman.unoccupied_categorical_l1 line 57
  4. theorem OAI.JointDickman.unoccupied_roots_test_bound line 87