OAI/NumberTheory/Ostmann/Characters/PrimitiveCharacterSieve.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The additive-sieve majorant for one primitive character

  1. theorem OAI.Ostmann.sum_units_eq_sum_ite line 14
  2. theorem OAI.Ostmann.primitive_unit_gauss line 32
  3. theorem OAI.Ostmann.primitive_character_sieve line 48