OAI/NumberTheory/JointDickman/Counting/SingleCoefficientIndicators.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The actual regularity events for one coefficient

  1. theorem OAI.JointDickman.indicator_le_of_imp line 12
  2. theorem OAI.JointDickman.single_prefix_upper_indicator line 21
  3. theorem OAI.JointDickman.single_prefix_lower_indicator line 34
  4. theorem OAI.JointDickman.single_tail_indicator line 47