Theorems · Theorem · complex analysis

circleIntegral.integral_sub_inv_smul_sub_smul

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (f : ℂ → E) (c w : ℂ) (R : ℝ),
  ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • (z - w) • f z = ∮ (z : ℂ) in C(c, R), f z

Defined in

Mathlib.MeasureTheory.Integral.CircleIntegral

Cited by

2 results in Mathlib

Foundations

Depth 256 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpace