OAI/NumberTheory/TotientAsymptotic/MertensEuler.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A finite Euler product controlled by a convergent real power series.

  1. def OAI.TotientAsymptotic.negativePower line 13
  2. lemma OAI.TotientAsymptotic.negative_power_sum_le line 19
  3. lemma OAI.TotientAsymptotic.finite_power_euler_product_le line 44