OAI/NumberTheory/DirichletL/Hecke/DyadicReflection.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.SevenEighths.HeckeDyadicReflection.functional_equationline 14 - theorem
OAI.SevenEighths.HeckeDyadicReflection.gamma_real_ratio_boundline 52 - theorem
OAI.SevenEighths.HeckeDyadicReflection.gamma_ratio_strip_boundline 69 - theorem
OAI.SevenEighths.HeckeDyadicReflection.completionScale_rpow_leline 103 - theorem
OAI.SevenEighths.HeckeDyadicReflection.primitive_reflected_boundline 121