OAI/NumberTheory/Ostmann/Preliminaries/DivisorReciprocalMass.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The reciprocal square-root mass of the selected divisors

  1. theorem OAI.Ostmann.sum_reciprocal_sqrt_divisors line 11
  2. theorem OAI.Ostmann.reciprocal_sqrt_divisor_mass_le line 20