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

winding_integral_simple_pole

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)

 313theorem winding_integral_simple_pole (c w : ℂ) (R : ℝ) (hw : w ∈ Metric.ball c R) :
 314    (∮ z in C(c, R), (z - w)⁻¹) = 2 * ↑π * Complex.I :=

proof body

Term-mode proof.

 315  circleIntegral.integral_sub_inv_of_mem_ball hw
 316
 317/-- Cauchy–Goursat for the circle: if `f` is holomorphic on the closed disk
 318(possibly off a countable set), the contour integral vanishes. -/

used by (1)

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

depends on (6)

Lean names referenced from this declaration's body.