`eulerZeroWindingCert`

definition

show as: view math explainer →

module: IndisputableMonolith.NumberTheory.EulerCarrierComplex
domain: NumberTheory
line: 143 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.NumberTheory.EulerCarrierComplex on GitHub at line 143.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 140  zero_winding := carrier_zero_winding cert
 141
 142/-- The Euler carrier's zero-winding certificate for any σ₀ > 1/2. -/
 143noncomputable def eulerZeroWindingCert (σ₀ : ℝ) (hσ : 1/2 < σ₀) :
 144    ZeroWindingCert :=
 145  (mkComplexCarrierCert σ₀ hσ).toZeroWindingCert
 146
 147end
 148
 149end EulerCarrierComplex
 150end NumberTheory
 151end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.