Theorem: circle_integral_sub_center_inv_smul (RMT4/cindex.lean)

State before:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f g : ℂ → E
r : ℝ
U : Set ℂ
c : ℂ
v : E
hr : 0 < r
⊢ (∮ (z : ℂ) in C(c, r), (z - c)⁻¹ • v) = (2 * ↑π * I) • v
Tactic:
simp [circleIntegral.integral_sub_inv_of_mem_ball (mem_ball_self hr)]
State after:
no goals