OAI/NumberTheory/JointDickman/Arithmetic/FixedDivisorWeights.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Removing a fixed divisor from finite-prime weights and intervals

  1. theorem OAI.JointDickman.finitePrimeWeight_mul_fixed line 9
  2. theorem OAI.JointDickman.fixedDivisorWeight_bounds line 23
  3. theorem OAI.JointDickman.sum_divisible_interval line 31