OAI/NumberTheory/Ostmann/QuadraticCenter/RankinParameterBudget.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Specializing the high-weight Rankin parameter at the manuscript's exponents

  1. theorem OAI.Ostmann.rankin_parameter_budget line 11