OAI/NumberTheory/CubicMoment/Transform/MetaplecticTotient.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The exact finite coprimality density at a squarefree primary level. Only residue-ring cardinalities and the ordinary Chinese remainder theorem enter this calculation.

  1. lemma OAI.CubicFirstMoment.metaplecticTotient_mul line 15
  2. lemma OAI.CubicFirstMoment.metaplecticTotient_prime line 25
  3. lemma OAI.CubicFirstMoment.metaplecticTotient_prod line 35
  4. lemma OAI.CubicFirstMoment.metaplecticTotient_density line 62
  5. lemma OAI.CubicFirstMoment.primary_moebius_density line 78