def definition def or abbrev

`eulerZeroWindingCert`

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

formal statement (Lean)

 143noncomputable def eulerZeroWindingCert (σ₀ : ℝ) (hσ : 1/2 < σ₀) :
 144    ZeroWindingCert :=

Definition body.

 145  (mkComplexCarrierCert σ₀ hσ).toZeroWindingCert
 146
 147end
 148
 149end EulerCarrierComplex
 150end NumberTheory
 151end IndisputableMonolith

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

eulerSampledBudgetedCarrier in IndisputableMonolith.NumberTheory.EulerInstantiation decl_use
riemann_hypothesis_euler_conditional in IndisputableMonolith.NumberTheory.EulerInstantiation decl_use

Lean names referenced from this declaration's body.

mkComplexCarrierCert in IndisputableMonolith.NumberTheory.EulerCarrierComplex decl_use
ZeroWindingCert in IndisputableMonolith.NumberTheory.EulerCarrierComplex decl_use