integral_sub_center_inv — Mathlib

English

If f(z) = (z−c)^{-1} and R ≠ 0, then the circle integral equals 2πi.

Русский

Если f(z) = (z−c)^{-1} и R ≠ 0, то круговой интеграл равен 2πi.

LaTeX

$$$\\oint z in C(c,R), (z-c)^{-1} = 2\\pi i$ for $R\\neq 0$$$

Lean4

@[simp]
theorem integral_sub_center_inv (c : ℂ) {R : ℝ} (hR : R ≠ 0) : (∮ z in C(c, R), (z - c)⁻¹) = 2 * π * I := by
  simp [circleIntegral, ← div_eq_mul_inv, mul_div_cancel_left₀ _ (circleMap_ne_center hR)]

Похожие утверждения