OAI/NumberTheory/JointDickman/Arithmetic/DivisorProductDifference.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Removing large-prime factors from a divisor product in mean

  1. theorem OAI.JointDickman.divisor_product_difference_mean line 9