OAI/NumberTheory/Ostmann/Characters/CharacterPositiveMassExclusion.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Positive harmonic mass of uniformly biased higher-order characters is impossible

  1. theorem OAI.Ostmann.PublishedProgressionInput.eventual_positive_character_mass_exclusion line 12