pith. machine review for the scientific record. sign in
theorem proved term proof

zetaReciprocal_order_at_zero

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 570theorem zetaReciprocal_order_at_zero (ρ : ℂ) (m : ℤ) (hm : 0 < m)
 571    (hzeta : meromorphicOrderAt riemannZeta ρ = ↑m) :
 572    meromorphicOrderAt zetaReciprocal ρ = ↑(-m) := by

proof body

Term-mode proof.

 573  rw [meromorphicOrderAt_zetaReciprocal, hzeta]; simp
 574
 575/-- A defect sensor witnessed by an actual meromorphic-order statement for
 576`ζ⁻¹` at a complex point `ρ` in the strip.
 577
 578The existing `DefectSensor` only records charge and real part; this stronger

depends on (10)

Lean names referenced from this declaration's body.