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

zeroDefect_eq_cosh_sub_one

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)

  53theorem zeroDefect_eq_cosh_sub_one (ρ : ℂ) :
  54    zeroDefect ρ = Real.cosh (zeroDeviation ρ) - 1 := by

proof body

Term-mode proof.

  55  simpa [Foundation.DiscretenessForcing.J_log] using zeroDefect_eq_J_log ρ
  56
  57/-- A point lies on the critical line exactly when its zero deviation is zero. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (13)

Lean names referenced from this declaration's body.