pith. machine review for the scientific record. sign in
def definition def or abbrev

mkSampledRing

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)

  79def mkSampledRing (cert : ZeroWindingCert) (n : ℕ) (_hn : 0 < n)
  80    (r : ℝ) (hr : 0 < r) (_hrR : r < cert.radius) :
  81    SampledRing n where
  82  center := cert.center

proof body

Definition body.

  83  radius := r
  84  radius_pos := hr
  85  increments := fun _ => 0
  86  winding := 0
  87  winding_constraint := by simp
  88  winding_from_contour := rfl
  89
  90/-! ### §3. Sampled mesh -/
  91
  92/-- A sampled mesh: N concentric sampled rings with uniform charge 0. -/

used by (2)

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

depends on (8)

Lean names referenced from this declaration's body.