69noncomputable def uniformChargeMesh (N : ℕ) (m : ℤ) : AnnularMesh N where 70 rings := fun n => uniformRingSample n.val m
proof body
Definition body.
71 charge := m 72 uniform_charge := by 73 intro n 74 rfl 75 76/-- The Fredholm–Carleman carrier associated with the Euler product. 77 C(s) = det₂(I−A(s))² = ∏_p (1−p^{−s})² exp(2p^{−s}). 78 Holomorphic and nonvanishing on Re(s) > 1/2. -/
used by (6)
From the project-wide theorem graph. These declarations reference this one in their body.