Theorems · Theorem · complex analysis

circleIntegral.integral_smul_const

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

Defined in

Mathlib.MeasureTheory.Integral.CircleIntegral

Cited by

3 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceCompleteSpace