OAI/NumberTheory/Ostmann/ZeroDensity/SmoothOriginResidue.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Identification of the literal even-character residue at zero

  1. theorem OAI.Ostmann.smoothContour_origin_residue_value line 14
  2. theorem OAI.Ostmann.smoothContour_origin_residue line 22
  3. theorem OAI.Ostmann.smoothContour_origin_circle line 29