OAI/NumberTheory/JointDickman/Arithmetic/TotientSummability.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The summable denominator majorant for the singular series

  1. theorem OAI.JointDickman.totient_reciprocal_subpower line 12
  2. theorem OAI.JointDickman.summable_totient_reciprocal_sq line 37