OAI/NumberTheory/Ostmann/Quadratic/QuadraticTotientMain.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The exact totient coefficient of the coprime Poisson main term

  1. theorem OAI.Ostmann.quadratic_totient_moebius line 12